2

人们常说

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。

4

1 回答 1

4

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

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

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

你对 STLC 的评论有点奇怪，因为 STLC 有一个非常不同的打字系统。因为没有多态性，我们需要为每个结果类型提供单独的布尔类型。

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

于 2016-06-05T18:06:20.220 回答