type theory In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of ...

, a

type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...

is said to have the principal type property if, given a term and an environment, there exists a principal type for this term in this environment, i.e. a type such that all other types for this term in this environment are an instance of the principal type. The principal type property is a desirable one for a type system, as it provides a way to type expressions in a given environment with a type which encompasses all of the expressions' possible types, instead of having several incomparable possible types.

Type inference Type inference, sometimes called type reconstruction, refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some bran ...

for systems with the principal type property will usually attempt to infer the principal type. 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 In computer science, polymorphic recursion (also referred to as Robin Milner, Milner–Alan Mycroft, Mycroft typability or the Milner–Mycroft calculus) refers to a recursion (computer science), recursive parametric polymorphism, parametric ...

, can make the inference of the principal type undecidable. Other extensions, such as

Haskell Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...

generalized algebraic data type In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of a Parametric polymorphism, parametric algebraic data type (ADT). Ove ...

s, destroy the principal type property of the language, requiring the use of type annotations or the compiler to "guess" the intended type from among several options. The principal typing property requires that, given a term, there exist a typing (i.e. a pair with a context and a type) which is an instance of all possible typings of the term. 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.

References

Type theory Type inference {{type-theory-stub