haskell - 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)

所以函数trueist 参数(x y)。

谁能解释为什么结果类型 t 绑定到第一个参数的结果以及 GHCi 以哪种方式确定 t 的类型(==>)？

score 4 · Accepted Answer

首先，为了更好地概述，

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

1 回答 1