haskell的布爾邏輯和類型

我目前擁有Haskell大學。考慮下面的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 IST參數(x y)。

任何人都可以解釋爲什麼結果類型t綁定到第一個參數的結果，以及在哪種方式GHCi確定(==>)的類型？

2013-01-15 user3001

這可能會有所幫助：http://lucacardelli.name/Papers/BasicTypechecking.pdf它解釋說，GHC用來推斷和檢查類型的東西（當然真正的算法是更基本的算法複雜，但這適用於您的示例） – Wes

x的返回類型是==>的返回類型，因爲x是最外層的函數，我認爲。 – user3001

首先，給出更好的概述，

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

哪個，擴大再次，是

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

2013-01-15 19:45:58 leftaroundabout

而且由於y是x的參數，它又會作爲第二個參數的類型出現，因爲它必須是相同的？ – user3001

這就好了。 – leftaroundabout

回答