Hindley-Milner II — Generating the Constraints

10/29/1

i) Rules for generating constraints

 

[We are following Bastiaan Heeren, Jurriaan Hage, Doaitse Swierstra 2002, Generalizing Hindley-Milner Type Inference Algorithms. Henceforward Heeren [2002] ]

Each of the inference rules has roughly the following form. 'Given assumptions A and constraints C, expression e has type t' then 'Under these other assumptions A1 and other constraints C1,  this other expression e1 has this other type t1'

Variable:

 

{x:t0}, ∅ ⊢ x:t0    

In English:-

If it is assumed that the variable x has the type t0 , and there are no constraints, then variable x has type t0 .

Application:

If A1, C1   e1:τand A2, C2   e2:τ2

A1∪A2, C1∪C2∪{τ1= τ2t0} ⊢(e1 e2 ):t0

In English:-

If expression  e1 has type τ1 under the assumptions A1 and constraints C1 and expression  e2 has type τ2 under the assumptions A2 and constraints C2
then under the assumptions of A1 and A2 combined together and the constraints C1 and C2 combined together plus the additional constraint {τ1= τ2t0} , the application (e1 e2 ) has the type t0

Lambda Abstraction

A, C ⊢  e:τ

A\x, C∪{τ=t0|x:τ∈A} ⊢ λx:t0 . e  :(t0τ)


In English:-

If expression  e has type τ under the assumptions A and constraints C
then under the assumptions of A, with all key-value pairs removed for the binding variable x (i.e. remove those with key x), and constraints C, augmented by additional constraints
τ=t0 for all the τ whose x:τpairs were formerly in A, the lambda abstraction λx:t0 . e has type (t0τ)

 

ii) Example of the Lambda Abstraction Rule

These rules are not the easiest to get one's head around. Let us try a simple example

λx:Int.x

This is a lambda abstraction, and to analyze it we need a type for its scope. Now the scope is the plain variable x.

x

We use the Rule for Variables, which requires us to guess a fresh type τ and put that in the assumptions. There are no constraints. Thus

{x:τ}, ∅ ⊢ x:τ

Then we use the Rule for Abstraction on λx:Int.x. It is easiest to work on the constraints first. We need to add τ=Int for all the x:τ' in the Assumptions. There is only one of those

{x:τ}, [τ =Int  result to come

We remove all the assumptions with key 'x'.

, [τ =Int  result to come

The Rule of Abstraction tells us, in this case, that the resulting type is (Intτ)

i.e.

, [τ =Int (Intτ)

We need to solve

=Int (Intτ) ] for the expression (Intτ)

Or to be more explicit about what we are solving for, We need to solve

=Int t0= (Intτ)  ] for t0

'Solving' here means 'find a substitution under which the constraints come out to be true'. Clearly the substitution is

[τ:Int t0: (IntInt)  ]

So,

λx:Int.x has type Int→Int

 

 

 

 

To be continued