Type Inference Exercise

(from discussion sections on 3/29/10)

Bill suggested a simpler process for type inference than the graph-based approach presented in lecture:
  1. Generate a set of equality constraints by recursively traversing the syntax tree (this is basically slide 15 [of lecture 13]).
  2. Solve the constraints by simplification. I'm going to assume that types are written as follows: That is, every type has a tag (like int or list) and some arguments (which will be empty for base types). When the argument list is empty, we omit the parentheses.

    To solve the generated equations we use a few rules:

    1. Given a constraint of the form A = term, just replace A with term in all the other constraints so that A is eliminated.
    2. Given a constraint of the form tag(T1, ..., Tn) = tag(T1', ..., Tn'), throw it away and replace it with new equations T1 = T1', ..., Tn = Tn'.
    3. Given a constraint of the form tag1(T1, ..., Tn) = tag2(T1', ..., Tn'), where tag1 != tag2, we have a type error and the equations have no solution.
    This technique needs minor modifications when there are recursive types (namely in rule (a)) but it seems more intuitive than the algorithm in lecture.

Our exercise is to apply Bill's approach to the following functions: 

fun f []        = ([], [])
  | f [x]       = ([x], [])
  | f (x::y::t) = let val (r, s) = f t
                   in (x::r, y::s)
                  end;

fun g p ([], s) = s
  | g p (s, []) = s
  | g p (x::s, y::t) =
    if p (x, y) then x::(g p (   s, y::t))
                else y::(g p (x::s,    t));

fun h p [] = []
  | h p a = let val (s, t) = f a
             in g p (h p s, h p t)
            end;
We'll take a few shortcuts. For example, instead of starting with A → B as the type for f, we'll skip to list(A) → (list(B), list(C)), since we can see from the first line of f that the argument type is a list type and the return type is a tuple of lists. We'll also use a little different notation from Bill's: A → B → C for functions and (A, B) for tuples.

Looking at the other lines of f, we get the following equations:

list(A) = list(B) (since we can return the argument in the tuple)
X = A (since x is an element of a list(A))
Y = A (ditto)
(list(R), list(S)) = (list(B), list(C)) (We use R and S as the element types rather than list types because we can see that r and s must have list types.)
X = R (since we can cons x onto a list(R))
Y = S (likewise)

Substituting A for X, Y, R, and S, we get that the type of f is list(A) → (list(A), list(A)).

Equations for g : P → (list(D), list(E)) → list(E)

list(D) = list(E)
X = D (This is a new X, not necessarily the same as the one we used for f.)
Y = E (ditto)
P = (X, Y) → bool
X = E
Solution: The type of g is ((D, D) → bool) → (list(D), list(D)) → list(D).

Equations for h : Q → list(F) → list(G):

list(A) = list(F) (because we pass a to f)
(S, T) = (list(A), list(A))
S = list(F)
T = list(F)
Q = ((D, D) → bool)
list(G) = list(D) (for two reasons: The return value of h becomes an argument of g, and the return value of g becomes the return value of h.)
Solution: The type of h is ((D, D) → bool) → list(A) → list(D).

You may have noticed that f, g, and h implement merge sort with a generic comparison predicate p. However, they have a bug, and the fact that type inference doesn't unify A and D is a consequence of the bug. See the slides starting here for an explanation of the bug and the fix.