An Explanation of Type Inference for ML/Haskell(jozefg.bitbucket.org)
jozefg.bitbucket.org
An Explanation of Type Inference for ML/Haskell
http://jozefg.bitbucket.org/posts/2015-02-28-type-inference.html
12 comments
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.
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...
[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...
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/
http://andrej.com/plzoo/
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
[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
Yeah...pretty much anything mentioning Cardelli needs an upvote. He's a brilliant guy and a very clear, understandable writer.
> The Programming Languages Zoo
I don't suppose you know of an equivalent written in Haskell, do you?
I don't suppose you know of an equivalent written in Haskell, do you?
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.
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.
> you can almost translate that with an emacs macro
If I knew Haskell, I expect I could. However I am currently learning Haskell, which is why I'd be interested in a repository of example language implementations in Haskell.
> some OCaml specific parser generator
Which looks quite nice, and is evidently modelled on yacc/lex. People rave about Haskell's Parsec but TBH I'm finding it a bit unintuitive.
If I knew Haskell, I expect I could. However I am currently learning Haskell, which is why I'd be interested in a repository of example language implementations in Haskell.
> some OCaml specific parser generator
Which looks quite nice, and is evidently modelled on yacc/lex. People rave about Haskell's Parsec but TBH I'm finding it a bit unintuitive.
There is Happy and Alex for Haskell, and also some older tools like Frown and BNFC.
But the coolest thing about Parsec is that you can construct the parser at run-time, for instance calculating it after scanning a file for infix declarations. If you want custom infix in a yaccy grammar, you have to walk the AST afterwards to fix the application precedence.
But the coolest thing about Parsec is that you can construct the parser at run-time, for instance calculating it after scanning a file for infix declarations. If you want custom infix in a yaccy grammar, you have to walk the AST afterwards to fix the application precedence.
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 :)
I suppose you could have inferred (ha) I feel that way from this blog post though :)
Sounds like fun, let's write one!
I ported this to F# so you can mouse over and view the types: http://fssnip.net/q2