1

I don't understand the connection between type inference and advanced type systems. I don't see why Haskell or Standard ML or OCaml could not have existed without type inference. My only guess is that type inference might have been a trend in the 70s when ML first came out and the descendent languages simply kept that ability in addition to the primary task of the type system which was to ensure type safety. Or perhaps the type safety algorithm also easily gave the ability to infer types and it was included just because it was simple?

I was just rereading the wikipedia article on System F and it indicates that HM introduced serious limitations to the type system in order to get type inference working. This is pretty surprising to read.

  • Mostly your last sentence, though not just because it was simple. The more advanced the type system is, the easier it is to infer types. Type inference was a specific design goal of ML and its family of languages; see sml-family.org/papers/MacQueen-reflections.pdf – Robert Harvey Jul 15 '16 at 16:43
  • Actually, after reviewing the wikipedia article on System F (en.wikipedia.org/wiki/System_F#Use_in_programming_languages), it indicates that HM introduced serious restrictions on the type system in order to allow type inference. This seems to contradict what you just stated about more advanced type systems. – eatonphil Jul 15 '16 at 16:48
  • 2
    Alright, well then that calls into question the definition of "advanced." And now I'm going to ask you what your specific question is. What is your specific question? – Robert Harvey Jul 15 '16 at 16:50
  • I guess I'm just confused because I'm so used to seeing type inference and type safety together. I'm trying to understand why so many languages share these traits. But I guess between that wikipedia article section and your pdf my question has been answered. – eatonphil Jul 15 '16 at 16:52
6

What is the connection between type inference and advanced type systems?

There are three things off the top of my head:

  1. Language designers interested in type systems will focus their language design around them. This means that all sorts of type oriented features were considered/implemented - inference being one.
  2. ML had it, so when follow up languages came along, they started with that design either due to familiarity, convenience, or adoptability.
  3. Once you start getting into more complex type systems, your annotations for types start becoming more and more complex. That adds confusion to the user, as well as noise to their code. Type inference was introduced to combat that problem, improving the usability of the language.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.