4 ms·

An Explanation of Type Inference for ML/Haskell

101 points by bjz_ 12y ago

glutamate 12y 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/ http://andrej.com/plzoo/
- dwenzek 12y 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 https://github.com/tomprimozic/type-systems. [2] http://lucacardelli.name/Papers/BasicTypechecking.pdf http://lucacardelli.name/Papers/BasicTypechecking.pdf
  - kjs3 12y ago
    Yeah...pretty much anything mentioning Cardelli needs an upvote. He's a brilliant guy and a very clear, understandable writer.
- cabalamat 12y ago
  > The Programming Languages Zoo I don't suppose you know of an equivalent written in Haskell, do you?
  - gelisam 12y ago
    Sounds like fun, let's write one!
  - glutamate 12y 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 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.
    - cabalamat 12y ago
      > 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.
      - glutamate 12y ago
        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.
  - jozefg 12y 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 12y 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 12y 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-system-sound-and-decidable http://stackoverflow.com/questions/23939168/is-c-sharp-type-... [2] http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html [3] http://www.normalesup.org/~simonet/publis/simonet-aplas03.pdf http://www.normalesup.org/~simonet/publis/simonet-aplas03.pd...
Rickasaurus 12y ago
I ported this to F# so you can mouse over and view the types: http://fssnip.net/q2 http://fssnip.net/q2

101 points by bjz_ 12y 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/ http://andrej.com/plzoo/

dwenzek 12y 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 https://github.com/tomprimozic/type-systems. [2] http://lucacardelli.name/Papers/BasicTypechecking.pdf http://lucacardelli.name/Papers/BasicTypechecking.pdf
- kjs3 12y ago
  Yeah...pretty much anything mentioning Cardelli needs an upvote. He's a brilliant guy and a very clear, understandable writer.
cabalamat 12y ago
> The Programming Languages Zoo I don't suppose you know of an equivalent written in Haskell, do you?
- gelisam 12y ago
  Sounds like fun, let's write one!
- glutamate 12y 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 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.
  - cabalamat 12y ago
    > 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.
    - glutamate 12y ago
      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.
- jozefg 12y 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 12y 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 12y 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-system-sound-and-decidable http://stackoverflow.com/questions/23939168/is-c-sharp-type-... [2] http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html [3] http://www.normalesup.org/~simonet/publis/simonet-aplas03.pdf http://www.normalesup.org/~simonet/publis/simonet-aplas03.pd...

Rickasaurus 12y ago

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