What is Hindley-Milner?

by

Hindley-Milner is a type system discovered independently by Roger Hindley (who was looking at logic) and later by Robin Milner (who was looking at programming languages). The advantages of Hindley-Milner are

  • It supports polymorphic functions; for example, a function that can give you the length of the list independent of the type of the elements, or a function does a binary-tree lookup independent of the type of keys stored in the tree.

  • Sometimes a function or value can have more than one type, as in the example of the length function: it can be “list of integers to integer”, “list of strings to integer”, “list of pairs to integer”, and so on. In this case, a signal advantage of the Hindley-Milner system is that each well-typed term has a unique “best” type, which is called the principal type. The principal type of the list-length function is “for any a, function from list of a to integer”. Here a is a so-called “type parameter,” which is explicit in lambda calculus but implicit in most programming languages. The use of type parameters explains why Hindley-Milner is a system that implements parametric polymorphism. (If you write a definition of the length function in ML, you can see the type parameter thus:

     fun 'a length []      = 0
   | 'a length (x::xs) = 1 + length xs

  • If a term has a Hindley-Milner type, then the principal type can be inferred without requiring any type declarations or other annotations by the programmer. (This is a mixed blessing, as anyone can attest who has ever been handled a large chunk of ML code with no annotations.)

Hindley-Milner is the basis for the type system of almost every statically typed functional language. Such languages in common use include

All these languages have extended Hindley-Milner; Haskell, Clean, and Objective Caml do so in ambitious and unusual ways. (Extensions are required to deal with mutable variables, since basic Hindley-Milner can be subverted using, for example, a mutable cell holding a list of values of unspecified type. Such problems are dealt with by an extension called the value restriction.)

Many other minor languages and tools based on typed functional languages use Hindley-Milner.

Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.

More Related Contents:

  1. Spanning repeatable keys
  2. What is a ‘Closure’?
  3. What is (functional) reactive programming?
  4. Set operations (union, intersection) on Swift array?
  5. What is referential transparency?
  6. What is a Y-combinator? [closed]
  7. What is the difference between eq?, eqv?, equal?, and = in Scheme?
  8. How do you represent a graph in Haskell?
  9. Advantages of stateless programming?
  10. How can you do anything useful without mutable state?
  11. What is the difference between procedural programming and functional programming? [closed]
  12. What is ‘Pattern Matching’ in functional languages?
  13. “Closures are poor man’s objects and vice versa” – What does this mean?
  14. What is the exact definition of a closure?
  15. Functional programming and non-functional programming
  16. How to understand curry and function composition using Lodash flow?
  17. How can I get a flat result from a list comprehension instead of a nested list?
  18. Functional Programming: what is an “improper list”?
  19. What is “point free” style (in Functional Programming)?
  20. What part of Hindley-Milner do you not understand?
  21. In Functional Programming, what is a functor?
  22. How to compose functions in Rust?
  23. How can a time function exist in functional programming?
  24. Pass a typed function as a parameter in Dart
  25. Specification for a Functional Reactive Programming language
  26. Are there problems that cannot be written using tail recursion?
  27. So: what’s the point?
  28. What is dependent typing?
  29. Functional programming vs Object Oriented programming [closed]
  30. Difference between timestamps with/without time zone in PostgreSQL

Leave a Comment