In type theory, a type system 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 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, can make the inference of the principal type undecidable. Other extensions, such as Haskell's generalized algebraic data types, 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 notion was introduced by Curry and Feys around 1958,[1] under the name of "principal functional character".[2] The "principal type" name (as well as "type scheme") is due to Hindley (1969).[2]
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.[3]
The principal typing property allows "compositional" type reasoning, meaning the analysis can be performed on the parts in any order. The Hindley–Milner type system is not compositional in this sense due to how let val x = e1 in e2 end is typed first by evaluating the type of e1 and using the result to type e2.[4] Thus, it is said that ML has principal types but not principal typings.[3] The simply typed lambda-calculus, on the other hand, has both of these properties.[3][4]
Generally speaking, type systems based on intersection types also have the principal typings property.[5] This may not be computable, although if one limits intersections to rank-2[3] or with the introduction of some additional variables to any finite rank, then principal typings are computable for intersection types.[6] These type systems been proposed for various applications, typically focused on incremental compilation[7][8][3] or gradual typing.[9]
References
^according to: Daniel Leivant, "Polymorphic type inference", POPL 1983
^ abR. Hindley, "The Principal Type-Scheme of an Object in Combinatory Logic", Transactions of the American Mathematical Society, Vol. 146 (Dec., 1969), pp. 29-60
^ abWells, J.B. (2003). "The Essence of Principal Typings". ICALP '02: Proceedings of the 29th International Colloquium on Automata, Languages and Programming. pp. 913–925.
^Pierce, Benjamin Crawford (1992). Programming with intersection types and bounded polymorphism. Carnegie Mellon University (PhD Thesis). p. 24.
^Kfoury, A.J.; Wells, J.B. (January 2004). "Principality and type inference for intersection types using expansion variables". Theoretical Computer Science: 1–70.
^Ancona, Davide; Zucca, Elena. "Principal typings for Java-like languages". POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages.
^Damiani, Ferruccio. "Rank 2 intersection types for modules". PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declarative programming.
^Castagna, Giuseppe; Lanvin, Victor. "Gradual Typing with Union and Intersection Types". ICFP 2017.
