Post #14

代数类型中的值可以按特定的规则对应到 Lambda 演算中的函数，例如： Bool 有两个情况：True 和 False，都不需要参数。True 可以对应到 λonTrue.λonFalse.onTrue，False 可以对应到 λonTrue.λonFalse.onFalse。这种对应关系也是最广为使用的。 Pair 有一个情况，但有两个参数。Pair a b 可以对应到 λonPair.onPair a b。使用示例：构造一个包含 1 和 3 的 Pair：p = λonPair.onPair 1 3。从中取出第一项：p (λa.λb.a) Maybe 有两个情况，第一个情况叫 Just，有一个参数。第二个情况叫 Nothing，没有参数。可以令 Just = λa.λonJust.λonNothing.onJust a，Nothing = λonJust.λonNothing.onNothing。 推而广之，考虑到自然数类型 Nat 有两个情况，第一种情况叫 Zero，没有参数。第二种情况叫 Succ，有一个参数。可以令 Zero = λonZero.λonSucc.onZero，Succ = λa.λonZero.λonSucc.onSucc a。在这种定义下，0 = Zero，1 = Succ 0，2 = Succ 1，… 这个定义和常见的 Church numbers 并不一样，但似乎更好用（也和其他类型的映射规则更统一），因为这个定义使得模式匹配成为可能，然后很容易定义减一函数，只要先写出伪代码： Pred Zero = Zero Pred (Succ n) = n 然后翻译过来： Pred = λx.x (Zero) (λn.n) （第一个括号中是 onZero，第二个括号中是 onSucc） 很好奇这种把代数类型对应过来的规则叫什么名字，以及这样构造的自然数叫什么，可是随便搜了一会什么也没找到