I recently read this brilliant blog post` and it made lambda calculus make sense to me for the first time. Ok, i say i read it, I got about halfway down before trying to implement the same thing in Nim.
It was...not easy.
i tried generics, i tried templates, but exponentiation and subtraction are stupid hard. (I notice in the otherwise very elegant Go solution on Rosetta Code` they cheated and used a for loop for pow.) I wasn't going to accept defeat that easily, nor was i going to cheat by converting numerals to another type of lambda via integers. So I decided it had to be type erasure. pointers, pointers everywhere!
My solution so far is here: https://play.nim-lang.org/#ix=2RmD please take a look and tell me what you think. I plan on submitting it to Rosetta Code, and maybe get a blog post out of it if I get as far as the Y combinator, but I'd very much like some feedback.
Cheers!
Y combinator
thanks to Ruby: https://www.youtube.com/watch?v=FITJMJjASUs and Haskell: http://r6.ca/blog/20060919T084800Z.html
import sugar
type
Fn[T] = (T)->T
func Y[T](X: (Fn[T])->Fn[T]): Fn[T] =
template lift(f): untyped =
cast[ptr Fn[Fn[T]]](f.unsafeaddr)[]
template lower(f): untyped =
cast[ptr Fn[T]](f.unsafeaddr)[]
(
(gen: Fn[T]->Fn[T]) => gen lower(gen)
)(
(gen: Fn[T])=>(block:
X((v: T) => lift(gen)(gen)v)
)
)
let fact_q = (partial: Fn[int]) => (block:
(n: int)=>(if n == 0: 1 else: n*partial(n-1))
)
echo Y(fact_q)(5)
I think there's a simpler solution, with no templates or macros. My Nim is rusty, but something like this:
import sugar
type Fn[T] = T -> T
type ChurchNum[T] = Fn[T] -> Fn[T]
proc zero[T](f: Fn[T]): Fn[T] =
return proc(x: T): T = x
proc succ[T](c: ChurchNum[T]): ChurchNum[T] =
return proc(f: Fn[T]): Fn[T] =
return proc(x: T): T = f(c(f)(x))
proc incr[T](i: T): T = int(i) + 1
proc toInt[T] (c: ChurchNum[T]): int =
int(c(incr)(0))
proc intToChurch[T](i: int): ChurchNum[T] =
if i == 0:
return zero
else:
return succ(intToChurch(i - 1))
when isMainModule:
let z = ChurchNum[int](zero)
let three = z.succ().succ().succ()
let four = three.succ()
echo("three ->", three.toInt())
echo("four ->", four.toInt())
is a straightforward translation of the Go. I only did zero and succ.
you're right, it's simple up to that point. you'll see if you try to take that farther it's exponentiation and subtraction etc that get complicated. for example exponentiation is proc(base:ChurchNum,exponent:ChurchNum):ChurchNum = exponent(base) which is beautiful, but requires somehow that (T->T) == T, and predicate poses similar problems: a ChurchNum gets applied to a (Pair)->Pair.
I agree the casting is horrible, and I'm all ears for a better way to do things, maybe with the union typepunning?
Or are you suggesting the rosetta code question doesn't need all those tricks, i.e. exp(base,exponent:ChurchNum) could also be defined as exponent(`*`(base))(one) with some currying?
ugh ok fine you're right trick is to wrap the base type in a closure the below can work generically if In is defined as In[T] = proc():T{.closure.} but left the Ts out for clarity
import sugar
type In = proc(): int{.closure.}
type Fn = proc(x: In): In{.closure.}
type Church = proc(f: Fn): Fn{.closure.}
type
Pun[T]{.union.} = object
down: T->T
up: (T->T)->(T->T)
func lift[T](f: T->T): (T->T)->(T->T) =
Pun[T](down: f).up
func lower[T](f: (T->T)->(T->T)): (T->T) =
Pun[T](up: f).down
let zero = proc(f: Fn): Fn {.closure.} =
result = proc(x: In): In{.closure.} = x
let pred = (c: Church)=>((f: Fn)=>((x: In)=>f(c(f)(x))))
let one = zero.pred
let add = proc(c: Church): auto{.closure.} =
result = proc(d: Church): auto{.closure.} =
(d.lift.lift)(pred)(c)
let mul = proc(c: Church): auto{.closure.} =
result = proc(d: Church): auto{.closure.} =
(d.lift.lift)(add(c))(zero)
let exp = proc(c: Church): auto{.closure.} =
result = proc(d: Church): auto{.closure.} =
(d.lift.lift)(mul(c))(one)
let exp2 = proc(c: Church): auto{.closure.} =
result = proc(d: Church): auto{.closure.} =
(d.lift)(c)
let incr = proc(x: In): In{.closure.} =
result = proc(): int = x()+1
proc toInt(c: Church): int = c(incr)(()=>0)()
proc `$`(c: Church): string = $(c.toInt)
let three = one.pred.pred
let four = three.pred
echo [(add three)four, (mul three)four, (exp three)four, (exp2 four)three]
@shirleyQuirk, I have been intrigued by this ever since I first saw this post, and extended your excellent contribution to add the Church Numeral functions of the isZeroChurch predicate, the Church predecessor function needed for the Church subtraction function, and the Church division function. To do this, I had to extend your type "punning" to include that needed for the Church predecessor function, as although one can write this without the level of punning and test it, it can't then be used by the Church subtraction function as it then has a chained use with variable "Kind"'s of rank of functions depending on the application in the chain, which leads to a non-determinable "infinite" type race: one needs to "pun" the arguments so that a consistent "Church -> Church" results to avoid this type race.
The Church division function is even more interesting as it implements the algorithm "count the number of loops it takes to subtract the divisor for the dividend until zero is reached", using a unwrapped version of the isZeroChurch function as the predicate which controls the branching if not zero or zero. Rather than use the Y-Combinator for the recursion, I just did a direct function call since Nim supports direct proc/func recursion.
I believe that once one knows the techniques to write these extended Church functions, one can write any of the other many Church functions.
I have also contributed the extended functions in Haskell on that same page for comparison, both using raw casting/coercion, and the GHC Haskell "RankNTypes" extension, which automates the "punning" for functions of differing ranks as to Kind.
To show it can also be done in other languages, I also added the extended functions to the C# and F# contributions on the page, although the F# solution is extremely slow due to having to use a kluge to do the function rank conversion in using what is essentially a DotNet dynamic type; F# does have delegates as for the C# solution but they aren't implemented the same way in that the F# type inference applies to the F# version and it doesn't allow the automatic rank conversion.
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.}
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 )
@shirleyquirk:
Sorry, I somehow missed seeing your reply:
I've only seen them (predecessor functions - GBG) based upon church pairs before, what was your inspiration?
I got it from Wikipedia Church Encoding as follows: pred = \\ n f x -> n (\\ g h -> h (g f)) (const x) id in Haskell notation.
Purely cosmetically speaking, I think all the -chuch suffixes are distracting. And i thought about cleaning up some of the meta boiler plate...
Different strokes, and you are particularly adept at the use of Nim macros and templates.
Which for me is a syntax I shall now stare at until I understand what wizardry is going on...
It's taken me quite a while to grok it ;-) The g h function sets up the conditions to reduce the argument n by one function in the composed chain, and the last two applications take care of whether n is zero or not, with the first application reducing the function chain if it is not zero and the second meaning the when the argument n is zero then zero is returned.
(in C++ -GBG) What is &{return y} able to do that proc(x:auto):auto = return y can't do?
Can't help you there, as I've turned my back on C++ for quite some time. I take most interest in functional languages now, other than Nim.
I've now implemented a new RosettaCode Church Numerals that doesn't use casting/punning at all by using Nim's Variant Objects, and this also works in a lot of other languages although in some, one needs to emulate these...
@shirleyquirk: About the YCombinator
trying to get closer to whatever the hell haskell does...
Everything is lazy in Haskell, so to do the same thing in a strict language like Nim, we need to inject some laziness with differed execution using thunks.
As per my RosettaCode Y-Combinator in Nim contribution, the usual name-calling implementation of the true YCombinator with injected laziness:
import sugar
proc ycombo[T](f: () -> T -> T): T = # can't be `func` because Nim thinks `g` is global...
type RecursiveFunc = object # any entity that wraps the recursion!
recfnc: (RecursiveFunc -> T)
let g = (x: RecursiveFunc) => f(() => x.recfnc(x))
g(RecursiveFunc(recfnc: g))
However, as noted in the Haskell contribution, Nim has direct function name-recursion as does Haskell, so this can be more directly implemented as:
import sugar
func ycombo[T](f: () -> T -> T): T = f(() => ycombo(f))
Note that the above is not the direct value-recursion that can be written in Nim but disallowed by the RosettaCode Task; in Haskell, the distinction is often made that value-recursion shares the value, whereas name-recursion doesn't:
import sugar
func ycombo[T](f: () -> T -> T): T =
var x: T; x = f(() => x); x
All three versions can be used for the try Y-Combinator factorial and Fibonacci functions as shown in RosettaCode.