CSC448: Type Checking Revisited: Hindley-Milner Type Inference [118/133] |
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
.