Type Theory¶

8 domain-specific abstractions whose origin domain is Type Theory.

Container (type theory) — A shape-and-positions representation of strictly positive collection-like type constructors in dependent type theory.
Identity type — A type-theoretic proposition whose inhabitants witness equality between two terms of a type.
Intersection type — A type assigned to values satisfying multiple type descriptions simultaneously, written as an intersection such as sigma ∩ tau.
Type constructor — A type-level operator that builds a new type from zero or more argument types, such as function, product, list or parameterized generic constructors.
Type variable — A formal variable ranging over types, enabling polymorphic expressions and quantified type schemes without denoting a mutable runtime storage location.
Typed lambda calculus — A lambda-calculus formalism assigning types to variables and terms and restricting abstraction and application through typing rules.
Typing rule — A formal inference rule specifying how types of component expressions and contextual assumptions justify a type judgment for a larger syntactic construction.
Unit type — A type with exactly one inhabitant up to equality, carrying no information beyond successful presence or completion.