λΠ-calculus

Π-types

The dependent function space, dependent product space, or simply Π-type $\text{pitype}\mathrm{Type}xtm$ generalises over the classic function type $s\to t$ as well as familiar parametric polymorphism constructs, such as the universal quantifier type $\forall \alpha .M$ of System F [cite:@loh2007simply]. In contrast to universal quantification, Π-types can abstract over more than just types — e.g. values. Π-types thus allow for the definition of types which depend on values.

$$s\to t\equiv \text{pitype}\mathrm{Type}\_st,$$

where $\_$ does not occur in $t$.

$$\forall \alpha .M\equiv \text{pitype}\mathrm{Type}\alpha \text{Type}M$$

References

• [cite:@loh2007simply]