= Principal type
A <principal type> is a most general valid type scheme: every other valid typing of the expression is obtained by substituting types for its quantified type variables, subject to any declared class constraints. For example, `\s x f y -> f (s y x)` has type `(u -> v -> w) -> v -> (w -> r) -> u -> r`; the application constraints require precisely these connections and no equality between the four type variables. A concrete typing is an instance, not evidence that the expression needs that particular type.
Back to article page
