Definition
Principal Type
A principal type of an expression
under a type environment is the most general type assignable to . Formally,
is principal for under iff: and for every
with , there exists a type substitution such that Thus every other valid type of
is an instance of .