11
$\begingroup$

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!

$\endgroup$
  • $\begingroup$ @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). $\endgroup$ – Kris Apr 6 '12 at 23:57
  • $\begingroup$ I'd start with the inference chapter in ATTAPL, I think they discuss everything you need at an accessible level. $\endgroup$ – Gilles Apr 7 '12 at 0:35
  • $\begingroup$ @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 : ) $\endgroup$ – Kris Apr 7 '12 at 10:04
  • $\begingroup$ @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. $\endgroup$ – michiakig Oct 29 '17 at 20:26
  • $\begingroup$ @spacemanaki Yes, I have since found pdfs.semanticscholar.org/8983/… to be an excellent resource for exactly this. $\endgroup$ – Kris Nov 2 '17 at 8:41
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Single links are generally not an answer. Please elaborate what can be found there and why it helps. $\endgroup$ – Raphael Apr 20 '12 at 8:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.