Type Constraints

To gather the constraints for a definition, HM does the following:

• Assign a preliminary type to every subexpression in the definition. For known operations and constants, such as + and 3, use the type that is already known for it. For anything else, use a new type variable that hasn't been used anywhere else.

• Use the "shape" of the expressions to generate constraints. For example, if an expression involves applying a function to an argument, then generate a constraint requiring the type of the argument to be the same as the function's input type.

We'll give some examples of this first, then we'll give the algorithms for doing it.

Example 1.

Here's an example utop interaction:

# let g x = 5 + x;;
val g : int -> int = <fun>

How did OCaml infer the type of g here? Let's work it out.

First, let's rewrite g syntactically to make our work a little easier:

let g = fun x -> ((+) 5) x

We've made the anonymous function explicit, and we've made the binary infix operator a prefix function application.

1. Assign preliminary types.

For each subexpression of fun x -> (+) 5 x, including the entire expression itself, we assign a preliminary type. We already know the types of (+) and 5, because those are baked into the language itself, but for everything else we "play dumb" and just invent a new type variable for it. For now we will use uppercase letters to represent those type variables, rather than the OCaml syntax for type variables (e.g., 'a).

Subexpression         Preliminary type
------------------    --------------------
fun x -> ((+) 5) x    R
    x                 U
         ((+) 5) x    S
         ((+) 5)      T
          (+)         int -> (int -> int)
              5       int
                 x    V

2. Collect constraints.

Here are some observations we could make about the "shape" of subexpressions and some relationships among them:

• Since function argument x has type U and function body ((+) 5) x has type S, it must be the case that R, the type of the anonymous function expression, satisfies the constraint R = U -> S. That is, the type of the anonymous function is the type of its argument arrow the type of its body.

• Since function ((+) 5) has type T and function application ((+) 5) x has type S, and since the argument x has type V, it must be the case that T = V -> S. That is, the type of the function being applied is the type of the argument it's being applied to arrow the type of the function application expression.

• Since function (+) has type int -> (int -> int) and function application (+) 5 has type T, and since the argument 5 has type int, it must be the case that int -> (int->int) = int -> T. Once again, the type of the function being applied is the type of the argument it's being applied to arrow the type of the function application expression.

• Since x occurs with both type U and V, it must be the case that U = V.

The set of constraints thus generated is:

                  U = V
                  R = U -> S
                  T = V -> S
int -> (int -> int) = int -> T

3. Solve constraints.

You can solve that system of equations easily. Starting from the last constraint, we know T must be int -> int. Substituting that into the second constraint, we get that int -> int must equal V -> S, hence V = S = int. Since U=V, U must also be int. Substituting for S and U in the first constraint, we get that R = int -> int. So the inferred type of g is int -> int.

Example 2.

# let apply f x = f x;;
val apply : ('a -> 'b) -> 'a -> 'b = <fun>

Again we rewrite:

let apply = fun f -> (fun x -> f x)

1. Assign preliminary types.

Subexpression              Preliminary type
-----------------------    ------------------
fun f -> (fun x -> f x)    R
    f                      S 
         (fun x -> f x)    T 
              x            U 
                   f x     V 
                   f       S
                     x     U

2. Collect constraints.

• R = S -> T, because of the anonymous function expression.
• T = U -> V, because of the nested anonymous function expression.
• S = U -> V, because of the function application.

3. Solve constraints.

Using the third constraint, and substituting for S in the first constraint, we have that R = (U -> V) -> T. Using the second constraint, and substituting for T in the first constraint, we have that R = (U -> V) -> (U -> V). There are no further substitutions that can be made, so we're done solving the constraints. If we now replace the preliminary type variables with actual OCaml type variables, specifically U with 'a and V with 'b, we get that the type of apply is ('a -> 'b) -> ('a -> 'b), which is the same as ('a -> 'b) -> 'a -> 'b.

Example 3.

# apply g 3;;
- : int = 8

We rewrite that as (apply g) 3.

1. Assign preliminary types.

In this running example, the inference for g and apply has already been done, so we can fill in their types as known, much like the type of + is already known.

Subexpression     Preliminary type
-------------     ------------------------------------------
(apply g) 3       R 
(apply g)         S  
 apply            (U -> V) -> (U -> V)
       g          int -> int
          3       int

2. Collect constraints.

• S = int -> R
• `(U -> V) -> (U -> V) = (int -> int) -> S

3. Solve constraints.

Breaking down the last constraint, we have that U = V = int, and that S = U -> V, hence S = int -> int. Substituting that into the first constraint, we have that int -> int = int -> R. Therefore R = int, so the type of apply g 3 is int.

Example 4.

# apply not false;;
- : bool = true

By essentially the same reasoning as in example 3, HM can infer that the type of this expression is bool. This illustrates the polymorphism of apply: because the type (U -> V) -> (U -> V) of apply contains type variables, the function can be applied to any arguments, so long as those arguments' types can be consistently substituted for the type variables.