7 ms·

A reckless introduction to Hindley-Milner type inference (2019)

140 points by nequo 2y ago

cies 2y ago
I encountered HM a lot in my working life as a programmer. I did not expect that when I first encountered the names. From the article: > HM type systems can't implement heterogenous lists [...] > [well it does when wrapping the elements in a sum type, but then] > it can only accept types you know about in advance. > [which makes it] a massive pain to work with. Sorry, I totally disagree... Heterogeneous lists without the sum types are a massive pain! Maybe it is easier for the initial development effort, but if you need to maintain code with heterogeneous lists (or dynamically typed code in general) the pain will come at some point and likely when already in production. I much rather fix compile errors than runtime errors. And a massive thanks to Hindley and Milner for advancing type systems! Found their photos in gratitude just now: https://www.researchgate.net/profile/J-Hindley https://www.researchgate.net/profile/J-Hindley https://en.wikipedia.org/wiki/Robin_Milner https://en.wikipedia.org/wiki/Robin_Milner
- fluoridation 2y ago
  They're only a pain if you need to know the run-time types of the elements. If you're just operating on them through a narrowly defined interface, that's just dynamic polymorphism, which is indeed more flexible with regards to future expandability, as long as you define the interface appropriately.
  - deleted 2y ago
    [deleted]
  - cies 2y ago
    > as long as you define the interface appropriately Well, if you have an interface that all entries adhere to it is not a heterogeneous list in my book. In Haskell that could be achieve without a sum type wrapper, but with a type class. https://fluoridealert.org/key-topics/tsca-fluoride-lawsuit/ https://fluoridealert.org/key-topics/tsca-fluoride-lawsuit/
    - fluoridation 2y ago
      I mean, a heterogeneous list is literally a list where its elements may be of different types. To use a tired example, if a list that contains both a Cat and a Dog is not heterogeneous just because both adhere to the Mammal interface, then what is a heterogeneous list?
- philh 2y ago
  I think my position is: Native heterogeneous lists will often be convenient, and sometimes when you've used them they're going to turn out in retrospect to have been a bad idea but sometimes they'll be just fine, especially if they stay fairly locally scoped. I haven't done any serious work in a language that supports them for years, so I don't have a strong opinion about how often each of those cases happens. But if you decide you want heterogeneous lists, but your language doesn't support them, so you try to implement that with a sum type, then that's basically always going to be a massive pain.
  - cies 2y ago
    > I haven't done any serious work in a language that supports them for years Is this not silently admitting that strong types to some degree have won? Don't get me wrong: I like Clojure/LISPs/Ruby. But I would not choose them for a new project these days. (and I do not like JS, which has them too)
    - philh 2y ago
      I'm still working at the same company as when I wrote this, and that company is still using Haskell (now mostly Typescript instead of Elm). If I did move on I'd ideally want to keep using Haskell, or failing that some other strongly typed language. But I don't expect that my own experience says much about the language ecosystem in general. I don't particularly have an opinion on whether or not strong types have "won", and I didn't intend to comment on that question.
    - freilanzer 2y ago
      I would definitely choose a Lisp if it had an Intellij-like IDE. Especially since the type system of CL is good, though not static, obviously. But it's a tradeoff between having Haskell during compile time and CL during development time, for me.
  - yawaramin 2y ago
    What's an example use case where heterogeneous lists turn out to be fine but can't be modelled with eg the OCaml difflist technique, eg https://github.com/yawaramin/re-web/blob/0d6c62fb432f85cc43757c46849df8b75985199b/ReWebTest/FormTest.ml#L9 https://github.com/yawaramin/re-web/blob/0d6c62fb432f85cc437... ?
skybrian 2y ago
I think this article would be better if it ignored the issue of proving termination. Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it. For a possibly long-running job like a SQL query, a static guarantee that it terminates eventually is almost certainly not what you want. You’re going to need to test its performance, and ideally have a timeout and a way of handling the timeout. If you want to get fancy, a progress bar and cancel button might be nice. Edit: Compilers need to run fast for the programs we actually write. A type system that possibly doesn’t terminate under unusual conditions isn’t that big a deal, as long as people don’t write code like that. Hopefully you get a decent error message. Compare with memory use. We don’t want compilers to use excessive amounts of memory, but don’t need static guarantees about memory use.
- deleted 2y ago
  [deleted]
- dmkolobov 2y ago
  The problem with “not writing code like that” is that eventually someone does. At work we use a home-grown Haskell-like language with “row types” which can be split into disjoint sets of fields in order to represent joins and the like. It works well in most cases, but it’s very easy to forget a type annotation and trigger unmanageable build-times. Often times, it is not obvious where something needs to be annotated. Sure, we can act as human time-outs, but the productivity loss can be substantial, especially for a newcomer to the language.
  - gpm 2y ago
    The solution to "eventually someone does" is "add a timeout, and when you hit that timeout give them an error so they can fix their code". There's no practical difference between exponential and infinite time, you need to do this for bad exponential time cases anyways. Many langauges type systems (Java, Typescript, C++, Rust, ...) really aren't guaranteed to terminate in the absence of a timeout either. They're (the type systems) turing complete, you can write infinite loops that the compiler can't know are infinite loops. This makes no practical difference relative to languages which "merely" have exponential time type systems, because with an exponential time type system you're alread accepting the risk that typechecking might not terminate before the heat death of the universe.
abeppu 2y ago
Can someone familiar with the territory recommend a better or complementary resource of similar level of approachability? The intro here flags that the author i) is not happy with the post in its current form, ii) was resynthesized from wikipedia "without particularly putting in the effort to check my own understanding", which doesn't inspire confidence. And then when you do get into the content, stuff looks incorrect, but a non-expert reader, given the caveats in the intro, should be on the lookout for errors but isn't equipped to identify them with confidence. E.g. the very first inference rule included is described as: > if you have a variable x declared to have some polytype π, and if the monotype μ is a specialisation of π, then x can be judged to have type μ ... but I think this should be "π is a specialization of μ". Basically, I think this is the kind of material where detail matters, where errors seriously impede understanding, and a resource where the reader/learner has to be on guard second-guessing the author is a bad intro resource. But surely there are better ones out there.
- nathanrf 2y ago
  The quoted paragraph is correct as written. E.g. if f: ∀A, B. A -> B -> A Then we have poly type π = "∀A, B. A -> B -> A". The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge that f has type μ. The type specialization operator "looks backwards", where we write sorta "π ≤ μ" because there's a kind of "subtyping" relationship (though most HM type systems don't actually contain subtyping) - anywhere that a term of type μ is used, a term of type π can be used instead because it can be specialized to μ. I think this is a good complementary article: https://boxbase.org/entries/2018/mar/5/hindley-milner/ https://boxbase.org/entries/2018/mar/5/hindley-milner/ (it also links to three more academic sources for more context/detail)
- shpongled 2y ago
  "Types and Programming Languages" by Benjamin Pierce is an excellent textbook (and approachable, even to people without formal CS education) that covers type inference and introduces a lot of the nomenclature/formalism gradually.
  - bbkane 2y ago
ashton314 2y ago
Here are my notes on writing a type checker/type inferrer in case anyone is interested: https://lambdaland.org/posts/2022-07-27_how_to_write_a_type_checker/ https://lambdaland.org/posts/2022-07-27_how_to_write_a_type_...

140 points by nequo 2y ago

cies 2y ago

I encountered HM a lot in my working life as a programmer. I did not expect that when I first encountered the names. From the article: > HM type systems can't implement heterogenous lists [...] > [well it does when wrapping the elements in a sum type, but then] > it can only accept types you know about in advance. > [which makes it] a massive pain to work with. Sorry, I totally disagree... Heterogeneous lists without the sum types are a massive pain! Maybe it is easier for the initial development effort, but if you need to maintain code with heterogeneous lists (or dynamically typed code in general) the pain will come at some point and likely when already in production. I much rather fix compile errors than runtime errors. And a massive thanks to Hindley and Milner for advancing type systems! Found their photos in gratitude just now: https://www.researchgate.net/profile/J-Hindley https://www.researchgate.net/profile/J-Hindley https://en.wikipedia.org/wiki/Robin_Milner https://en.wikipedia.org/wiki/Robin_Milner

fluoridation 2y ago
They're only a pain if you need to know the run-time types of the elements. If you're just operating on them through a narrowly defined interface, that's just dynamic polymorphism, which is indeed more flexible with regards to future expandability, as long as you define the interface appropriately.
- deleted 2y ago
  [deleted]
- cies 2y ago
  > as long as you define the interface appropriately Well, if you have an interface that all entries adhere to it is not a heterogeneous list in my book. In Haskell that could be achieve without a sum type wrapper, but with a type class. https://fluoridealert.org/key-topics/tsca-fluoride-lawsuit/ https://fluoridealert.org/key-topics/tsca-fluoride-lawsuit/
  - fluoridation 2y ago
    I mean, a heterogeneous list is literally a list where its elements may be of different types. To use a tired example, if a list that contains both a Cat and a Dog is not heterogeneous just because both adhere to the Mammal interface, then what is a heterogeneous list?
philh 2y ago
I think my position is: Native heterogeneous lists will often be convenient, and sometimes when you've used them they're going to turn out in retrospect to have been a bad idea but sometimes they'll be just fine, especially if they stay fairly locally scoped. I haven't done any serious work in a language that supports them for years, so I don't have a strong opinion about how often each of those cases happens. But if you decide you want heterogeneous lists, but your language doesn't support them, so you try to implement that with a sum type, then that's basically always going to be a massive pain.
- cies 2y ago
  > I haven't done any serious work in a language that supports them for years Is this not silently admitting that strong types to some degree have won? Don't get me wrong: I like Clojure/LISPs/Ruby. But I would not choose them for a new project these days. (and I do not like JS, which has them too)
  - philh 2y ago
    I'm still working at the same company as when I wrote this, and that company is still using Haskell (now mostly Typescript instead of Elm). If I did move on I'd ideally want to keep using Haskell, or failing that some other strongly typed language. But I don't expect that my own experience says much about the language ecosystem in general. I don't particularly have an opinion on whether or not strong types have "won", and I didn't intend to comment on that question.
  - freilanzer 2y ago
    I would definitely choose a Lisp if it had an Intellij-like IDE. Especially since the type system of CL is good, though not static, obviously. But it's a tradeoff between having Haskell during compile time and CL during development time, for me.
- yawaramin 2y ago
  What's an example use case where heterogeneous lists turn out to be fine but can't be modelled with eg the OCaml difflist technique, eg https://github.com/yawaramin/re-web/blob/0d6c62fb432f85cc43757c46849df8b75985199b/ReWebTest/FormTest.ml#L9 https://github.com/yawaramin/re-web/blob/0d6c62fb432f85cc437... ?

skybrian 2y ago

I think this article would be better if it ignored the issue of proving termination. Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it. For a possibly long-running job like a SQL query, a static guarantee that it terminates eventually is almost certainly not what you want. You’re going to need to test its performance, and ideally have a timeout and a way of handling the timeout. If you want to get fancy, a progress bar and cancel button might be nice. Edit: Compilers need to run fast for the programs we actually write. A type system that possibly doesn’t terminate under unusual conditions isn’t that big a deal, as long as people don’t write code like that. Hopefully you get a decent error message. Compare with memory use. We don’t want compilers to use excessive amounts of memory, but don’t need static guarantees about memory use.

deleted 2y ago
[deleted]
dmkolobov 2y ago
The problem with “not writing code like that” is that eventually someone does. At work we use a home-grown Haskell-like language with “row types” which can be split into disjoint sets of fields in order to represent joins and the like. It works well in most cases, but it’s very easy to forget a type annotation and trigger unmanageable build-times. Often times, it is not obvious where something needs to be annotated. Sure, we can act as human time-outs, but the productivity loss can be substantial, especially for a newcomer to the language.
- gpm 2y ago
  The solution to "eventually someone does" is "add a timeout, and when you hit that timeout give them an error so they can fix their code". There's no practical difference between exponential and infinite time, you need to do this for bad exponential time cases anyways. Many langauges type systems (Java, Typescript, C++, Rust, ...) really aren't guaranteed to terminate in the absence of a timeout either. They're (the type systems) turing complete, you can write infinite loops that the compiler can't know are infinite loops. This makes no practical difference relative to languages which "merely" have exponential time type systems, because with an exponential time type system you're alread accepting the risk that typechecking might not terminate before the heat death of the universe.

abeppu 2y ago

Can someone familiar with the territory recommend a better or complementary resource of similar level of approachability? The intro here flags that the author i) is not happy with the post in its current form, ii) was resynthesized from wikipedia "without particularly putting in the effort to check my own understanding", which doesn't inspire confidence. And then when you do get into the content, stuff looks incorrect, but a non-expert reader, given the caveats in the intro, should be on the lookout for errors but isn't equipped to identify them with confidence. E.g. the very first inference rule included is described as: > if you have a variable x declared to have some polytype π, and if the monotype μ is a specialisation of π, then x can be judged to have type μ ... but I think this should be "π is a specialization of μ". Basically, I think this is the kind of material where detail matters, where errors seriously impede understanding, and a resource where the reader/learner has to be on guard second-guessing the author is a bad intro resource. But surely there are better ones out there.

nathanrf 2y ago
The quoted paragraph is correct as written. E.g. if f: ∀A, B. A -> B -> A Then we have poly type π = "∀A, B. A -> B -> A". The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge that f has type μ. The type specialization operator "looks backwards", where we write sorta "π ≤ μ" because there's a kind of "subtyping" relationship (though most HM type systems don't actually contain subtyping) - anywhere that a term of type μ is used, a term of type π can be used instead because it can be specialized to μ. I think this is a good complementary article: https://boxbase.org/entries/2018/mar/5/hindley-milner/ https://boxbase.org/entries/2018/mar/5/hindley-milner/ (it also links to three more academic sources for more context/detail)
shpongled 2y ago
"Types and Programming Languages" by Benjamin Pierce is an excellent textbook (and approachable, even to people without formal CS education) that covers type inference and introduces a lot of the nomenclature/formalism gradually.
- bbkane 2y ago

ashton314 2y ago

Here are my notes on writing a type checker/type inferrer in case anyone is interested: https://lambdaland.org/posts/2022-07-27_how_to_write_a_type_checker/ https://lambdaland.org/posts/2022-07-27_how_to_write_a_type_...