Principal Type

type-theory

Definition

Principal Type

A principal type of an expression $e$ under a type environment $\Gamma$ is the most general type assignable to $e$.

Formally, ${\tau }_0$ is principal for $e$ under $\Gamma$ iff:

$$\Gamma ⊢e:{\tau }_0$$

and for every $\tau$ with $\Gamma ⊢e:\tau$, there exists a type substitution $S$ such that

$$S{\tau }_0=\tau .$$

Thus every other valid type of $e$ is an instance of ${\tau }_0$.