7 ms·

What is Hindley-Milner and why is it cool? (2008)

185 points by jwdunne 9y ago

krat0sprakhar 9y ago
Hindley Milner is awesome and surpursingly not super hard to implement. Shameless plug: Wrote a minimal implementation in OCaml back in college https://github.com/prakhar1989/type-inference https://github.com/prakhar1989/type-inference
- chewxy 9y ago
  The challenge is of course writing one that is fast enough to be used for runtime-compilation (imagine a service that compiles code). I had to rewrite mine (https://github.com/chewxy/hm https://github.com/chewxy/hm) twice, and finally removing typeclasses to be fast enough for a inference system I wrote.
- mbrock 9y ago
  I first became interested in programming language theory back in high school when a guy in an IRC chat, who was a student at UIUC, asked me to do his homework for him. The assignment was to implement Hindley-Milner type checking with unification in OCaml. Thanks, lazy IRC guy!
  - jjtheblunt 9y ago
    Wow, good for you, ridiculous for the student's integrity; from UIUC also.
- Profan 9y ago
  Hindley Milner is quite elegant, but as applied in languages it becomes a quite different beast (OCaml etc, yikes) But also thanks to that detour, this article is a nice read on OCaml in particular: http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html
Animats 9y ago
The trend seems to be for languages to have forward inference of types within functions, while declaring them in function definitions. Assignments which initialize a variable also implicitly declare its type. C++ started this with "auto", but it's really because programmers had become used to dynamic languages where assignment set type. Go and Rust both do this. Inferring types of function parameters and results isn't as useful. Combined with generics, it gets really complicated. It seems better to have those declared explicitly. Programmers need to be able to read function signatures when programming. They're an essential part of the documentation. Also, whole-program type inference and separate compilation inherently conflict. That's pretty much where things seem to be settling out. Even Python now has optional type declarations for function signatures.
- jackmott 9y ago
  if the editor is aware of the type inference, you can display the signature without having to type it. it can be useful as you get automatically generic functions, which can save a lot of time if you decide the refactor later and use say, floats instead of doubles. you don't have to edit any functions. just start using floats.
  - Animats 9y ago
    if the editor is aware of the type inference Does any actual editor do that? Few text editors for programs are even aware of definitions in other modules.
    - sacheendra 9y ago
      I don't know if it is available for other languages. But IntelliJ does it for Kotlin.
    - paavohtl 9y ago
      Any editor or IDE with F# or TypeScript support can show the inferred type for anything you have selected or hover over. Ionide (an F# plugin for VS Code) can even show the inferred type over each let binding (including functions) within the text editor itself.
iitalics 9y ago
Hindley-Milner is cool, but if you're planning on implementing a language with type inference, I strongly suggest you take inspiration from bidirectional type inference, notably Pierce-Turner[1] and subsequently Dunfield-Krishnaswami[2]. These algorithms are capable of inferring much more complex types and generally produce better error messages. Typically, there are very few programs which can't be typed when you combine Dunfield-Krishnaswami type inference and have the user place annotations on major function definitions. [1] http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf [2] https://arxiv.org/pdf/1306.6032.pdf https://arxiv.org/pdf/1306.6032.pdf
- adrianratnapala 9y ago
  What does "bidirectional" mean in this context?
  - Others 9y ago
    Here is what they say in the introduction of the second paper: Bidirectional propagation of type information allows the types of parameters of anonymous functions to be inferred. When an anonymous function appears as an argument to another function, the expected domain type is used as the expected type for the anonymous abstraction, allowing the type annotations on its parameters to be omitted. A similar, but even simpler, technique infers type annotations on local variable bindings. From this I gather it means syntactically bidirectional. (But I don't understand this really, so someone should correct me :P)
  - tel 9y ago
    The algorithm is split into two mutual components the "inference" and the "checking" (upward and downward) which run together. This turns out to be a really flexible setting for playing with language and type features as it's often possible to figure out how to extend a bidirectional typer/inferrer with new features.
  - chewxy 9y ago
    It means check both ways Gamma |- e => t Given Gamma (the environment) and e, you want to derive the type t (bog standard type inference). The other direction also holds: Gamma |- e <= t Now we want to ensure that e conforms to type t. Consider for example, a function: func foo(a) b and an expression that we know the type of already: e <= a Therefore we can say when we apply `foo` onto `e`, we'll yield something of type `b` In effect, you perform 2 passes: forwards inference, and then backwards inference. p/s: I'm not actually a PL person. This is from my casual reading, so my understanding is highly probably very wrong
gergoerdi 9y ago
One drawback of the Hindley-Milner type system is that its typecheckers are necessarily non-compositional. The basic idea here is that this can result in "non-symmetrical" error messages[1]: given something like MkPair :: a -> b -> Pair a b not :: Bool -> Bool succ :: Int -> Int foo x = MkPair (succ x) (not x) the error message will either complain that `x` has type `Bool` but it should be `Int`, or it will complain that `x` has type `Int` but it should be `Bool` -- depending on what implementation you use! For example, in Haskell, Hugs 98 will emit the first error message, but GHC 7.10 will emit the second (see the full example in my slides[2]). And in some sense, neither is right (and certainly neither is as helpful for the programmer as it could be). So next time you're implementing vanilla HM, maybe consider a compositional type system[3] instead, which can give the following, much more informative error message: Cannot unify 'Int' with 'Bool' when unifying 'x': Cannot unify 'Int' with 'Bool' in the following context: MkPair (succ x) (not x) Bool -> Pair Int Bool Bool x :: Int Bool I have a simple implementation here[4], and am about to release a new version which works on `haskell-src-ext`'s AST to support more of Haskell 98 syntax (but still for vanilla HM only). [1] https://gergo.erdi.hu/blog/2010-10-23-the_case_for_compositional_type_checking/ https://gergo.erdi.hu/blog/2010-10-23-the_case_for_compositi... [2] https://gergo.erdi.hu/talks/2016-06-compty/CompTy.pdf https://gergo.erdi.hu/talks/2016-06-compty/CompTy.pdf [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.818 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.8... [4] https://github.com/gergoerdi/hm-compo/blob/master/src/Language/HM/Compositional.hs https://github.com/gergoerdi/hm-compo/blob/master/src/Langua...

185 points by jwdunne 9y ago

Hindley Milner is awesome and surpursingly not super hard to implement. Shameless plug: Wrote a minimal implementation in OCaml back in college https://github.com/prakhar1989/type-inference https://github.com/prakhar1989/type-inference

chewxy 9y ago
The challenge is of course writing one that is fast enough to be used for runtime-compilation (imagine a service that compiles code). I had to rewrite mine (https://github.com/chewxy/hm https://github.com/chewxy/hm) twice, and finally removing typeclasses to be fast enough for a inference system I wrote.
mbrock 9y ago
I first became interested in programming language theory back in high school when a guy in an IRC chat, who was a student at UIUC, asked me to do his homework for him. The assignment was to implement Hindley-Milner type checking with unification in OCaml. Thanks, lazy IRC guy!
- jjtheblunt 9y ago
  Wow, good for you, ridiculous for the student's integrity; from UIUC also.
Profan 9y ago
Hindley Milner is quite elegant, but as applied in languages it becomes a quite different beast (OCaml etc, yikes) But also thanks to that detour, this article is a nice read on OCaml in particular: http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html

Animats 9y ago

The trend seems to be for languages to have forward inference of types within functions, while declaring them in function definitions. Assignments which initialize a variable also implicitly declare its type. C++ started this with "auto", but it's really because programmers had become used to dynamic languages where assignment set type. Go and Rust both do this. Inferring types of function parameters and results isn't as useful. Combined with generics, it gets really complicated. It seems better to have those declared explicitly. Programmers need to be able to read function signatures when programming. They're an essential part of the documentation. Also, whole-program type inference and separate compilation inherently conflict. That's pretty much where things seem to be settling out. Even Python now has optional type declarations for function signatures.

jackmott 9y ago
if the editor is aware of the type inference, you can display the signature without having to type it. it can be useful as you get automatically generic functions, which can save a lot of time if you decide the refactor later and use say, floats instead of doubles. you don't have to edit any functions. just start using floats.
- Animats 9y ago
  if the editor is aware of the type inference Does any actual editor do that? Few text editors for programs are even aware of definitions in other modules.
  - sacheendra 9y ago
    I don't know if it is available for other languages. But IntelliJ does it for Kotlin.
  - paavohtl 9y ago
    Any editor or IDE with F# or TypeScript support can show the inferred type for anything you have selected or hover over. Ionide (an F# plugin for VS Code) can even show the inferred type over each let binding (including functions) within the text editor itself.

iitalics 9y ago

Hindley-Milner is cool, but if you're planning on implementing a language with type inference, I strongly suggest you take inspiration from bidirectional type inference, notably Pierce-Turner[1] and subsequently Dunfield-Krishnaswami[2]. These algorithms are capable of inferring much more complex types and generally produce better error messages. Typically, there are very few programs which can't be typed when you combine Dunfield-Krishnaswami type inference and have the user place annotations on major function definitions. [1] http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf [2] https://arxiv.org/pdf/1306.6032.pdf https://arxiv.org/pdf/1306.6032.pdf

adrianratnapala 9y ago
What does "bidirectional" mean in this context?
- Others 9y ago
  Here is what they say in the introduction of the second paper: Bidirectional propagation of type information allows the types of parameters of anonymous functions to be inferred. When an anonymous function appears as an argument to another function, the expected domain type is used as the expected type for the anonymous abstraction, allowing the type annotations on its parameters to be omitted. A similar, but even simpler, technique infers type annotations on local variable bindings. From this I gather it means syntactically bidirectional. (But I don't understand this really, so someone should correct me :P)
- tel 9y ago
  The algorithm is split into two mutual components the "inference" and the "checking" (upward and downward) which run together. This turns out to be a really flexible setting for playing with language and type features as it's often possible to figure out how to extend a bidirectional typer/inferrer with new features.
- chewxy 9y ago
  It means check both ways Gamma |- e => t Given Gamma (the environment) and e, you want to derive the type t (bog standard type inference). The other direction also holds: Gamma |- e <= t Now we want to ensure that e conforms to type t. Consider for example, a function: func foo(a) b and an expression that we know the type of already: e <= a Therefore we can say when we apply `foo` onto `e`, we'll yield something of type `b` In effect, you perform 2 passes: forwards inference, and then backwards inference. p/s: I'm not actually a PL person. This is from my casual reading, so my understanding is highly probably very wrong

gergoerdi 9y ago

One drawback of the Hindley-Milner type system is that its typecheckers are necessarily non-compositional. The basic idea here is that this can result in "non-symmetrical" error messages[1]: given something like MkPair :: a -> b -> Pair a b not :: Bool -> Bool succ :: Int -> Int foo x = MkPair (succ x) (not x) the error message will either complain that `x` has type `Bool` but it should be `Int`, or it will complain that `x` has type `Int` but it should be `Bool` -- depending on what implementation you use! For example, in Haskell, Hugs 98 will emit the first error message, but GHC 7.10 will emit the second (see the full example in my slides[2]). And in some sense, neither is right (and certainly neither is as helpful for the programmer as it could be). So next time you're implementing vanilla HM, maybe consider a compositional type system[3] instead, which can give the following, much more informative error message: Cannot unify 'Int' with 'Bool' when unifying 'x': Cannot unify 'Int' with 'Bool' in the following context: MkPair (succ x) (not x) Bool -> Pair Int Bool Bool x :: Int Bool I have a simple implementation here[4], and am about to release a new version which works on `haskell-src-ext`'s AST to support more of Haskell 98 syntax (but still for vanilla HM only). [1] https://gergo.erdi.hu/blog/2010-10-23-the_case_for_compositional_type_checking/ https://gergo.erdi.hu/blog/2010-10-23-the_case_for_compositi... [2] https://gergo.erdi.hu/talks/2016-06-compty/CompTy.pdf https://gergo.erdi.hu/talks/2016-06-compty/CompTy.pdf [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.818 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.8... [4] https://github.com/gergoerdi/hm-compo/blob/master/src/Language/HM/Compositional.hs https://github.com/gergoerdi/hm-compo/blob/master/src/Langua...