CSC448: Type Checking Revisited: Hindley-Milner Type Inference [118/133] Previous pageContentsNext page

We differentiate between types of the form:

int
'a -> 'a list
('a -> 'b) -> ('a list) -> ('b list)
        

And type schemes that bind free type variables:

forall [] int
forall ['a] 'a -> 'a list
forall ['a, 'b] ('a -> 'b) -> ('a list) -> ('b list)
        

The type inference process assigns fresh type variables to bound variables in an expression, and then generates equality constraints between types. Those constraints must be satisfiable for the expression to be well-typed.

In addition, when we use a type scheme, we will instantiate the type scheme with fresh type variables.

For example, suppose we started with:

fun f x => head1 (head2 x)
        

We would generate fresh type variables 'a and 'b and say:

f : 'a -> 'b
x : 'a
head (head x) must have type 'b
        

head has type scheme forall ['a] ('a list) -> 'a, but the type variable 'a is bound and so is unrelated to the previous 'a. We instantiate the innermost head with a new type variable 'c:

head : 'c list -> 'c
        

Now we have head x, so we know that:

'c list = 'a
head x : 'c
        

Now we use the type scheme for head with another fresh type variable to get:

head : 'd list -> 'd
        

Applying that to head (head x), we have:

'd list = 'c
head (head x) : 'd
        

Finally, we must add the constraint:

'b = 'd
        

So the overall constraints are:

'b = 'd
'd list = 'c
'c list = 'a
        

And the expression has type 'a -> 'b, which simplifies to ('d list) list -> 'd.

Thus the expression has the type scheme forall ['d] ('d list) list -> 'd.

Previous pageContentsNext page