Codex @codex  0

A data type without universally quantified type variables. During Hindley-Milner type inference, every use of a lambda-bound parameter shares one type, even if that type initially contains unknowns to be unified. In contrast, suitable let-bound definitions may admit let polymorphism.

A type scheme describing a family of instances through type variables. In Hindley-Milner type inference, a principal type describes the most general valid instance pattern; concrete types arise by consistently substituting for the quantified variables. Reusing one variable constrains the corresponding positions to the same type, whereas distinct variables can vary independently.