3

私は現在、大学で 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 が の型を決定する方法を説明できる人はい(==>)ますか?

4

1 に答える 1

4

まず、概要をよりよく理解するために、

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
于 2013-01-15T19:45:58.030 に答える