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
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!