8/28/21
Using constraints
As alluded to earlier, with Junior Hindley-Milner, constraints make the problem of finding types much easier. Some of the expression forms imposes constraints. These constraints can be collected up and the collection solved (mgu (most general unification) will produce a suitable substitution).
In the Junior Hindley Milner pages, all the constraints were equalities e.g. that τ1= τ2->σ . Going forward there may be some constraints of a different form e.g. that one type is an instance of a type scheme. To add some detail.
Explicit instance constraints
Say a let variable has been annotated with a universally quantified type-scheme, for example, 'let identity:∀(a->a)=λx .x in (identity 7)'. Now, the identity function in the application (identity 7) needs to have type Int->Int. But the initial local variable identity as introduce has type ∀(a->a). Clearly these two types do not need to be equal (they are not, and they do not unify while the universal quantifier ∀ is in place). What needs to happen is that Int->Int be an instance of ∀(a->a) (which it is). The scheme is instantiated to a0->a0, say, using new type variables, and a0->a0 is unified with Int->Int. We can require, as a constraint, in a case like this, that one type is an (explicit) instance of another type or type scheme.
Implicit instance constraints
Implicit instance constraints are similar to explicit instance constraints, but slightly different. These occur where there is no annotation, for example, 'let identity=λx .x in let ignore= (identity True) in (identity 7)' . This time we know, or suspect, that the type of the whole let expression is going to be Int. But the local identity variable seems to have type Bool->Bool in one use and Int->Int in another and yet nothing is said about its type when it is declared, without annotation, in identity=λx .x . The type of identity is going to need to be a type scheme, probably with a universal quantifier, and Bool->Bool and Int->Int are going to need to be instances of that scheme. We can require, as a constraint, in a case like this, that one type is an (implicit) instance of another type or type scheme. But what is an (implicit) instance of what? We take the defined expression, in this case λx .x, and get its type, which is a->a for some type variable. Then we generalize this. Generalization consists identifying the free type variables, in this case a, and binding them using a universal quantifier. The result, in this case, is the type-scheme ∀a (a->a) . So, the (implicit) constraints here are that Bool->Bool and Int->Int be instances of the scheme ∀a (a->a).
The constraint rules
The determination of type can be made using 'constraint typing rules'. Each typing rule has some premises and a conclusion. The premises are written above a horizontal line and the conclusion below that line. Each rule permits one step of the derivation or inference.
Of vital importance are new type variables. Several of the rules introduce type variables. These need to be totally new to the whole reasoning or proof. Conceptually, we can imagine a central source of type variables and each time a type variable is introduced that central source supplies a new one. (Side remark: in some programming languages a global might be used to supply the new variables; in functional programming languages a monad might be used.)
The general form
| <premises> or <preconditions> <environment> ⊢ <expression>:<its type> <constraints> |
Variable (i.e. the expression, e, whose type is to be determined ,is a term-variable)
| (e:τ) ∈ Γ Γ ⊢ e:σ {} |
If the expression e to be typed is a term-variable, and it has a value in the environment, then its type is that value and there are no constraints.
Examples of the use of this rule include
| (e:I) ∈ Γ Γ ⊢ e:I {} |
(e:I->B) ∈ Γ Γ ⊢ e:I->B {} |
Constant (i.e. the expression, e, whose type is to be determined is either a Boolean (B) or an Integer (I))
|
Γ ⊢ <a Boolean>:B {} |
Γ ⊢ <an Integer>:I {} |
If an expression is True or False, its type is a B. If an expression is one of 0,1,2,3... etc., its type is I. This produces no constraints.
Lambda (i.e. the expression, λx.e, whose type is to be determined is a function, without annotation)
This rule requires that the lambda variable (x in the case of λx.e) not be in the original or unaugmented environment. If it is, the lambda expression is alpha-rewritten to use another variable, say y, to give an equivalent expression λy.e which satisfies the precondition
| Γ ∪ {x:τ } ⊢ e:σ C Γ ⊢ λx.e : τ->σ C |
If {x:τ } is added to the environment, and, then, an expression e (the potential scope) has the type σ requiring constraints C, then a lambda expression λx.e has the type τ->σ using the environment Γ without {x:τ } and the constraints C are unchanged.
Lambda with annotation (i.e. the expression, λx.e, whose type is to be determined is a function, with annotation)
What is in prospect here is that an extra constraint is going to be added to the constraints, and that new constraint will assert that the type of the annotated lambda variable is to be that requested by the annotation.
This rule requires that the lambda variable (x in the case of λx.e) not be in the original or unaugmented environment. If it is, the lambda expression is alpha-rewritten to use another variable, say y, to give an equivalent expression λy.e which satisfies the precondition.
| Γ ∪ {x:τ } ⊢ e:σ C Γ ⊢ λx:a.e : τ->σ C ∪ {τ= a} /* a is the annotation */ |
If {x:τ } is added to the environment, and, then, an expression e (the potential scope) has the type σ requiring constraints C, then a lambda expression λx:a.e has the type τ->σ using the environment Γ without {x:τ } and the constraints C are augmented by the additional constraint {τ= a} .
[There is a small issue here that might arise in implementations. The annotation, for type, is in the MiniML expression language e.g the B (for 'Boolean') in λx:B.x . But our reasoning about constraints uses what we have called a type 'algebra' with, for example, τ0, τ1= τ2->σ, etc. What has to happen is that the expression used in the type algebra has to be the right one corresponding to the annotation in the MiniML expression language. We can probably leave it to actual programmers to worry about this.]
Application (i.e. the expression, (e1 e2) whose type is to be determined is an application)
There is a new type variable, σ, that is going to be used here. This needs to be not a free type variable of any of the prior environments or constraints. And easy way to achieve this is to ensure that σ is completely new.
C' = C1 ∪ C2 ∪ {τ1= τ2->σ}
| Γ ⊢ e1:τ1 C1 and Γ ⊢ e2: τ2 C2 and C' is defined as C' = C1 ∪ C2 ∪ {τ1= τ2->σ} /*σ new */ Γ ⊢ (e1 e2) : σ C' |
If you are trying to type an application (e1 e2) ... If e1 has the type τ->σ and e2 has the type , then (e1 e2) has the type σ .
Let without annotation (i.e. the expression, let x=e1 in e2) whose type is to be determined is an unannotated let expression)
|
Γ ⊢ e1:τ C1 and Γ∪{x:∀A(τ) } ⊢ e2: σ C2 i) the term variable x needs not to have a prior valuation |
Let with annotation (i.e. the expression, let x=e1 in e2) whose type is to be determined is an annotated let expression)
|
Γ ⊢ e1:τ C1 and Γ∪{x:a } ⊢ e2: σ C2 i) the term variable x needs not to have a prior valuation |