Simply typed lambda calculus vs Hindley-Milner type system

Question

I have recently been learning about λ-calculus. I understood the difference between untyped and typed λ-calculus. But, I'm not much clear about the distinction between the Hindley-Milner type system and the typed λ-calculus. Is it about parametric polymorphism or are there any other differences ?

Can anyone clearly point out the differences (and similarities) between the two ?

Answer 1

The way I look at the relationship between typed λ-calculus and Hindley-Milner type system is that typed λ-calculus is λ-calculus with types added. You can do typed λ-calculus without needing Hindley-Milner type system, e.g. all of the types are declared, they are not inferred.

Now if you were to write a strongly statically typed programming language based on typed λ-calculus and wanted to omit type annotations allowing the types to be inferred then type inference is used and most likely you would use Hindley-Milner type system or a variation of it.

Another way to think about this is when creating a programming language based on typed λ-calculus is that the compiler would have phases, one of which would use Hindley-Milner type system. The order of the phases would be:

1. Syntax check - Lexer
2. Semantic check - Parser
3. Type inference - Hindley-Milner type system
4. Type checking
5. ...

Another way to think about this is that a type system has a set of type rules and that Hindley-Milner type system is a specific type system with a specific set of type rules. One of the main benefits of Hindley-Milner type system is that it is time efficient for inferring types and also has many of the typing rules sought in functional programming, e.g. Let-polymorphism and parametric polymorphism. In the real world if you are creating a programming language and want the types to be inferred then you want that to be done in a reasonable amount of time, e.g. seconds. Since inferencing can lead to combinatorial explosion an efficient set of rules is often sought and that is one of the main reasons why Hindley-Milner type system is so often used or referenced.

For real world programming languages based on typed λ-calculus see System F.

Answer 2

The distinction is that there are many type systems for the lambda calculus, and Hindley-Milner is one of them. Hindley-Milner is a type system with parametric polymorphism. This is what we call generics in today's programming languages.