I did make sure that division worked so I'm not surprised it was easy to add,
but I'm surprised by the elegance of your predicate function. I've only seen
them based upon church pairs before, what was your inspiration?
Purely cosmetically speaking, I think all the -chuch suffixes are distracting.
And i thought about cleaning up some of the meta boiler plate:
import sugar, macros,std/genasts
template Meta(T:type):type = T->T
template Sesqui[T](t:typedesc[(T->T)->(T->T)]):type =
(T->T->T)->(T->T->T)
type
In = () -> int # a lazy thunk producing an int
Func = Meta In
Church = Meta Func
macro lifter(x:untyped):untyped =
result = x
let ret_ty = x[3][0]
let param_ty = x[3][1][1]
let param_name = x[3][1][0]
result[6] = genast(ret_ty,param_ty,param_name):
type Pun{.union.}=object
l:param_ty
h:ret_ty
Pun(l:param_name).h
func ²[T](x:T):Meta T{.lifter.}
func ⁴[T](x:T):Meta Meta T{.lifter.}
func ³(x:Church):Meta Sesqui Church {.lifter.}
Run
Similarly, templates for the common lambda definitions might make things more
readable, if lambda calculus syntax counts as readable:
template λc(body:untyped):untyped =(proc(c{.inject.}: Church):Church =
body)
#etc for λf:Func, λx:In, λab:Church
#and maybe for λg:Func λy:In
#so that pred can be written like so:
let pred = λc λf do:
let prd = (gf: In->In->In) => ((hf: In->In) => hf gf f)
# magic is here, reduces by one function level...
λx (c.³)(prd)( λg x )( λy y )
Run
