布尔值和 STLC 的 Church 编码

Question

人们常说

tru t f = t
fls t f = f

在“我们可以使用这些术语来执行测试布尔值真实性的操作”的意义上表示 True 和 False。

但这隐藏了一个重要的警告，它似乎只在无类型的 lambda 演算中才成立。如果我只是将这些值插入到 haskell 中，我可以编写一个函数：

tryMeOnFalse ∷  (∀ t f. t → f → t) → String
tryMeOnFalse tr = "Hi"
a' = tryMeOnFalse tru
b' = tryMeOnFalse fls  -- type error !

在类型级别区分 tru 和 fls。这么说会有多错误/真实：

• 在 STLC 中，tru 和 fls 是一些提升的'Boolean 类型的价值级别见证，类型为'True 和'False
• 在 STLC 中，（强制）类型化值 (tru :: ∀ t . t → t → t) 和 (fls :: ∀ t . t → t → t) 代表 True 和 False（在未类型化中，通常情况下）

编辑：感谢@Daniel Wagner 的回答，我现在意识到我在考虑二阶 Lambda 微积分，而不是我的问题中的 STLC。

Answer 1

这不仅适用于无类型的 lambda 演算；但是在键入的演算中，确实需要像往常一样在键入时要小心。我们应该定义：

type Boolean = forall r. r -> r -> r

我们当然有tru, fls :: Boolean，应该这样注释它们。 但我们确实没有有tryMeOnFalse :: Boolean -> String！所以这里没有真正的矛盾。

您关于 STLC 的 cmets 有点奇怪，因为 STLC 有一个非常不同的打字系统。那里的每个结果类型都需要单独的布尔类型，因为没有 多态性。

在 Haskell 中，当然可以定义仅由tru 或仅由fls 存在的类型（当然，每种类型也由undefined 存在）；但这通常不是很有用。