Boolean logic and types in haskell

Question

I'm currently having Haskell for university. Given the following haskell code:

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

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

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

The task is to determine the type of the function (==>). GHCi says it is (==>) :: (t1 -> (t2 -> t3 -> t2) -> t) -> t1 -> t.

I can see that the evaluation order is the following (as the type stays the same):

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

So the function true ist argument to (x y).

Can anyone explain why the result type t is bound to the result of the first argument and in which way GHCi determines the type of (==>)?

This might be helpful: lucacardelli.name/Papers/BasicTypechecking.pdf It explains the basic algorithm that GHC uses to infer and check types of things (obviously the real algorithm is more complex, but this works for your example) — Wes
The return type of x is the return type of ==> because x is the outermost function, I think. — user3001

leftaroundabout leftaroundabout · Accepted Answer · 2013-01-15T19:45:58

First, to give a better overview,

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

Let's call the result of the implication r, then we have, in \x y -> x y true :: r, that

x y :: True t f -> r

so x :: y -> True t f -> r, and thus

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

which, expanding True again, is

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