It is a type system for the lambda calculus.
It was discovered by Roger Hindley and later by Robin Milner.
It is a type system with parametric polymorphism. By this system, an algorithm for determining the types from an un-typed syntax can be formulated.

This is done using “unification”. By unification, the types of a well-structured program, upon solving, give constraints with a unique principal type.
Hindley Milner is used for functional languages.

In the beginning, it was used for programming language ML. It has been extended in many ways since them.
It is the basis for the type systems of the following functional languages:

• The ML family
• Haskell
• Clean
  Many other minor functional languages also use Hindley-Milner.
  

It is a restriction of System F.
In System F; there are more types annotations are required by the programmer.

How it works

The first task is to describe what types an expression can have.
The second task is to compute the algorithm that would help to create that type.
We need to figure out the logic behind the algorithm as well as the algorithm itself.

Hindley-Milner is an algorithm for inferring value types based on use.
We look through the body of a function and compute a constraint set.
This set is on the usage of each value.
Then the type reconstruction is completed by the algorithm by unifying the constraints.
We will get an unambiguous type at the end of the line if the expression is well typed.
If that is not the case, the constraints will not be satisfiable with the available types

The first phase is to derive the constraint set.
The second phase is to look for operations which impose some sort of type constraint.  The last phase is to unify all of these constraints.
Unification is the process of looking at the constraints and finding a single type which satisfies all constraints.

Advantages of Hindley-Milner System:

Here are some advantages of the system are:

• It supports Polymorphic functions.
• When there is more than one type of a function, we find a principal type using Hindley-Milner system.The principal type is the unique best type for each of the well-typed term.
• The type parameters used in this system help in implementing parametric polymorphism. It can deduce the most general type of a program even with lack of type annotations
• Many complicated reconstructions can be done using this algorithm.
  It reduces the required amount of syntax to a bare minimum.