###### 10/29/1

**i) Rules for generating constraints**

**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 A_{1} and other constraints C_{1}, this other expression e_{1} has this other type t_{1}'

**Variable:**

⇩

{x:t_{0}}, ∅ ⊢ x:t_{0}

In English:-

**If** it is assumed that the variable x has the type t_{0} , **and** there are no constraints, **then** variable x has type t_{0} .

**Application:**

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

⇩

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

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= τ2→t_{0}} , the application (e1 e2 ) has the type t_{0}

**Lambda Abstraction**

A, C ⊢ e:τ

⇩

A\x, C∪{τ′ =t_{0}|x:τ′ ∈A} ⊢ λx:t_{0} . e :(t_{0}→τ)

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

τ′ =t_{0} for all the τ′ whose x:τ′ pairs were formerly in A, the lambda abstraction λx:t_{0} . e has type (t_{0}→τ)

**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, t_{0}= (Int→τ) ] for t_{0}

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

[τ:Int, t_{0}: (Int→Int) ]

So,

λx:Int.x has type Int→Int