Scala中lambda演算中的布尔逻辑

Question

我正在尝试在 Scala 的 lambda 演算中实现基本的布尔逻辑，但我一开始就卡住了。

我有两种类型：

type λ_T[T] = T => T

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

“假”，效果很好：

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

但是当我尝试实现“真”时，正如它在 lambda 演算的数学背景中给出的那样，我得到了错误的类型：

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

结果错误：类型 λ_T[T] 的表达式不符合预期的类型 T

我该如何实现呢？

Answer 1

布尔值的 Church 编码 is of type

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

其中[X] => 表示X -> X -> X 部分在X 中是多态的。

这里有两个建议，您可以如何在 Scala 中表达这一点。

---

布尔值作为通用方法，在调用点进行类型推断

这是一种适用于布尔值的类型，其中所需的多态类型参数可以直接在调用点推断：

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

下面是true和false的定义，以及一些操作：

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)

例子：

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"))

请注意，这不允许您表达“Church-Boolean per-se”的想法，因为它需要可以应用的固定类型的参数（上例中的String）。一旦您尝试从一个特定的调用站点提取表达式并将其移动到其他位置，您就必须重新调整所有类型参数，这很烦人。

---

布尔值的真正多态 Church 编码

如果你想将一个真正的多态函数表示为一等对象，你必须定义一个特征或抽象类。对于布尔值，这类似于

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

请注意，现在apply 方法在X 中是多态的。这允许您将布尔值的 Church 编码实现为可以传递的一流对象（从方法返回、保存在列表中等）：

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 }

以下是如何将其应用于一些实际值：

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

以上行将调用apply[Boolean](...)。

一个例子：

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)))

打印：

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