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@cl.cam.ac.uk