HM is proven to be complete and able to infer the most general type of a given program: wikipedia article.
It is often described using natural deduction notation. Here is an handy explanation: What part of Hindley-Milner do you not understand?
Desirable properties
- Decidability - there is a procedure to make a typing decision.
- Soundness - everything the typing system prove is true.
- Completeness - everything that is true can be proven.