###### 6/21/21

**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]. Also consulted was Benjamin C. Pierce, 2002, *Types and Programming Languages*. ]

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} . [This inference rule does not require any premises.]

**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

## A reminder

**STLC (Simply Typed Lambda Calculus)**

i) insists on annotation of the lambda variable in an abstraction. So, for example, λa:(I->I).(a 3) is well-formed, whereas λa.(a 3) is not well-formed

ii) has no type variables in the expression language. So, for example, STLC has no well-formed abstraction similar to λx:TypeVar1.x

iii) in our example STLC there are just two basic type constants I (for integer) and B (for boolean). Infinitely many atomic expressions in the expression language have type I (namely, 0,1,2,3... etc.) Two atomic expressions in the expression language have type B (namely, True, False). Infinitely many other expressions in the expression language have type I, and similarly for B, for example, an identity abstraction can be applied to an integer, say, 3, then the same identity abstraction can be applied to itself applied to 3, and so on (all these infinite applications will have type I)

iv) further type constants can be constructed from the two basic ones using the constructor '->', for example B->I, (I->I)->B, etc