lambda calculus in scala

Question

OK, so I'm trying to implement the basics of lambda calculus. Here it goes.

My numbers:

def zero[Z](s: Z => Z)(z: Z): Z = z
def one[Z](s: Z => Z)(z: Z): Z = s(z)
def two[Z](s: Z => Z)(z: Z): Z = s(s(z))

Partially (actually, non) applied version of them is smth like that:

def z[Z]: (Z => Z) => (Z => Z) = zero _

Before I continue I define some types:

type FZ[Z] = Z => Z
type FFZ[Z] = FZ[Z] => FZ[Z]

Fine, succ function goes like (Application order should be exactly like that! I took the definition here):

def succ[Z](w: FFZ[Z])(y: FZ[Z])(x: Z): Z = y((w(y))(x))

And the unapplied version of it gets as scary as:

def s[Z]: FFFZ[Z] = successor _

Beg your pardon, here is the missing types:

type FFFZ[Z] = FFZ[Z] => FFZ[Z]
type FFFFZ[Z] = FFFZ[Z] => FFFZ[Z]

But I'm stuck at the add function. If conformed to types and definition (taken here as well) it goes like

def add[Z](a: FFFFZ[Z])(b: FFZ[Z]): FFZ[Z] =
  (a(s))(b)

But I want a to be a common number of type FFZ[Z].

So -- how can I define addition?

Updo

My first guess was that it works only for untyped lambda calculus, where value is just somehting and function is a mapping from something to something so I can invoke function f whose argument type is, say, a: Z -> Z and it might not not exactly conform to a function f': (Z -> Z) -> (Z -> Z) I apply it to. – Updo

Perhaps a title like "Addition for Church numerals in Scala" would be a bit more precise. – Bipolar

Answer 1

It's totally possible to implement Church numerals in Scala. Here is one such rather straight-forward implementation:

object ChurchNumerals {

  type Succ[Z] = Z => Z
  type ChNum[Z] = Succ[Z] => Z => Z

  def zero[Z]: ChNum[Z] =
    (_: Succ[Z]) => (z: Z) => z

  def succ[Z] (num: ChNum[Z]): ChNum[Z] =
    (s: Succ[Z]) => (z: Z) => s( num(s)(z) )

  // a couple of church constants
  def one[Z] : ChNum[Z] = succ(zero)
  def two[Z] : ChNum[Z] = succ(one)

  // the addition function
  def add[Z] (a: ChNum[Z]) (b: ChNum[Z]) =
    (s: Succ[Z]) => (z: Z) => a(s)( b(s)(z) )

  def four[Z] : ChNum[Z] = add(two)(two)

  // test
  def church_to_int (num: ChNum[Int]): Int =
    num((x: Int) => x + 1)(0)

  def fourInt: Int = church_to_int(four)

  def main(args: Array[String]): Unit = {
    println(s"2 + 2 = ${fourInt}")
  }
}

Compiles and prints:

$ scala church-numerals.scala
2 + 2 = 4

If I were to explain Church numerals from scratch I'd add more commentaries. But taking the context into account, I'm not sure on what to comment in this case. Please feel free to ask and I'll add more explanations.

Bipolar

That's beautiful. Thanks. – Updo

Answer 2

I have coded Numerals, Booleans and Pairs: https://github.com/pedrofurla/church/blob/master/src/main/scala/Church.scala following Church's style.

One thing I noticed is that using the curried function syntax was much easier than using multiple argument lists. Some of the interesting snippets

type NUM[A] = (A => A) => A => A
def succ  [A]: NUM[A]  =>  NUM[A] = m => n => x => n(m(n)(x))
def zero  [A]: NUM[A] = f => x => x
def one   [A]: NUM[A] = f => x => f(x)
def two   [A]: NUM[A] = f => x => f(f(x))
def three [A]: NUM[A] = f => x => f(f(f(x)))
def plus  [A]: (NUM[A]) => (NUM[A]) => NUM[A] = m => n => f => x => m(f)(n(f)(x))

Now for printing them out (very similar to Antov Trunov's solution):

def nvalues[A] = List(zero[A], one[A], two[A], three[A])

val inc: Int => Int  = _ + 1 
def num: (NUM[Int]) => Int = n => n(inc)(0)
def numStr: (NUM[String]) => String = n => n("f (" + _ + ") ")("z")

Some output:

scala> println(nvalues map num)
List(0, 1, 2, 3)

scala> println(nvalues map numStr) // Like this better :)
List(z, f (z) , f (f (z) ) , f (f (f (z) ) ) )

Renz