Church encodings in Scala
Follow-up of https://discord.com/channels/885109005469511700/885109005469511704/922863225689759804.
Representing Church encodings in Scala is not trivial, and we didn't want to show something like that because we did not want to confuse you.
But as some of you tried, here are some examples of how this could be done following what was posted on Discord:
type ChurchNum[T] = (T => T) => T => T // By Fran.
def zero [T]: ChurchNum[T] = f => z => z // By Fran.
def one [T]: ChurchNum[T] = f => z => f(z) // By Fran.
def two [T]: ChurchNum[T] = f => z => f(f(z)) // By Fran.
def three[T]: ChurchNum[T] = f => z => f(f(f(z))) // By Fran.
def toInt[T](i: ChurchNum[Int]): Int = i(_ + 1)(0)
assert(toInt(three) == 3)
def succ[T]: ChurchNum[T] => ChurchNum[T] = (n: ChurchNum[T]) => f => z => f(n(f)(z))
// Trick to make this version work: set type of `n` to `ChurchNum[ChurchNum[T]]`
def add[T]: ChurchNum[ChurchNum[T]] => ChurchNum[T] => ChurchNum[T] = n => m => n(succ)(m)
def add2[T]: ChurchNum[T] => ChurchNum[T] => ChurchNum[T] = a => b => f => z => a(f)(b(f)(z)) // By David Kalajdzic
assert(toInt(add(zero)(one)) == 1)
assert(toInt(add(two)(three)) == 5)
assert(toInt(add2(zero)(one)) == 1)
assert(toInt(add2(two)(three)) == 5)However, the trick used for add is limited. With these typings we can only refer to a specific instance of the type ChurchNum at a time; typing n as ChurchNum[ChurchNum[T]] excludes using it as ChurchNum[T] for example.
To encode Church numerals more faithfully, we could use Scala 3's polymorphic function types: https://docs.scala-lang.org/scala3/reference/new-types/polymorphic-function-types.html. Note that this is advanced material, outside of the scope of this course.
Polymorphic function types allow us to encode the fact that a Church numeral is a function that can be instantiated with any type (a polymorphic function in due form):
type ChurchNum = [T] => (T => T) => T => T
val zero: ChurchNum = [T] => (f: T => T) => (z: T) => z
val one: ChurchNum = [T] => (f: T => T) => (z: T) => f(z)
val two: ChurchNum = [T] => (f: T => T) => (z: T) => f(f(z))
val three: ChurchNum = [T] => (f: T => T) => (z: T) => f(f(f(z)))
def toInt(i: ChurchNum): Int = i[Int](_ + 1)(0)
assert(toInt(three) == 3)
val succ: ChurchNum => ChurchNum = (n: ChurchNum) => [T] => (f: T => T) => (z: T) => f(n(f)(z))
val add: ChurchNum => ChurchNum => ChurchNum = n => m => n(succ)(m)
val add2: ChurchNum => ChurchNum => ChurchNum = a => b => [T] => (f: T => T) => (z: T) => a(f)(b(f)(z))
assert(toInt(add(zero)(one)) == 1)
assert(toInt(add(two)(three)) == 5)
assert(toInt(add2(zero)(one)) == 1)
assert(toInt(add2(two)(three)) == 5)We could represent Church Booleans similarly:
type ChurchBool = [T] => T => T => T
val tru: ChurchBool = [T] => (x: T) => (y: T) => x
val fls: ChurchBool = [T] => (x: T) => (y: T) => y
val not2 /*: ChurchBool => ChurchBool*/ = (a: ChurchBool) => [T] => (x: T) => (y: T) => a(y)(x)
val and: ChurchBool => ChurchBool => ChurchBool = (a: ChurchBool) => (b: ChurchBool) => a(b)(fls)
val nand: ChurchBool => ChurchBool => ChurchBool = (a: ChurchBool) => (b: ChurchBool) => a(not2(b))(not2(a))
val nand2: ChurchBool => ChurchBool => ChurchBool = (a: ChurchBool) => (b: ChurchBool) => a(not2(b))(tru)
def toBool(b: ChurchBool): Boolean = b(true)(false)
assert(toBool(not2(nand2(tru)(tru))) == true)This is not prefect, as inference does not always work as expected (or at least I could not make it work, see the not2 case for example).
Also, we can not represent church lists as we'd need a recursive type definition which is not supported yet:
type ChurchList = [A, L] => (n: L) => (c: A => ChurchList => L) => L
// illegal cyclic type referenceAnyway, if these thoughts can help some of you to better understand Church encodings, good. Otherwise, if this yields to more confusion, just forget it