7/27/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:τ1 and A2, C2 ⊢ e2:τ2
⇩
A1∪A2, C1∪C2∪{τ1= τ2→t0} ⊢(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= τ2→t0} , 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: (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