Type checking

[Jon Fairbairn]

On 2003-12-31 at 19:27GMT "Lee Dixon" wrote:
> Hi,
> 
> Can anyone explain to me how hugs manages to derive that
> 
> f x y z = y (y z) x
> 
> is of type
> 
> f :: a -> ((a -> b) -> a -> b) -> (a -> b) -> b

To begin with, f has three arguments, x y and z, so letting
each of these have types Tx Ty and Tz, f has to have type 

Tx -> Ty -> Tz -> R, for some R.

We see that y is applied to z, so y must have type Tz -> Ry:

f:: Tx -> (Tz -> Ry) -> Tz -> R

but y is also applied to (y z) and x. (y z):: Ry, so y must
also have type

Ry -> Tx -> R since R is the type of the body of f.

so we need to find a type that has instances Tz -> Ry and Ry -> Tx -> R
putting Ry = (a -> b), we want 

Tz -> (a -> b) 

to be the same as 

(a -> b) -> Tx -> R, which it is if Tz = (a -> b), Tx = a
and R = b. ie Ty = (a -> b) -> a -> b.

So substitute all those in the first guess for the type of f
we get

a -> ((a -> b) -> a -> b) -> (a -> b) -> b
|     ---|---                ---|----    |
|        Tz                     Tz       |
|    ---------|----------                |
Tx            Ty                         R

You want to look up unification and Hindley-Milner type
inference.

Does that help?

   Jón


-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk