haskell 中的布尔逻辑和类型答案

【问题标题】：Boolean logic and types in haskellhaskell 中的布尔逻辑和类型
【发布时间】：2013-01-16 03:45:58
【问题描述】：

我目前正在使用 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 以何种方式确定 (==>) 的类型？

【问题讨论】：

这可能会有所帮助：lucacardelli.name/Papers/BasicTypechecking.pdf 它解释了 GHC 用于推断和检查事物类型的基本算法（显然真正的算法更复杂，但这适用于您的示例）
x 的返回类型是 ==> 的返回类型，因为我认为 x 是最外层的函数。

【解决方案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

【讨论】：