# Type checking

Jon Fairbairn Jon.Fairbairn at cl.cam.ac.uk
Wed Dec 31 19:48:23 EST 2003

```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

```