在Haskell中的布尔逻辑和类型

Question

我目前正在学习大学的Haskell课程。给定以下Haskell代码：

true::t -> t1 -> t
true = (\x y -> x)

false::t -> t1 -> t1
false = (\x y -> y)

-- Implication
(==>) = (\x y -> x y true)

任务是确定函数 (==>) 的类型。 GHCi 显示它的类型为 (==>) :: (t1 -> (t2 -> t3 -> t2) -> t) -> t1 -> t。

从类型不变可以看出，评估顺序如下：

(==>) = (\x y -> (x y) true)

因此，函数true是(x y)的参数。

有人能解释一下为什么结果类型t绑定到第一个参数的结果上，以及GHCi如何确定(==>)的类型吗？

- user3001

---

这可能会有所帮助：http://lucacardelli.name/Papers/BasicTypechecking.pdf 它解释了 GHC 用于推断和检查事物类型的基本算法（显然，实际算法更复杂，但对于您的示例来说，这很有效）。 - Wes

x的返回类型是==>的返回类型，因为我认为x是最外层的函数。 - user3001

Answer 1

首先，为了更好地概述，

type True t f = t -> f -> t
type False t f = t -> f -> f

让我们称暗示的结果为r，那么在\x y -> x y true :: r中，我们有：

x y :: True t f -> r

所以，x :: y -> True t f -> r，因此

(==>) :: (y -> True t f -> r) -> y -> r

再次扩展True，即为

(==>) :: (y -> (t->f->t) -> r) -> y -> r

- leftaroundabout

---

因为 y 是 x 的参数，所以它再次出现作为第二个参数的类型，因为它必须相同？ - user3001