Constraint-based Type Inference with Algebraic Data

Question

I am working on an expression based language of ML genealogy, so it naturally needs type inference >:)

Now, I am trying to extend a constraint-based solution to the problem of inferring types, based on a simple implementation in EOPL (Friedman and Wand), but they elegantly side-step algebraic datatypes.

What I have so far works smoothly; if an expression e is a + b, e : Int, a : Int and b : Int. If e is a match,

match n with
  | 0 -> 1
  | n' -> n' * fac(n - 1)`, 

I can rightly infer that the t(e) = t(the whole match expression), t(n) = t(0) = t(n'), t(match) = t(1) = t(n' * fac(n - 1) and so on...

But I am very unsure when it comes to algebraic datatypes. Suppose a function like filter:

let filter pred list =
  match list with
    | Empty -> Empty
    | Cons(e, ls') when pred e -> Cons (e, filter ls')
    | Cons(_, ls') -> filter 

For the list type to remain polymorphic, Cons needs to be of type a * a list -> a list. So, in establishing these constraints, I obviously need to look up these types of my algebraic constructors - the problem I now have is the 'context-sensitivity' of multiple uses of algebraic constructors - how do I express in my constraint equations that the a in each case needs to be the same?

I am having trouble finding a general solution to this, and I am unable to find much literature on this. Whenever I find something similar - expression based language with constraint-based type inference - they stop just short of algebraic datatypes and polymorphism.

Any input is much appreciated!

Answer 1

See: Mini ML Specifically the Type Inference section.

This contains sample code in F# for a complete parser of a simple functional language. More importantly the Type Inference section implements the Hindley-Milner algorithm which is what is found in most type inference system. The author also provides links to two other important documents to help in understanding Hindley-Milner; one being a kind of high level introduction and the other being a paper that describes the implementation of the algorithm in code.