An Explanation of Type Inference for ML/Haskell

http://jozefg.bitbucket.org/posts/2015-02-28-type-inference.html

by bjz_ • 11 years ago

101 12 11 years ago

jozefg.bitbucket.org

glutamate3• 11 years ago

The Programming Languages Zoo really helped me in learning type inference implementation. It has a series of increasingly complex languages, all implemented in ML.

http://andrej.com/plzoo/

dwenzek• 11 years ago

In the same vein you have this site [1], with misc type related algorithms and implementations in OCaml .

[2] is a paper with a modula-2 implementation. Written by Luca Cardelli, a type fellow, it really helped me to understand type inference.

[1] https://github.com/tomprimozic/type-systems. [2] http://lucacardelli.name/Papers/BasicTypechecking.pdf

kjs3• 11 years ago

Yeah...pretty much anything mentioning Cardelli needs an upvote. He's a brilliant guy and a very clear, understandable writer.

cabalamat2• 11 years ago

The Programming Languages Zoo

I don't suppose you know of an equivalent written in Haskell, do you?

gelisam• 11 years ago

Sounds like fun, let's write one!

glutamate3• 11 years ago

A lot of the code in the PL Zoo is very readable and translates straight to Haskell. I mean look at this stuff:

http://andrej.com/plzoo/html/miniml.html

you can almost translate that with an emacs macro. Except for the parsing stuff, which is some OCaml specific parser generator.

jozefg• 11 years ago

It's not a bad skill to be able to read SML/OCaml. They're really very similar to Haskell and actually pretty fun to write.

I suppose you could have inferred (ha) I feel that way from this blog post though :)

seanmcdirmid• 11 years ago

The only thing better than unification is semi-unification. The fact that semi-unification is a lot harder than unification has meant that imperative OO languages get the shaft with poorer type inference support: both assignment and subtyping are inequalities! What Scala has done with least-upper bounds is absolutely heroic in that context even if it does work better for its functional parts.

tomp• 11 years ago

I'm not sure if "better" is appropriate in this context; in general, semi-unification is undecidable. Type checking in presence of subtypes is decidable for simple cases (where types form a lattice), but the presence of polymorphism/generics makes it undecidable (Java [1], OCaml[2]). The type inference algorithms for subtyping are not that performant (an algorithm is described in [3]).

[1] http://stackoverflow.com/questions/23939168/is-c-sharp-type-...

[2] http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html

[3] http://www.normalesup.org/~simonet/publis/simonet-aplas03.pd...

Rickasaurus• 11 years ago

I ported this to F# so you can mouse over and view the types: http://fssnip.net/q2

An Explanation of Type Inference for ML/Haskell

Related Stories