Type

Definition

In type theory, a type is a primitive notion representing a collection of mathematical objects, called terms, which share a common structure or behavior. We denote that a term $a$ belongs to a type $A$ with the judgment $a:A$. Types serve as the foundational building blocks for formal logic and computation, where the Curry-Howard correspondence relates types to propositions and terms to proofs.

Example

An common example is that of function types. The type $A\to B$ represents the collection of mappings from domain $A$ to codomain $B$. For the addition operation on natural numbers $\mathbb{N}$, the type signature is:

$+:\mathbb{N}\to \mathbb{N}\to \mathbb{N}$

This signature specifies that $+$ is a curried function taking two arguments of type $\mathbb{N}$ and producing a result of type $\mathbb{N}$. In dependent type theory, types may also depend on terms, generalizing the function type to the Pi type ${\prod }_{x:A}B(x)$.

References

martin-lof1984-mltt hott2013-book nederpelt2014-type-theory