Type Inference System

PPL 2021

In the previous lecture, we have introduced the Type Equations algorithm to perform Type Inference over Scheme (\(L5\)) expressions.

In this lecture, we present two distinct implementations of this algorithm - one which is a “literal” application of the algorithm, and one which is an optimized transformation of the algorithm relying on more compact data structures and less traversals of the program.

Architecture of the Type Equations Inference System

The Type Inference with Type Equations system builds on the L5 AST abstract syntax defined for the Type Checker. It introduces two new modules:

The Substitution ADT

The Substitution ADT is a direct implementation of the mathematical substitution object introduced in the previous lecture, adjusted to work on type variables and type expressions.

Type Substitution Definition

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\).

As usual, when defining substitutions and partial functions (we have already implemented such data structures when talking about environments), we adopt an inductive implementation to define the Type Substitution data type, which is the union of two disjoint types:

The functional interface of the Substitution data type includes:

Both the functions sub(tvars, texps) and subCombine(sub1, sub2) return a non-empty substitution. They also enforce the key invariant of substitutions: for any variable \(T\), \(sub(T)\) does not include \(T\).

This invariant check is performed by the function checkNoOccurrence(tvar, texp). This function is a standard AST traversal of the Type expression Texp looking for any instance of the Type variable Tvar at any level.

This process is called occurrence check and is central to all unification based methods. It is a computationally expensive component of the algorithm.

// Purpose: when attempting to bind tvar to te in a sub - check whether tvar occurs in te.
// Return error if a circular reference is found.
export const checkNoOccurrence = (tvar: TVar, te: TExp): Result<true> => {
    const check = (e: TExp): Result<true> =>
        isTVar(e) ? ((e.var === tvar.var) ? 
                       bind(unparseTExp(te), 
                            up => makeFailure(`Occur check error - circular sub ${tvar.var} in ${up}`)) : 
                       makeOk(true)) :
        isAtomicTExp(e) ? makeOk(true) :
        isProcTExp(e) ? bind(mapResult(check, e.paramTEs), _ => check(e.returnTE)) :
        makeFailure(`Bad type expression ${e} in ${te}`);
    return check(te);
};

Similarly to environments, we define the non-empty substitution as a linked-list of bindings mapping variables to values. This value type is computed using the extend-sub(sub,tvar,texp) method. Note that the method requires two “complications” in addition to extending the base-substitution with the new binding:

  1. The existing right-hand-side of the base substitutions are updated with the new substitution (var->te)
  2. We perform occur check on the resulting substitution (by invoking make-sub which includes an occur-check).
// Purpose: extend a substitution with one pair (tv, te)
// Calls to makeSub to do the occur-check
export const extendSub = (sub: Sub, v: TVar, te: TExp): Result<Sub> =>
    bind(makeSub([v], [te]), (sub2: Sub) => {
        const updatedTEs = map((te) => applySub(sub2, te), sub.tes);
        return includes(v.var, map(prop('var'), sub.vars)) ? makeSub(sub.vars, updatedTEs) :
               makeSub(cons(v, sub.vars), cons(te, updatedTEs));
    });

In addition, we explicitly “compile” extended substitutions which are the result of composing two substitutions into a flat representation, using the value constructor subCombine. Recall that substitution composition is defined as:

This method is implemented literally in the subCombine(sub1, sub2) procedure - which has a structure similar to a reduce of the extendSub operation over all the pairs in sub2:

// ============================================================
// Purpose: Returns the composition of substitutions s.t.:
//  applySub(result, te) === applySub(sub2, applySub(sub1, te))
// The composition fails if it would lead to a circular substitution.
export const combineSub = (sub1: Sub, sub2: Sub): Result<Sub> =>
    isEmptySub(sub1) ? makeOk(sub2) :
    isEmptySub(sub2) ? makeOk(sub1) :
    combine(sub1, sub2.vars, sub2.tes);

const combine = (sub: Sub, vars: TVar[], tes: TExp[]): Result<Sub> =>
    isEmpty(vars) ? makeOk(sub) :
    bind(extendSub(sub, first(vars), first(tes)), 
         (extSub: Sub) => combine(extSub, rest(vars), rest(tes)));

Type Equations Module

The type equations module follows the definition of the algorithm:

Renaming of all bound variables in e is performed in the same way as we introduced when discussing the Substitution model for Operational Semantics. We do not repeat this code here, and instead make the assumption that in the following, all bound variables have distinct names (the same variable name is never used twice in different scopes).

We implement the assignment of type variables to all sub-expressions by defining a data structure which we call the pool which contains a list of pairs (exp Tvar) for every node in the expression AST.

The pool is a list of pairs (expression-AST-node, type variable) which exhaustively includes all the sub-expressions in the AST. It is built using the function expToPool. As usual, this function is an AST traversal method. Whenever a node in the AST is visited, we allocate a fresh Type Variable for it.

Pay attention to the way variable declarations and variable references are processed when constructing the pool.

When we continue the traversal of the AST, and we later meet a VarRef node which refers to this VarDecl node, we want to associate it to the existing VarDecl type declaration (whether it is provided by the programmer or allocated by the parser).

To achieve this mechanism, when we meet a var-decl node, we use the procedure extendPoolVarDecl(varDecl, pool) which adds the pair (varRef(varDecl.var) varDecl.texp)) to the pool. When we later reach a VarRef in the scope of this VarDecl, we find that the pair (VarRef tvar) already exists in the pool, and we do not allocate any new fresh type variable for it.

This mechanism crucially depends on the fact that expToPool traverses the expression ADT top-down (traverse the VarDecl before the corresponding VarRef nodes are met) and the expression has been renamed before so that all VarRefs with a given name refer to the single VarDecl with the same name.

expToPool uses the function reducePool to accumulate the pairs (AST-node TVar) into the pool without repetitions. This function is a variant of the reduce family of higher-order functions.

Optional<T> and maybe

We use in these functions the inPool function which checks whether an expression is already present in the pool. In case the expression is found, we return the associated TExp, else we need to return a value that indicates the expression was not found. This is a typical situation where we have a search operator which can fail. We adopt the standard Optional generic type to represent this return type in a type-safe manner. In the same way as Result represents a call which may fail, Optional represents a call which may either return a value or the legitimate case of a missing value (which should not be considered an error). The two options are wrapped as Some<T> and None (parallel to Ok<T> and Failure for Result<T>). To manipulate Optional values, we use the maybe operator which passes the Optional<T> two possible continuations: a method receiving a T value in case the value was found, and one receiving no argument in case none was found. maybe belongs to the family of fold operators in functional programming: it is used to reduce a data structure containing multiple values into a single one (in the case of product-like types like arrays, reduce belongs to the fold family; in the case of sum-like types (unions) like Result or Option, a fold-operator provides one procedure for each case - as in the maybe operator).

We also implement a bind versions for Optional<T> values with the same behavior as that we adopted for Result<T>.

// Purpose: construct a pool with one additional pair
//          [exp, fresh-tvar]
// @Pre: exp is not already in pool.
export const extendPool = (exp: A.Exp, pool: Pool): Pool =>
    cons({e: exp, te: T.makeFreshTVar()}, pool);

// Purpose: construct a pool with one additional pair
//          [VarRef(var), texp]
//          from a VarDecl(var, texp) declaration.
// @Pre: var is not already in pool - which means
// that all bound variables have been renamed with distinct names.
const extendPoolVarDecl = (vd: A.VarDecl, pool: Pool): Pool =>
    cons({e: A.makeVarRef(vd.var), te: vd.texp}, pool);

export const inPool = (pool: Pool, e: A.Exp): Opt.Optional<T.TExp> => {
    const exp = R.find(R.propEq('e', e), pool);
    return exp ? Opt.makeSome(R.prop('te')(exp)) : Opt.makeNone();
}

// Map a function over a list of expressions to accumulate
// matching sub-expressions into a pool.
// fun should construct a new pool given a new expression from exp-list
// that has not yet been seen before.
const reducePool = (fun: (e: A.Exp, pool: Pool) => Pool, exps: A.Exp[], result: Pool): Pool =>
    isEmpty(exps) ? result :
    Opt.maybe(inPool(result, first(exps)),
              _ => reducePool(fun, rest(exps), result),
              () => reducePool(fun, rest(exps), fun(first(exps), result)));

const reducePoolVarDecls = (fun: (e: A.VarDecl, pool: Pool) => Pool, vds: A.VarDecl[], result: Pool): Pool =>
    isEmpty(vds) ? result :
    Opt.maybe(inPool(result, A.makeVarRef(first(vds).var)),
              _ => reducePoolVarDecls(fun, rest(vds), result),
              () => reducePoolVarDecls(fun, rest(vds), fun(first(vds), result)));

// Purpose: Traverse the abstract syntax tree L5-exp
//          and collect all sub-expressions into a Pool of fresh type variables.
// Example:
// bind(bind(p('(+ x 1)'), parseL5Exp), e => makeOk(TE.expToPool(e))) =>
// Ok([[AppExp(PrimOp(+), [VarRef(x), NumExp(1)]), TVar(16)],
//     [NumExp(1), TVar(15)],
//     [VarRef(x), TVar(14)],
//     [PrimOp(+), TVar(13)]])
export const expToPool = (exp: A.Exp): Pool => {
    const findVars = (e: A.Exp, pool: Pool): Pool =>
        A.isAtomicExp(e) ? extendPool(e, pool) :
        A.isProcExp(e) ? extendPool(e, reducePool(findVars, e.body, 
                                    reducePoolVarDecls(extendPoolVarDecl, e.args, pool))) :
        A.isCompoundExp(e) ? extendPool(e, reducePool(findVars, A.expComponents(e), pool)) :
        makeEmptyPool();
    return findVars(exp, makeEmptyPool());
};

The post-condition met at the end of the pool construction is that every node in the AST is mapped to a type variable - while preserving scoping relations (different occurrences of the same varRef are all merged as a single pair mapping the varRef to its declared type - which can be a non-instantiated type variable).

Equations Generation

The next step of the algorithm consists of transforming the pool of {e:expression, te:TVar} pairs into a set of equations. This part of the algorithm is the one that encapsulates the semantics of the type system used in the programming language.

The procedure poolToequations performs this mapping. This procedure accumulates the transformation of all pairs {e:exp, te:Tvar} in the pool to equations. The equation ADT is a pair left-hand-side / right-hand-side of type expressions (that is, each equation is encoded as a pair {left: TExp, right: TExp}).

The heart of the typing algorithm is the operation makeEquationsFromExp which covers the typing rules of the programming language. This implements the typing rules for procedure expressions, application expressions and atomic expressions. For example, given a pair ( application-exp, TVar ), the procedure derives a type equation which mandates that the type variable associated to the operator of the application must be made equal to the type expression (T1 * ... * Tn -> TVar) where Ti is the type variable associated to the ith argument of the application expression.

For the base cases of atomic types and primitive operators, we reuse the procedures typeof-bool-exp, typeof-num-exp and typeof-prim-op which we defined in the type checker.

Observe that there is no processing of if-exp - do you understand why?

// Signature: make-equation-from-exp(exp, pool)
// Purpose: Return a single equation
// @Pre: exp is a member of pool
export const makeEquationsFromExp = (exp: A.Exp, pool: Pool): Opt.Optional<Equation[]> =>
    // An application must respect the type of its operator
    // Type(Operator) = [T1 * .. * Tn -> Te]
    // Type(Application) = Te
    A.isAppExp(exp) ? Opt.bind(inPool(pool, exp.rator), (rator: T.TExp) =>
                        Opt.bind(Opt.mapOptional((e) => inPool(pool, e), exp.rands), (rands: T.TExp[]) =>
                            Opt.mapv(inPool(pool, exp), (e: T.TExp) => 
                                [makeEquation(rator, T.makeProcTExp(rands, e))]))) :
    // The type of procedure is (T1 * ... * Tn -> Te)
    // where Te is the type of the last exp in the body of the proc.
    // and   Ti is the type of each of the parameters.
    // No need to traverse the other body expressions - they will be
    // traversed by the overall loop of pool->equations
    A.isProcExp(exp) ? Opt.bind(inPool(pool, exp), (left: T.TExp) =>
                            Opt.mapv(Opt.bind(safeLast(exp.body), (last: A.CExp) => inPool(pool, last)), (ret: T.TExp) =>
                                [makeEquation(left, T.makeProcTExp(R.map((vd) => vd. texp, exp.args), ret))])) :
    // The type of a number is Number
    A.isNumExp(exp) ? Opt.mapv(inPool(pool, exp), (left: T.TExp) => [makeEquation(left, T.makeNumTExp())]) :
    // The type of a boolean is Boolean
    A.isBoolExp(exp) ? Opt.mapv(inPool(pool, exp), (left: T.TExp) => [makeEquation(left, T.makeBoolTExp())]) :
    // The type of a string is String
    A.isStrExp(exp) ? Opt.mapv(inPool(pool, exp), (left: T.TExp) => [makeEquation(left, T.makeStrTExp())]) :
    // The type of a primitive procedure is given by the primitive.
    A.isPrimOp(exp) ? Opt.bind(inPool(pool, exp), (left: T.TExp) =>
                            Opt.mapv(Res.resultToOptional(TC.typeofPrim(exp)), (right: T.TExp) =>
                                [makeEquation(left, right)])) :
    // Todo: define, let, letrec, set 
    Opt.makeNone();

Solving the Type Equations System

The last stage of the algorithm consists of solving the set of equations collected by the equations generator. The procedure solve(equations, substitution) is a direct implementation of the solve algorithm presented in the last lecture. It computes the unifier of all the equations - that is, it computes a type substitution which when it is applied to both sides of all the equations, makes the two sides identical.

This unifier substitution is computed incrementally, by processing each equation in turn.

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 is implemented in the following procedure:

export const solveEquations = (equations: Equation[]): Res.Result<S.Sub> =>
    solve(equations, S.makeEmptySub());

// Purpose: Solve the equations, starting from a given substitution.
//          Returns the resulting substitution, or error, if not solvable
const solve = (equations: Equation[], sub: S.Sub): Res.Result<S.Sub> => {
    const solveVarEq = (tvar: T.TVar, texp: T.TExp): Res.Result<S.Sub> =>
        Res.bind(S.extendSub(sub, tvar, texp), sub2 => solve(rest(equations), sub2));

    const bothSidesAtomic = (eq: Equation): boolean =>
        T.isAtomicTExp(eq.left) && T.isAtomicTExp(eq.right);

    const handleBothSidesAtomic = (eq: Equation): Res.Result<S.Sub> =>
        T.isAtomicTExp(eq.left) && T.isAtomicTExp(eq.right) && T.eqAtomicTExp(eq.left, eq.right)
        ? solve(rest(equations), sub)
        : Res.makeFailure(`Equation with non-equal atomic type ${eq}`);

    if (isEmpty(equations)) {
        return Res.makeOk(sub);
    }

    const eq = makeEquation(S.applySub(sub, first(equations).left),
                            S.applySub(sub, first(equations).right));

    return T.isTVar(eq.left) ? solveVarEq(eq.left, eq.right) :
           T.isTVar(eq.right) ? solveVarEq(eq.right, eq.left) :
           bothSidesAtomic(eq) ? handleBothSidesAtomic(eq) :
           T.isCompoundTExp(eq.left) && T.isCompoundTExp(eq.right) && canUnify(eq) ?
                solve(R.concat(rest(equations), splitEquation(eq)), sub) :
           Res.makeFailure(`Equation contains incompatible types ${eq}`);
};

The logic of the unification is implemented in the procedures canUnify and splitEquation. These procedures transform an equation of the form:

[T1 * ... * Tn -> T] = [U1 * ... * Un -> U]

into \(n+1\) equations of the form:

[T1 = U1]
...
[Tn = Un]
[T = U]

// Signature: canUnify(equation)
// Purpose: Compare the structure of the type expressions of the equation
const canUnify = (eq: Equation): boolean =>
    T.isProcTExp(eq.left) && T.isProcTExp(eq.right) &&
    (eq.left.paramTEs.length === eq.right.paramTEs.length);

// Signature: splitEquation(equation)
// Purpose: For an equation with unifyable type expressions,
//          create equations for corresponding components.
// Type: [Equation -> List(Equation)]
// Example: splitEquation(
//            makeEquation(parseTExp('(T1 -> T2)'),
//                         parseTExp('(T3 -> (T4 -> T4))')) =>
//            [ {left:T2, right: (T4 -> T4)},
//              {left:T3, right: T1)} ]
// @Pre: isCompoundExp(eq.left) && isCompoundExp(eq.right) && canUnify(eq)
const splitEquation = (eq: Equation): Equation[] =>
    (T.isProcTExp(eq.left) && T.isProcTExp(eq.right)) ?
        R.zipWith(makeEquation,
                  R.prepend(eq.left.returnTE, eq.left.paramTEs),
                  R.prepend(eq.right.returnTE, eq.right.paramTEs)) :
    [];

Solve Termination Argument

How do we know that the solve algorithm terminates given a list of type expression equations?

The main loop of the algorithm has for state the current list of equations and the current substitution.

Let us consider the effect of one iteration through the main loop:

The argument for completion is based on the characterization of the size of the input equation set as a pair \((D, N)\) where \(D\) is the maximum height of the ASTs that appear in any equation in the equation set and \(N\) is the number of equations in the set.

Each iteration in the loop changes the size to either \((D, N-1)\) or \((D-1, N+n)\). When \(D=1\), the transition is necessarily to \((1, N-1)\) because the only case where we add equations is for composite ASTs. Hence all transitions lead to the completion state of \((1, 0)\).

Putting all Steps Together: inferType

Putting all the steps of the algorithm together, we define the procedure infer and verifyType:

// ========================================================
// Purpose: Infer the type of an expression using the equations method
// Example: unparseTExp(inferType(parse('(lambda (f x) (f (f x)))')))
//          ==> '((T_1 -> T_1) * T_1 -> T_1)'
export const inferType = (exp: A.Exp): Opt.Optional<T.TExp> => {
    const pool = expToPool(exp);
    const equations = poolToEquations(pool);
    const sub = Opt.bind(equations, (eqns: Equation[]) => Res.resultToOptional(solveEquations(eqns)))
    const texp = inPool(pool, exp);
    return Opt.bind(sub, (sub: S.Sub) => 
             Opt.mapv(texp, (texp: T.TExp) => 
               T.isTVar(texp) ? S.subGet(sub, texp) : 
               texp));
};

// Type: [Concrete-Exp -> Concrete-TExp]
export const infer = (exp: string): Res.Result<string> =>
    Res.bind(A.parseL5Exp(exp),
             (exp: A.Exp) => Opt.maybe(inferType(exp),
                                       (te: T.TExp) => T.unparseTExp(te),
                                       () => Res.makeFailure("Infer type failed")));

This is invoked as follows:

> infer('(lambda (f g) (lambda (n) (f (g n))))')
{tag: 'Ok', ((T459051 -> T459052) * (T459049 -> T459051) -> (T459049 -> T459052))

Observe the usage of freshly generated type variable names which are different each time we invoke the procedure. This makes it difficult to test the procedure.

To resolve this difficulty, we introduce the procedure equivalentTEs? in TExp.ts which verifies that two type expressions are equivalent up to type variable renaming. This allows us to write tests in a deterministic manner (see test-helpers.ts):

export const verifyTeOfExprWithEquations = (exp: string, texp: string): Result<boolean> => {
    const e = bindResult(p(exp), parseL5Exp);
    const expectedType = parseTE(texp);
    const computedType = bindResult(e, (exp: Exp) => optionalToResult(inferType(exp), "Could not infer type"));
    return bindResult(computedType, (ct: TExp) =>
                mapv(expectedType, (et: TExp) => 
                    equivalentTEs(ct, et)));
};

This can be invoked as follows:

expect(verifyTeOfExprWithEquations("(lambda (x y) x)", "(T1 * T2 -> T1)")).toEqual(makeOk(true));

Type Inference with Direct Unification

The implementation described above based on type equations follows literally the type equations algorithm. It explicitly manipulates substitution data structures and type equations. In addition, it constructs a map of expression to type variables to ensure the exhaustive traversal of the program to be type-checked.

We present here an optimized version of this algorithm which relies on a slightly modified representation of the type variable data structure. Using this new data structure for type variables, we implement exactly the same algorithm but avoid creating explicit data structures for the pool, the equations and the substitutions. This leads to a more memory-efficient implementation, which also turns out to be more time efficient, as less traversals of the data structures are required, and operations performed eargerly in the type equations method are turned into lazy operations.

The complete code is available in L5-typeinference.ts.

Tests are in L5-typeinference.test.ts.

Type Variable with One-way Assignment

The extension to the TVar data type we introduce is implemented as follows:

// TVar: Type Variable with support for dereferencing (TVar -> TVar)
export type TVar = { tag: "TVar"; var: string; contents: Box<undefined | TExp>; };
export const isEmptyTVar = (x: any): x is TVar =>
    (x.tag === "TVar") && unbox(x.contents) === undefined;
export const makeTVar = (v: string): TVar =>
    ({tag: "TVar", var: v, contents: makeBox(undefined)});
export const isTVar = (x: any): x is TVar => x.tag === "TVar";
export const eqTVar = (tv1: TVar, tv2: TVar): boolean => tv1.var === tv2.var;

In addition to the name of the type variable, we associate a boxed value, initialized to undefined. We use this new field in the TVar datatype to associate the TVar to another type expression, when we derive a constraint that the variable must be bound to another type expression as part of the type inference process.

We extend the TVar data type with the following methods:

export const tvarContents = (tv: TVar): undefined | TExp => unbox(tv.contents);
// @Pre: tv is empty (one-way assignment)
export const tvarSetContents = (tv: TVar, val: TExp): void =>
    setBox(tv.contents, val);
export const tvarIsNonEmpty = (tv: TVar): boolean => tvarContents(tv) !== undefined;

The assignment managed by TVar is one-way - we can only assign a value to an empty type variable.

In many occurrences, we will bind a TVar to another TVar. When this is the case, we are interested in accessing the type expression to which the referenced TVar refers. That is, we create a graph of TVar references to other TVars which eventually lead to non-TVar expressions. We want to follow the path of references from any TVar to a non-TVar value (which may be empty).

The method VarDeref performs this graph traversal:

export const tvarDeref = (te: TExp): TExp => {
    if (! isTVar(te)) return te;
    const contents = tvarContents(te);
    if (contents === undefined)
        return te;
    else if (isTVar(contents))
        return tvarDeref(contents);
    else
        return contents;
}

Unification-based CheckTvarEqualType

Using the one-way assignment TVar data structure, we return to the procedure checkEqualType which we defined in the Type Checker implementation. The original implementation applied the invariance check and verified that two type expressions are identical (using the deepEqual predicate).
When they were, the type checker proceeded - otherwise the type checking failed.

In the case of the type inference, we replace this type equal test with a different procedure, which instead of testing that two types are equal, attempts to make them equal when they contain type variables. The way two type expressions are made equal is by unifying them - that is, finding a substitution which when applied to both sides makes them equal.

But instead of representing the substitution as an explicit data structure (the sub type we defined in L5-substitution-adt.ts, we encode the substitution bindings within the TVar data structure. When Tvar1 is bound to a type expression s(TVar1), we invoke tvarSetContents(tvar1, te).

The following procedure effectively computes the MGU (most general unifier) in-place given two expressions te1 and te2 which may contain type variables:

// Purpose: Make type expressions equivalent by deriving a unifier
// Return an error if the types are not unifiable.
// Exp is only passed for documentation purposes.
// te1 can be undefined when it is retrieved from a type variable which is not yet bound.
const checkEqualType = (te1: T.TExp | undefined, te2: T.TExp, exp: A.Exp): Result<true> =>
    te1 === undefined ? bind(T.unparseTExp(te2), (texp: string) => makeFailure(`Incompatible types: undefined - ${JSON.stringify(texp, null, 2)}`)) :
    T.isTVar(te1) && T.isTVar(te2) ? ((T.eqTVar(te1, te2) ? makeOk(true) : checkTVarEqualTypes(te1, te2, exp))) :
    T.isTVar(te1) ? checkTVarEqualTypes(te1, te2, exp) :
    T.isTVar(te2) ? checkTVarEqualTypes(te2, te1, exp) :
    T.isAtomicTExp(te1) && T.isAtomicTExp(te2) ?
        T.eqAtomicTExp(te1, te2) ? makeOk(true) : bind(T.unparseTExp(te1), (te1: string) =>
                                                    bind(T.unparseTExp(te2), (te2: string) =>
                                                        makeFailure<true>(`Incompatible atomic types ${te1} - ${te2}`))) :
    T.isProcTExp(te1) && T.isProcTExp(te2) ? checkProcEqualTypes(te1, te2, exp) :
    bind(T.unparseTExp(te1), (te1: string) =>
        bind(T.unparseTExp(te2), (te2: string) =>
            makeFailure<true>(`Incompatible types structure: ${te1} - ${te2}`)));

// Purpose: make two lists of equal length of type expressions equal
// Return an error if one of the pair of TExps are not compatible - true otherwise.
// Exp is only passed for documentation purposes.
const checkEqualTypes = (tes1: T.TExp[], tes2: T.TExp[], exp: A.Exp): Result<true> => {
    const checks = zipWithResult((te1, te2) => checkEqualType(te1, te2, exp), tes1, tes2);
    return bind(checks, _ => makeOk(true));
}

const checkProcEqualTypes = (te1: T.ProcTExp, te2: T.ProcTExp, exp: A.Exp): Result<true> =>
    te1.paramTEs.length !== te2.paramTEs.length ? bind(T.unparseTExp(te1), (te1: string) =>
                                                    bind(T.unparseTExp(te2), (te2: string) =>
                                                        makeFailure<true>(`Wrong number of args ${te1} - ${te2}`))) :
    checkEqualTypes(T.procTExpComponents(te1), T.procTExpComponents(te2), exp);

In exactly the same manner as we had to deal with the occur-check case in the substitution data type, we must also avoid creating circular references in the graph of TVar references. This is enforced in the checkTVarEqualTypes procedure which binds a TVar to a value - and makes sure the reference type expression does not include a reference to TVar:

// Purpose: check that a type variable matches a type expression
// Updates the var is needed to refer to te.
// Exp is only passed for documentation purposes.
const checkTVarEqualTypes = (tvar: T.TVar, te: T.TExp, exp: A.Exp): Result<true> =>
    T.tvarIsNonEmpty(tvar) ? checkEqualType(T.tvarContents(tvar), te, exp) :
    bind(checkNoOccurrence(tvar, te, exp), _ => { T.tvarSetContents(tvar, te); return makeOk(true); });


// Purpose: when attempting to bind tvar to te - check whether tvar occurs in te.
// Throws error if a circular reference is found.
// Exp is only passed for documentation purposes.
// Pre-conditions: Tvar is not bound
const checkNoOccurrence = (tvar: T.TVar, te: T.TExp, exp: A.Exp): Result<true> => {
    const checkList = (tes: T.TExp[]): Result<true> =>
        bind(mapResult(loop, tes), _ => makeOk(true));

    const loop = (te1: T.TExp): Result<true> =>
        T.isAtomicTExp(te1) ? makeOk(true) :
        T.isProcTExp(te1) ? checkList(T.procTExpComponents(te1)) :
        T.isTVar(te1) ? (T.eqTVar(te1, tvar) ? bind(A.unparse(exp), (exp: string) => makeFailure(`Occur check error - ${te1.var} - ${tvar.var} in ${exp}`)) : makeOk(true)) :
        bind(A.unparse(exp), (exp: string) => makeFailure(`Bad type expression - ${JSON.stringify(te1)} in ${exp}`));

    return loop(te);
}

Type Inference Algorithm

Surprisingly, the type inference algorithm is exactly the same code as the Type Checker - except for the transformation of the procedure checkEqualType from a test of equality to the unification building version presented above.

The program that we obtain is in fact an implementation of the type equation algorithm - with the following transformations:

The implementation of unification through one-way variable assignment is a powerful technique, which we will revisit in Chapter 5 when we survey Logic Programming.

Summary