Menu
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 ?
337
The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus. and suitable type variables, while polymorphism and dependency cannot.
Actual TypeScript implements bidirectional type checking; bidirectional type checking is simpler to implement; and Hindley-Milner doesn't combine easily with subtyping and union types, so it isn't a good fit for TypeScript.
Rust uses Hindley-Milner type inference. OCaml uses Hindley-Milner. Swift apparently uses a variant of the system with more features. None of these make use of monads or anything rooted in category theory.
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:
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.
133
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.
22
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
