Hindley-Milner II — Generating the Constraints

6/21/21

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

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

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

 

 

To be continued