For instance, the ML system has the principal type property and principal types for an expression can be computed by Robinson's unification algorithm, which is used by the Hindley–Milner type inference algorithm.
However, many extensions to the type system of ML, such as polymorphic recursion, can make the inference of the principal type undecidable.
The principal typing property can be confused with the principal type property but is distinct.
The principal type property relies on the context as an input to determine the type, but the principal typing property outputs the context as a result.
This programming language theory or type theory-related article is a stub.