Type inference is used in functional programming languages to automatically deduce the type of expressions based on how the expression is used. Inference reduces the burden on the programmer who would otherwise have to write all the types manually. Anyone who uses an imperative statically typed programming language knows how quickly explicit type annotations can become burdensome. Type inference is slowly permeating non-functional languages such as C++ and C#, which widens the potential use of inference.

Programming language designers are very interested in how type inference is implemented. Unfortunately the vast majority of the content on type inference is contained in academic publications from the 1990s and early 2000s. The implementation details have not yet made their way to the sphere of general public knowledge, which hinders further adoption by programming language designers. This blog post will present an overview of solving type inference problems by solving a system of constraints. The solver will be capable of solving constraints in a Hindley-Milner type system. The algorithm presented here is significantly simpler than Algorithm W, which is the classic method of type inference. Most of the resources on the Internet revolve around Algorithm W, which is not ideal.

Understanding Kinds

Understanding kinds is a critical prerequisite to understand how types are represented by type expressions. Just as expressions have a type signature, a type expression has a kind signature. In its most basic form, a kind tells us how we can construct a type. We represent kinds by using asterisks * and kind functions ->. The asterisk is pronounced as “type”. Here is how we will represent kinds in the constraint solver:

So we have a representation of kinds, but what do they actually mean? The easiest way to understand kinds is by looking at a bunch of examples of types and type constructors. Monomorphic types such as Int and Bool have kind *. Type constructors are handled differently. An example of a type constructor is [] (list), which has kind * -> *. So list is a type constructor that takes in a type (which we represent with an asterisk), and returns another type. Therefore [Int] has kind *, since we applied the type Int to the list type constructor [], resulting in the type [Int]. Types constructors can also in some situations be partially applied, just like value constructors. Kinds are right associative, so the kind *->*->* is the same as *->(*->*)

The table below gives the kinds of various type expressions from Haskell:

Type Expression	Kind
Int	*
Bool	*
Maybe	*->*
Either	*->*->*
[]	*->*
->	*->*->*
a->b	*
[Either Int Bool]	*
Either Int	*->*
(->) a	*->*
(,,,)	*->*->*->*->*
Mu where newtype Mu f = In { out :: f (Mu f) }	(* -> *) -> *

Note that partial application of type constructors have limitations. For example, the kind of [Either Int] is nonsensical, and Haskell gives the following error: Expecting one more argument to ‘Either Int’. Expected a type, but ‘Either Int’ has kind ‘* -> *’. The kind of the type constructors that we write are determined by the number of type variables on the left side of the type declaration. For example, the type data Foo a b c = ... has kind *->*->*->* since we have three type variables a, b, and c. So kinds fundamentally represent the arity of type constructors.

Type Expressions

Programs are typically composed of expressions of values, constants, variables, operators, and functions. Analogously, we can have type expressions which live at the type level. First we will define type expressions in terms of type variables, type constructors, and type applications:

The definition above also includes the type Scheme, which represents a type with a forall quantifier. Schemes are used when defining parametric polymorphic functions. Note that the constraint solver does not deal with Scheme in any way. When we want to solve a constraint that involves a polymorphic function, we will first have to instantiate a scheme by substituting the quantified variables with fresh type variables. This will be discussed in more detail later.

We will now define some functions which will be helpful for creating specific types:

Defining some string conversion functions will be useful for debugging. These functions may introduce extraneous parenthesis, but they will get the job done for our purposes:

Although the constraint solver will not deal with type schemes directly, it is useful to define some functions that work with them.

• tysubst is a very important function. It is used both by the constraint solver and the type scheme functions. tysubst takes in theta, which maps type variables to type expressions. Every type variable in the domain of theta is replaced with a corresponding type expression. Type variables that are not present in the domain of theta remain untouched.
• freshtyvar is used all the time when generating constraints. This generates a globally unique type variable.
• instantiate converts a type scheme to a type expression by substituting the universally quantified type variables with the list of type expressions in the actuals parameter.
• freevars will tell us what type variables exist within a certain type expression
• generalize does the opposite of instantiate by looking for free type variables in the type expression and then making them universally quantified. The skipTyVar parameter tells generalize which type variables it should ignore. This function is used when generalizing let bindings.

Constraints

We are now ready to define the types which will represent the constraints. The constraint type will be divided into three different value constructors:

• Equal which tells the solver that the two type expressions must be equal. Equal also includes an ErrorMessage, which is a lazily evaluated string. This ensures that the error messages are not actually created unless they are actually needed. In some of the compilers that I’ve written, the string includes information obtained from a disk read (to show the programmer where the error was in their source code), so making this lazy is very important for performance reasons. Including an error message here makes type errors that are very understandable.
• And which conjoins two constraints that must both be satisfied.
• Trivial is a constraint which is always satisfied.

conjoinConstraints is a helper function which joins a list of constraints together by using the And value constructor.

Solver

Now for the big finale! Given a system of constraints, we want to get a Map<TyVar, TyExpr> (aka Subst), which will tell us how we should map the unknown variables to concrete TyExprs.

• First we define some extension functions to F#’s Map module, which will be helpful in writing the solver.
• The varsubst function takes in a Subst and a TyVar. If the TyVar is in the domain of the substitution, we apply the substitution, otherwise we leave the TyVar alone.
• compose will join two Substs together into a new map. compose is more sophisticated than a simple Map merge. To start off, we union the two domains of the substitutions together. Then for every TyVar in the new domain, first apply theta1 by running it through varsubst, then pass this result through theta2 via the tysubst function we defined before.
• (|--->) will create a new binding in an empty Subst. If the variable being bound a is exactly the same as tau there is no need to define a new substitution, so just return idSubst. If a is in the free variables of tau, then the constraint is unsolvable. An example where we can run into this is with the constraint a ~ [a]. In all other cases, we should return a new Subst, where a is mapped to tau.
• consubst will update a Constraint with the results of the Subst.
• The solve function will solve a system of constraints and return a Subst as a solution.
  • In the case where the constraint is Trivial, then the system is solvable by the identity substitution.
  • In the case where the constraint is And, we first solve the left hand side, then apply the resulting substitution to the right hand constraints. Then we solve the new right hand constraints by calling solve again. The final step is to compose the results together.
  • In the case where the constraint is Equal, we pattern match on the type pair (tau1, tau2).
    • In the case where one of the two sides is a type variable, then we try to bind one side to the other. If (|--->) returns None, then the system cannot be solved, so we should raise a TypeError. Otherwise, we return the substitution given by (|--->).
      
      Notice that if both sides are type variables, then the left type variable ends up mapping to the right type variable. From the perspective of the constraint solver, this preference for mapping from left to right doesn’t matter much. In the larger picture, keeping this asymmetry in mind when generating constraints is important. For example, we should always prefer to place a user declared constraint on the right hand side so that the right side ends up in the codomain of the Subst map instead of the domain.
    • In the case where the two sides were both type constructors, then we check if they are equal. If they are the same, then the identity substitution is returned. Otherwise, we raise a TypeError.
    • In the case where the two sides are type applications, then we make a new system of constraints by demanding that the left side of the type applications must be equal, and the right hand sides of the type applications must be equal. We then solve the new system of constraints via a recursive call.
    • In all other cases, the system is unsolvable, so we raise a TypeError.

Now we can test our solver by writing some test cases:

On lines 1-3, we can see the result of the first call to solve. The constraint we were trying to solve was (t1, Number) ~ (Unit, t2), and the output was the Map {t1 → Unit, t2 → Number}, as expected. The second constraint was Unit ~ Number, which wasn’t solvable. The solver correctly raised a TypeError which notified us of the mistake in addition to showing the error message attached to the constraint.

Wrapping Up

Generating constraints is usually a straightforward process, and can be accomplished by using a recursive function. The constraint generation process will be the subject of my next blog post.

The constraint solver presented here is based on Norman Ramsey’s book Programming Languages: Build, Prove, and Compare. The book is still unpublished at the time of this post’s publication.

The code in this blog post is placed under the Unlicense license (which places the code presented here in the public domain).

Related Links

• Typing Haskell in Haskell
• Let Should not be Generalised