Type Inference

PPL 2023

After having described the process of type checking, we now address a more ambitious task in type analysis: type inference.
In this task, we not only verify that a program is safe, we also allow the programmer to leave some (or even all) the type annotations empty - and attempt to guess their value from the structure of the program.

If we can infer such a consistent set of type annotations for the program, we conclude that the program is type safe and provide the annotations. Otherwise, we point to the inconsistency.

To enable this process, we consider all the type annotations in the \(L5\) language as optional. This process is similar to the strategy adopted in TypeScript which we reviewed in Chapter 1 (gradual typing).

We first investigate how we can perform the process of type inference manually, and then present an algorithm which automates this process, relying on a critical operation on substitutions called unification. The operation of unification is a fundamental tool in the semantics of programming languages, and we will further expand its use in Chapter 5 (on Logic Programming).

Type Inference using Type Equations

The algorithm we present extends the type checker method by introducing type equations which are constructed for every sub-expression of the expression to be typed. A solution to the equations assigns types to every sub-expression. The type checking/inference procedure turns into a type equation solver.

Let us first present informally how we would proceed manually to infer the type of some programs.

Type Inference: Example 1

Let us consider an example: we want to type the following expression:

((lambda (x) 
   (+ x 3))
 5)

We consider this equation as an AST where all variable declarations have optional type annotations which are not provided. That is, we view this expression as if it had been provided as follows in the \(L5\) syntax with full type annotations:

((lambda ([x : Tx]) : T1
   (+ x 3))
 5)

In this notation, type variables are used to indicate our lack of knowledge of the actual types. Our objective is to infer the value of the type variables Tx and T1.

In addition, we also want to type check the whole expression and verify that every node in the AST can be assigned a consistent type.
Therefore, we also introduce type variables for the nodes in the expression:

Given these 5 type variables: Tx, T1, Tapp, Tproc and T+, we derive type constraints (equations) by inspecting the syntactic type of each expression and applying typing rules to each node:

Tproc = [Tx -> T1] // By the procedure-typing rule #1
T1 = T+  // By the procedure-typing rule - the return type of the procedure is that of the last exp in the body #2

These two constraints are derived from the procedure-typing rule which we introduced in the previous lecture:

Typing rule Procedure :
For every: type environment _Tenv,
           variables _x1, ..., _xn, n >= 0 (the parameters of the procedure)
           expressions _e1, ..., _em, m >= 1, (the body of the procedure)
           type expressions _S1, ...,_Sn, _U1, ...,_Um :

Procedure with parameters (n > 0):
    If   _Tenv o {_x1:_S1, ..., _xn:_Sn } |- _ei:_Ui for all i = 1..m ,
    Then _Tenv |- (lambda (_x1 ... _xn ) _e1 ... _em) : [_S1 * ... * _Sn -> _Um]

Parameter-less Procedure (n = 0):
    If   _Tenv |- _ei:_Ui for all i=1..m,
    Then _Tenv |- (lambda () _e1 ... _em) : [Empty -> _Um]

In our case, we consider the procedure (lambda ([x : Tx] : T1 (+ x 3)) and we have named the type of the application (+ x 3) T+.

The procedure typing rule mandates that:

In general, we derive 2 constraints from each procedure node in the AST:

Observe that we did not explicitly take into account the Tenv extension specified in the rule when we derived type equations. Instead, we assigned a type variable to the variable declaration (Tx for the variable x in our case) - and in the continuation of the analysis, we assume that all occurrences of x have type Tx.

This assumption relies on the implicit assumption that all the bound variables in the program have been renamed to distinct names to avoid confusion.

We then consider the application expression and derive two more constraints:

Tapp = T1   // By the application-typing rule - T1 is the return type of the procedure
Tx = Number // By the application-typing rule - the arguments have the type of the formal parameters

We derive these constraints from the application typing rule:

Typing rule Application :
For every: type environment _Tenv,
           expressions _f, _e1, ..., _en, n >= 0 , and
           type expressions _S1, ..., _Sn, _S:

Procedure with parameters (n > 0):
    If   _Tenv |- _f : [_S1 * ... * _Sn -> _S],
         _Tenv |- _e1 : _S1, ..., _Tenv |- _en : _Sn
    Then _Tenv |- (_f _e1 ... _en) : _S

Parameter-less Procedure (n = 0):
    If   _Tenv |- _f : [Empty -> _S]
    Then _Tenv |- (_f) : _S

In our case, we apply a procedure of type Tproc = [Tx -> T1] to the parameter 5 of type Number. The rule mandates that:

In general, typing an application expression creates n+1 equations - one for each formal parameter ei and one for the type of the whole application.

Finally, we consider the primitive application expression (+ x 3) and derive three constraints:

T+ = Number         // By the primitive-application rule for +: (Number * Number -> Number)
Tx = Number
typeof(3) = Number

In general, we derive n+1 type equations for every primitive application analysis: one for each of the n parameters (our primitives so far have either 1 or 2 parameters) and one for the return type of the primitive application.

Observe how primitive expressions produce extremely rich constraints - they are supremely informative. This is because primitives in our language are strongly typed - they expect a single type for their parameter and produce a single type.

Primitives in JavaScript are much less informative, because they accept variables of many types and can return many types as well.

We then solve this system of equations by systematic inspection and susbstitution across all equations when we find the value of a type variable.

We have thus derived the type of the overall expression.
In addition, we have inferred the type of the variables Tx and T1 and can thus provide a fully annotated version of the program:

((lambda ([x : Number]) : Number
   (+ x 3))
 5)

Type Inference: Example 2

Let us type the following expression - which computes the derivative of the function g with resolution gx:

(lambda (g dx)
  (lambda (x)
    (/ (- (g (+ x dx)) (g x))
       dx)))

We consider this equation as an AST where all variable declarations have optional type annotations which are not provided. We view this expression as if it had been provided as follows:

(lambda ([g : Tg] [dx : Tdx]) : T1
  (lambda ([x : Tx]) : T2
    (/ (- (g (+ x dx)) (g x))
       dx)))

Our objective is to infer the value of the type variables Tg, Tdx, T1, Tx and T2.

In addition, we also want to type check the whole expression and verify that every node in the AST can be assigned a consistent type. Therefore, we also introduce type variables for the nodes in the expression:

Given these 12 type variables: Tg, Tdx, T1, Tx, T2 and Tproc1, Tproc2, Tdiv, T-, Tg1, T+, Tg2, we derive type constraints (equations) by inspecting the syntactic type of each expression and applying typing rules to each node:

Tproc1 = [Tg * Tdx -> T1]   // By the procedure-typing rule
T1 = Tproc2                 // By the procedure-typing rule: 
                            // the type of the last exp in body is the return type of the proc

Tproc2 = [Tx -> T2] // By the procedure-typing rule 
T2 = Tdiv           // By the procedure-typing rule: type of body

Tdiv = Number  // By the primitive application typing rule for /
T- = Number
Tdx = Number

T- = Number    // By the primitive application typing rule for -
Tg1 = Number
Tg2 = Number

Tg = [T+ -> Tg1]  // By the application typing rule on application g1
T+ = T+

T+ = Number     // By the primitive application typing rule for +
Tx = Number
Tdx = Number

Tg = [Tx -> Tg2]  // By the application typing rule on application g2
Tx = Tx

We then solve this system of equations by systematic inspection and susbstitution across all equations when we find the value of a type variable.

By substituting Tg2 and Tx with their values, we find:

Tg = [Number -> Number]

By substituting Tdiv - we get T2 = Number, then Tproc2 = [Number -> Number], then T1 = [Number -> Number] and eventually:

Tproc1 = [[Number -> Number] * Number -> [Number -> Number]]

This is the expected type for the derivative function, which given a numeric function and a resolution, returns a new numeric function.

In addition, we can provide the fully annotated version of the program:

(lambda ([g : [Number -> Number] [dx : Number]) : [Number -> Number]
  (lambda ([x : Number]) : Number
    (/ (- (g (+ x dx)) (g x))
       dx)))

Type Inference: Example 3

Let us type this expression:

(let ((x 1)) 
  (lambda (f y)
    (f (+ x y)))

We consider this equation as an AST where all variable declarations have optional type annotations which are not provided. We view this expression as if it had been provided as follows:

(let (([x : Tx] 1)) 
  (lambda ([f : Tf] [y : Ty]) : Tres
    (f (+ x y)))

Our objective is to infer the value of the type variables Tx, Tf, Ty and Tproc. In addition, we also want to type check the whole expression and verify that every node in the AST can be assigned a consistent type.
Therefore, we also introduce type variables for the nodes in the expression:

Given these 8 type variables: Tx, Tf, Ty, Tres, Tlet, Tproc, Tapp, T+, we derive type constraints (equations) by inspecting the syntactic type of each expression and applying typing rules to each node:

Tx = Number   // By the let-typing rule - binding of the variable x to a number
Tlet = Tproc  // By the let-typing rule - the type of the let-exp is that of the last exp in body.

We use here the let-typing rule, which combines the type constraints of procedure definition and application:

Typing rule Let :
For every: type environment _Tenv,
           n >= 0 and m > 0,
           variables _x1, ..., _xn, (the variables of the bindings in the let-exp)
           expressions _e1, ..., _en, (the values of the bindings in the let-exp)
           expressions _b1, ..., _bm, (the body of the let-exp)
           type expressions _S1, ...,_Sn, _U1, ...,_Um :

If   _Tenv o {_x1 : _S1, ..., _xn : _Sn } |- _bi : _Ui for all i = 1..m
     _Tenv |- _ei : _Si for all i = 1..n
Then _Tenv |- (let ((_x1 _e) ... (_xn _en)) _b1 ... _bm) : _Um

In general, applying the let-typing rule yields n+1 constraints, one for each binding in the let, and one for the type of the body being equal to the type of the whole let-expression.

Tres = Tapp               // By the procedure-typing rule
Tproc = [Tf * Ty -> Tapp] // By the procedure typing rule

Tf = [T+ -> Tapp]         // By the application typing rule

Tx = Number   // By the primitive-application + rule
Ty = Number   // By the primitive-application + rule
T+ = Number   // By the primitive-application + rule

We then solve this system of equations by systematic inspection and susbstitution across all equations when we find the value of a type variable.

By substituting T+ with its value, we find:

Tf = [Number -> Tapp]

Then, by substituting Tf and Ty by their value:

Tproc = [[Number -> Tapp] * Number -> Tapp]

We eventually infer that Tlet = [[Number -> Tapp] * Number -> Tapp].

We also have inferred the type of all the variables which appear in the annotations and can fill the annotations as follows:

(let (([x : number] 1)) 
  (lambda ([f : [Number -> Tapp]] [y : Number]) : Tapp
    (f (+ x y)))

We observe that the resulting type for Tlet includes type variables.
This is because this expression is polymorphic - we can compute this program for any type Tapp and ensure that no typing error will be met.

Type Inference: Example 4

We want to type the procedure (lambda (f x) (f x x)) using type equations.

We consider this equation as an AST where all variable declarations have optional type annotations which are not provided. We view this expression as if it had been provided as follows:

(lambda ([f : Tf] [x : Tx]) : Tres (f x x))

Our objective is to infer the value of the type variables Tf and Tx. In addition, we also want to type check the whole expression and verify that every node in the AST can be assigned a consistent type. Therefore, we also introduce type variables for the application node (f x x) (Tapp) and for the overall procedure (lambda (f x) (f x x)) (Tproc).

Given these 4 type variables: Tf, Tx, Tapp, Tproc, we derive type constraints (equations) by inspecting the syntactic type of each expression and applying typing rules to each node:

Tf = [Tx * Tx -> Tapp]     // By the application typing rule
Tproc = [Tf * Tx -> Tres]  // By the procedure typing rule
Tres = Tapp                // By the procedure typing rule

Crucially, the same variables appear in the two equations. Our objective is to find a solution which assigns a value to the variables to make the whole system consistent. Alternatively, if there is a problem in the type of the expressions, we must detect the conflict.

Our solution consists of inspecting each equation, and to try to make the two sides of the equation equal by applying consistent substitution on both sides (this approach is quite similar to the way we solve algebraic equations).

In our case, the solution is provided by replacing Tf by its value in the right-hand side of the second equation, yielding:

Tproc = [[Tx * Tx -> Tapp] * Tx -> Tapp].

In addition, we have inferred the required types for all variables in the expression, and can produce the fully annotated version:

(lambda ([f : [Tx * Tx -> Tapp]] [x : Tx]) : [[Tx * Tx -> Tapp] * Tx -> Tapp]
  (f x x))

We observe that the resulting expression still contains type variables (Tx and Tapp). This is ok - it means the procedure we have typed is polymorphic - it can work on any type pairs (Tx, Tapp) and still be executed without leading to a typing error.

Type Inference: Example 5

Let us now consider a case where type inference fails:

(lambda (x) (x x))

The annotated AST is:

(lambda ([x : Tx]) : T1 (x x))

The additional type variables are:

We derive type equations:

Tproc = [Tx -> T1]   // By the procedure-typing rule (shape of the procedure type)
T1 = Tapp            // By the procedure typing rule (type of the last exp in the body)

Tx = [Tx -> Tapp]    // By the application-typing rule on (x x) (type of rator)
Tx = Tx              // By the application-typing rule on (x x) (type of rand)

There is no solution to this system of equations - because we cannot solve the constraint:

Tx = [Tx -> Tapp]

Type Inference Algorithm using Type Equations

Let us now present the algorithm which performs type inference by constructing and solving type equations.

Type equation solvers use the unification algorithm for unifying type expressions and producing a consistent substitution of type variables which makes all equations equal.

The method has four stages:

  1. Rename bound variables in e.
  2. Assign type variables to all sub-expressions.
  3. Construct type equations.
  4. Solve the equations.

Type Substitutions and Unifiers

In order to describe the process of type equations more formal, we introduce the definition of type substitutions and unifiers. The notions of substitutions and renaming we will use are identical to those we introduced when describing the operational semantics of the language.
The notion of unifier builds on those.

Definition: Type Substitution

A type-substitution s is a mapping from a finite set of type variables to a finite set of type expressions, such that s(T) does not include T. A type-binding is a pair T; s(T).

Substitutions are written using set notions: {T1=Number, T2=[[Number->T3]->T3]}.

{T1=Number, T2=[[Number->T3]->T2]} is an illegal substitution because T2 occurs in s(T2).

Definition: Substitution Application

The application of a type-substitution s to a type expression T, denoted T o s (or just Ts), consistently replaces all occurrences of type variables Ti in T by their mapped type expressions s(Ti). The replacement is simultaneous.

Example:

[[T1->T2]->T2] o {T1=Boolean, T2=[T3->T3]} = [[Boolean->[T3->T3]] -> [T3->T3]]

Definition: Type Instance, More General Relation

We say that a type expression T' is an instance of a type expression T, if there is a type substitution s such that T o s = T'.

T is more general than T', if T' is an instance of T.

The following type expressions are instances of [T -> T]:

[Number -> Number] = [T->T] o {T = Number}
[Symbol -> Symbol] = [T->T] o {T = Symbol}
[[Number->Number] -> [Number->Number]] = [T->T] o {T = [Number->Number]}
[[Number->T1] -> [Number->T1]] = [T->T] o {T = [Number->T1]}

Definition: Combination (composition) of Type Substitutions

The combination of type-substitutions s and s', denoted s o s', is an operation that results in a type-substitution, or fails.

It is defined by:

  1. s' is applied to the type-expressions of s, i.e., for every variable T' for which s'(T') is defined, occurrences of T' in type expressions in s are replaced by s'(T').
  2. A variable T' in s', for which s(T) is defined, is removed from the domain of s', i.e., s'(T) is not defined on it anymore.
  3. The modified s' is added to s.
  4. Identity bindings, i.e., s(T) = T, are removed.
  5. If for some variable, (s o s')(T) includes T, the combination fails.

For example,

{T1=Number, T2=[[Number->T3] -> T3]} o {T3=Boolean, T1=[T2->T2]} =
{T1 = Number, T2 = [[Number->Boolean]->Boolean], T3=Boolean}

Definition: Renaming of Type Variables

Renaming is the operation of consistent renaming of type variables within a type expression, by new type symbols, that do not occur in the type expression.

Renamed type expressions are equivalent:

[[T1 -> T2]*T1 -> T2] ~ [[S1 -> T2] * S1 -> T2]
[[T1 -> T2]*T1 -> T2] ~ [[S1 -> S2] * S1 -> S2]

The variables in the substituting expressions should be new. For example, the following renamings of [[T1->T2]*T1 -> T2] are illegal:

[[T1 -> T2] * S2 -> T2]   // T1 is not consistently replaced - T1 and S2 are not kept together
[[T2 -> T2] * T2 -> T2]   // T2 is reused to replace T1

Definition: Unification of Type Expressions

Unification is an operation that makes type expressions identical by application of a type substitution to both expressions. When such a subtitution can be found, it is called a unifier of the two type expressions.

For example:

[S * [Number -> S] -> S]   o {S=Pair(T1), T2=[Number->S], T3=Pair(T1)} =
[Pair(T1) * T2 -> T3]      o {S=Pair(T1), T2=[Number->S], T3=Pair(T1)} =

[Pair(T1)*[Number->Pair(T1)]->Pair(T1)]

Therefore, {S=Pair(T1), T2=[Number->S], T3=Pair(T1)} is a unifier for these type expressions.

Definition: Unifier of Type Expressions

A unifier of type expressions T1; T2 is a type substitution s such that T1 o s = T2 o s.

The type expressions should not include common type variables! (Apply renaming, if needed.)

Example: Unification of Type Expressions

Consider the type expressions:

[S * [Number -> S1] -> S] and
[Pair(T1) * [T1 -> T1] -> T2]

are unifiable by:

{S = Pair(Number), T1 = Number, S1 = Number, T2 = Pair(Number)}

[S * [Number -> S] -> S] and
[Pair(T1) * [T1 -> T1] -> T2]

are not unifiable - because we would need to resolve (find a substitution which leads to the equality):

S = Pair(T1) and
S = T2 and
[Number -> S] = [T1 -> T1]

hence S = T1

which is not compatible with T1 = Pair(T1)

Definition: Most General Unifier (mgu)

Unifiable type expressions can be unified by multiple unifiers.

For example, the type expressions [S * S -> S] and [Pair(T1) * T2 -> T2] are unifiable by the unifiers:

  1. {S=Pair(T1), T2=Pair(T1)}
  2. {S=Pair(Number), T2=Pair(Number)}
  3. {S=Pair(Boolean), T2=Pair(Boolean)}, etc

The first unifier is the most general unifier (mgu), since it substitutes only the necessary type variables, without making additional assumptions about the replaced terms. All other unifiers are obtained from it by application of additional substitutions. The most general unifier is unique, up to consistent renaming. It is called the most general unifier (mgu) of the two type expressions.

We will use in the type inference algorithm the function unify(TE1, TE2) which returns the mgu of TE1 and TE2 if it can be found and false otherwise (indicating the two expressions cannot be unified).

Type Inference With Equations Step by Step

With the unification tool at our disposal, let us run the full details of the type inference algorithm step by step:

We want to type the following expression:

(lambda (f g)
  (lambda (x)
    (f (+ x (g 3)))))

We consider it with its type annotations:

(lambda ([f : Tf] [g : Tg]) : T1
  (lambda ([x : Tx]) : T2
    (f (+ x (g 3)))))

Stage I: Renaming :

None needed because all declared variables already have distinct names.

Stage II: Assign type variables: Every sub expression is assigned a type variable

Expression                                    Variable
(lambda (f g) (lambda (x) (f (+ x (g 3)))))   T0
(lambda (x) (f (+ x (g 3))))                  T1
(f (+ x (g 3)))                               T2
f                                             Tf
(+ x (g 3))                                   T3
+                                             T+
x                                             Tx
(g 3)                                         T4
g                                             Tg
3                                             Tnum3

Stage III: Construct type equations

The typing rules of algorithm Type-derivation turn into type equations: The rules are:

  1. Number, Boolean, Symbol, Primitive-procedures: Construct equations using their types.

For example, for the number 3: Tnum3 = Number and for the binary primitive procedure +: T+ = [Number * Number -> Number].

  1. Procedure (Lambda expressions):

The type inference rule is:

For every: type environment _Tenv,
           variables _x1, ..., _xn, n >= 0
           expressions _e1, ..., _em, m >= 1, and
           type expressions _S1, ...,_Sn, _U1, ...,_Um :
Procedure with parameters (n > 0):
    If   _Tenv o {_x1:_S1, ..., _xn:_Sn } |- _ei : _Ui for all i = 1..m ,
    Then _Tenv |- (lambda (_x1 ... _xn ) _e1 ... _em) : [_S1 * ... *_Sn -> _Um]

Parameter-less Procedure (n = 0):
    If   _Tenv |- _ei : _Ui for all i=1..m,
    Then _Tenv |- (lambda ( ) _e1 ... _em) : [Empty -> _Um]

Extracting the type restriction on the involved sub-expressions yields:

For (lambda (v1 ...vn) e1 ... em) with n > 0, construct the equation:

T(lambda(v1...vn) e1...em) = [Tv1 * ... * Tvn -> Tem].

For (lambda ( ) e1 ... em), construct the equation:

T(lambda() e1...em) = [Empty -> Tem].
  1. Application: The type-inference rule is:
For every: type environment _Tenv,
           expressions _f, _e1, ..., _en, n >= 0 , and
           type expressions _S1, ..., _Sn, _S:
Procedure with parameters (n > 0):
    If   _Tenv |- _f : [_S1 * ... * _Sn -> _S],
         _Tenv |- _e1 : _S1, ..., _Tenv |- _en : _Sn
    Then _Tenv |- (_f _e1 ... _en) : _S

Parameter-less Procedure (n = 0):
    If _Tenv |- _f:[Empty -> _S]
    Then _Tenv |- (_f):_S

Extracting the type restriction on the involved sub-expressions yields:

For (f e1 ... en) with n > 0, construct the equation:
Tf = [Te1 * ... * Ten -> T].

For (f) construct the equation:
Tf = [Empty -> T(f)].

Note: Observe that the inference rules for Procedure and Application require type inference for all internal expressions, even though the final inferred type does not depend on their type. Why?

In the type-equations approach this requirement is achieved by constructing type equations for all sub-expressions, as described below. The algorithm constructs equations for the primitive sub-expressions and for all composite sub-expressions.

In our example:

The equations for the primitive sub-expressions are:

Expression       Equation
===============================================
3                Tnum3 = Number
+                T+ = Number * Number -> Number

The equations for composite sub-expressions are:

Expression                                    Equation
==================================================================
(lambda (f g) (lambda (x) (f (+ x (g 3)))))   T0 = [Tf * Tg -> T1]
(lambda (x) (f (+ x (g 3))))                  T1 = [Tx -> T2]
(f (+ x (g 3)))                               Tf = [T3 -> T2]
(+ x (g 3))                                   T+ = [Tx * T4 -> T3]
(g 3)                                         Tg = [Tnum3 -> T4]

Stage IV: Solving the Equations

The equations are solved by gradually producing type-substitutions for all type variables. For an expression e, the algorithm infers a type t if the final type-substitution maps its variable Te to t. If an expression has an infered type then all of its sub-expressions have types as well. If the procedure fails (output is FAIL) then either there is a type error or the constructed type equations are too weak.

Circular type-substitution cause failure.

The solution is processed by considering the equations one by one.

The equation solving process is described by this algorithm:

Input:  A set of type equations.
Output: A type substitution of FAIL.

Initialization:
  substitution := { }
  Order the set of input equations in any sequential order.
  equation := te1 = te2, the first equation.

Loop:
  1. Apply the current substitution to the equation: 
     equation := <te1 o substitution = te2 o substitution>
  
  2. If [te1 o substitution] and [te2 o substitution] are atomic types:
        if [te1 o substitution] != [te2 o substitution]: 
            substitution := FAIL
        otherwise: 
            Do nothing.
  
  3. Without loss of generality:
     If [te1 o substitution] = T, i.e., a type variable, and [te1 o substitution] != [te2 o substitution]:
         substitution := substitution o {T = [te2 o substitution]}. 
         That is, apply the equation to substitution, and add the equation to the substitution. 
         If the application fails (circular mapping), substitution := FAIL.
  
  4. if [te1 o substitution] and [te2 o substitution] are composite types:
         if they have the same type constructor: 
             Split [te1 o substitution] and [te2 o substitution] into component type expressions, 
             Create equations for corresponding components, and 
             Add the new equations to the pool of equations.
         if they have different type constructors: substitution := FAIL

  5. Without loss of generality:
     if [te1 o substitution] is an atomic type and [te2 o substitution] is a composite type: 
         substitution := FAIL

  6. if there is a next equation: equation := next(equation)

until substitution = FAIL or
      there is no next equation.
      
Return: Substitution

This algorithm computes the unifier of all the equations into a single consistent type substitution.

In other words, each time we process an equation [Te1 = Te2], we make the two sides equal by finding their unifier and then apply the resulting unifier to the remaining equations and continue the process. The constraints flow from equation to equation because we re-use the same substitution across equations and, thus, propagate information from one equation to the next.

Let us continue our example applying this algorithm to solve the equations:

Equations                 substitution
=========================================
1. T0 = [Tf * Tg -> T1]   {}
2: T1 = [Tx -> T2]
3: Tf = [T3 -> T2]
4: T+ = [Tx * T4 -> T3]
5: Tg = [Tnum3 -> T4]
6: Tnum3 = Number
7: T+ = Number * Number -> Number

Equation 1 is processed by the case 3 of the algorithm - since one of its sides is a type variable (T0).

Equations                     substitution
2: T1 = [Tx -> T2]            {T0 = [Tf * Tg -> T1]}
3: Tf = [T3 -> T2]
4: T+ = [Tx * T4 -> T3]
5: Tg = [Tnum3 -> T4]
6: Tnum3 = Number
7: T+ = Number * Number -> Number

In the second iteration, we process the second equation, and again apply case 3 of the algorithm:

Equations                     substitution
3: Tf = [T3 -> T2]            {T0 = [Tf * Tg -> [Tx -> T2], 
4: T+ = [Tx * T4 -> T3]        T1 = [Tx -> T2]}
5: Tg = [Tnum3 -> T4]
6: Tnum3 = Number
7: T+ = Number * Number -> Number

Note how the substitution composition resulted in the transformation of the T1 argument by its value in the right hand side of T0 in the substitution.

Same case 3 for the third equation:

Equations                     substitution
4: T+ = [Tx * T4 -> T3]       {T0 = [[T3 -> T2] * Tg -> [Tx -> T2]], 
5: Tg = [Tnum3 -> T4]          T1 = [Tx -> T2], Tf = [T3 -> T2]}
6: Tnum3 = Number
7: T+ = Number * Number -> Number

Again case 3 for the 4th equation:

Equations                     substitution
5: Tg = [Tnum3 -> T4]         {T0 = [[T3 -> T2] * Tg -> [Tx -> T2]], 
                               T1 = [Tx -> T2], Tf = [T3 -> T2],
6: Tnum3 = Number              T+ = [Tx * T4 -> T3]}
7: T+ = Number * Number -> Number

One more case 3 for the 5th equation:

Equations                          substitution
6: Tnum3 = Number                  {T0 = [[T3 -> T2] * [Tnum3 -> T4] -> [Tx -> T2]],
7: T+ = Number * Number -> Number   T1 = [Tx -> T2], Tf = [T3 -> T2],
                                    T+ = [Tx * T4 -> T3],
                                    Tg = [Tnum3 -> T4]}

Equation 6:

Equations                          substitution
7: T+ = Number * Number -> Number  {T0 = [[T3 -> T2] * [Number -> T4] -> [Tx -> T2]],
                                    T1 = [Tx -> T2], Tf = [T3 -> T2],
                                    T+ = [Tx * T4 -> T3],
                                    Tg = [Number -> T4],
                                    Tnum3 = Number }

When processing Equation 7, we must solve:

[Tx * T4 -> T3] = [Number * Number -> Number]

This is case 4 of the algorithm - we split the two sides of the equation into components - because they have the same type constructor (proc-te) and yield the new equations:

Tx = Number
T4 = Number
T3 = Number

We eventually output the following substitution:

{T0 = [[Number -> T2] * [Number -> Number] -> [Number -> T2]],
 T1 = [Number -> T2], 
 Tf = [Number -> T2],
 T+ = [Number * Number -> Number],
 Tg = [Number -> Number],
 Tnum3 = Number,
 Tx = Number
 T4 = Number
 T3 = Number}

On the basis of this substitution, we can return the fully annotated expression:

(lambda ([f : Tf] [g : Tg]) : T1
  (lambda ([x : Tx]) : T2
    (f (+ x (g 3)))))

becomes:

(lambda ([f : [Number -> T2] [g : [Number -> Number]]) : [Number -> T2]
  (lambda ([x : Number]) : T2
    (f (+ x (g 3)))))