Boolean logic in lambda calculus in Scala

Question

I am trying to implement basic Boolean logic in lambda calculus in Scala, but I am stuck at the beginning.

I have two types:

type λ_T[T] = T => T

type λ_λ_T[T] = λ_T[T] => T => T

And 'false', that works pretty well:

def λfalse[T]: λ_λ_T[T] = (s: λ_T[T]) => (z: T) => z

But when I try to implement 'true', as It is given in math background of lambda calculus, I get wrong type:

def λtrue[T]: λ_λ_T[T] = (s: λ_T[T]) => (z: T) => s

Outcome error: Expression of type λ_T[T] doesn't conform to expected type T

How can I implement this?

Andrey Tyukin Andrey Tyukin · Accepted Answer · 2018-06-21T11:00:54

A Church encoding of Booleans is of type

[X] => X -> X -> X

where [X] => means that the X -> X -> X-part is polymorphic in X.

Here are two proposals how you could express this in Scala.

Booleans as generic methods, type inference at call-site

Here is a type that would be appropriate for booleans where the required polymorphic type parameter can be inferred directly at the call-site:

type B[X] = X => X => X

Here are the definitions of true and false, together with a few operations:

def churchTrue[X]: B[X] = a => b => a
def churchFalse[X]: B[X] = a => b => b
def ifThenElse[X](b: B[X], thenResult: X, elseResult: X) = 
  b(thenResult)(elseResult)

def and[X](a: B[B[X]], b: B[X]): B[X] = a(b)(churchFalse)
def or[X](a: B[B[X]], b: B[X]): B[X] = a(churchTrue)(b)
def not[X](a: B[B[X]]) = a(churchFalse)(churchTrue)

Example:

println("t & t = " + and[String](churchTrue, churchTrue)("t")("f"))
println("t & f = " + and[String](churchTrue, churchFalse)("t")("f"))
println("f & t = " + and[String](churchFalse,churchTrue)("t")("f"))
println("f & f = " + and[String](churchFalse,churchFalse)("t")("f"))

Note that this does not allow you to express the idea of a "Church-Boolean per-se", because it requires a fixed type of the arguments to which it can be applied (String in the above example). As soon as you try to extract the expression from one particular call site and move it elsewhere, you have to readjust all the type parameters, and this is annoying.

Truly polymorphic Church encodings of Booleans

If you want to represent a truly polymorphic function as first-class object, you have to define a trait or abstract class. For booleans, this would be something like

trait B {
  def apply[X](trueCase: X, elseCase: X): X
}

Note that now the apply method is polymorphic in X. This allows you to implement Church encodings of Booleans as first-class objects that can be passed around (returned from methods, saved in lists, etc.):

trait B { self =>
  def apply[X](thenCase: X, elseCase: X): X
  def |(other: B): B = new B { 
    def apply[A](t: A, e: A) = self(True, other)(t, e) 
  }
  def &(other: B): B = new B { 
    def apply[A](t: A, e: A) = self(other, False)(t, e) 
  }
  def unary_~ : B = self(False, True)
}

object True extends B { def apply[X](a: X, b: X) = a }
object False extends B { def apply[X](a: X, b: X) = b }

Here is how you can apply it to some actual values:

def toBoolean(b: B): Boolean = b(true, false)

The above line will invoke apply[Boolean](...).

An example:

println("And: ")
println(toBoolean(True & True))
println(toBoolean(True & False))
println(toBoolean(False & True))
println(toBoolean(False & False))

println("Or:")
println(toBoolean(True | True))
println(toBoolean(True | False))
println(toBoolean(False | True))
println(toBoolean(False | False))  

println("Funny expresssion that should be `true`:")
println(toBoolean((False | True) & (True & ~False)))

prints:

And: 
  true
  false
  false
  false
Or:
  true
  true
  true
  false
Funny expresssion that should be `true`:
  true

Boolean logic in lambda calculus in Scala

1 Answers