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
More information about the Haskell-Cafe
mailing list