Constraint-based Type Inference with Algebraic Data

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!

• @Guy I don't mean to sound ungrateful, but I am not looking for an off-the-shelf solution - do you have any suggestions? Most existing docs I could find (like the INRIA papers on ML, OCaml...) are much more extensive than what I need (and am capable of understanding). – Kris Apr 6 '12 at 23:57
• I'd start with the inference chapter in ATTAPL, I think they discuss everything you need at an accessible level. – Gilles Apr 7 '12 at 0:35
• @Gilles I think ATTAPL is the only 'classic' PL book I don't have on my bookshelf : P But thanks, I will take a look on monday, I sit on a floor at Uni with perhaps 10 copies distributed across the offices : ) – Kris Apr 7 '12 at 10:04
• @Kris did you ever find an accessible resource tackling this problem? My implementation of a "mini ML" is stuck on exactly this problem... I think I found the relevant chapter from ATTAPL (pauillac.inria.fr/~fpottier/publis/emlti-final.pdf) and skimmed the section on algebraic data types, but I'm afraid it's a bit over my head. – michiakig Oct 29 '17 at 20:26
• @spacemanaki Yes, I have since found pdfs.semanticscholar.org/8983/… to be an excellent resource for exactly this. – Kris Nov 2 '17 at 8:41