principal type


principal type

The most general type of an expression. For example, thefollowing are all valid types for the lambda abstraction(\\ x . x):

Int -> IntBool -> Bool(a->b) -> (a->b)

but any valid type will be an instance of the principal type:a -> a. An instance is derived by substituting the same typeexpression for all occurences of some type variable. Theprincipal type of an expression can be computed from those ofits subexpressions by Robinson's unification algorithm.