Skip to main content
1 of 2
Couchy
  • 2.3k
  • 2
  • 9
  • 39

The role of constructors and eliminators can be understood through category theory. For every type former (for example $A\times B$, $A+B$, $A^B$, $\mathbb N$, etc...) we can ask

  • How can we construct a morphism into this type?
  • How can we construct a morphism out of this type?

We might as well call the morphisms into the type constructors and morphisms out of the type as eliminators.

The product type, for example, has the following universal property:

Given $P,Q$, there exists morphisms $\pi_1 : P\times Q\to P$, $\pi_2 : P\times Q\to Q$, such that for every object $R$, and morphisms $p : R\to P$, $q:R\to Q$ such that $\pi_1\circ p = \pi_2\circ q$, there exists a unique morphism $\langle p,q\rangle : R\to P\times Q$ such that $\langle p,q\rangle\circ \pi_1 = p$ and $\langle p,q\rangle\circ\pi_2 = q$.

From this, we see that the eliminators are $$\pi_1 : P\times Q\to P\\\pi_2 : P\times Q\to Q$$ and the only constructor is $$\frac{p : R\to P\quad q : R\to Q}{\langle p,q\rangle : R\to P\times Q}.$$

Similarly, the universal property of the natural numbers gives constructors $$z : 1\to \mathbb N\\ s : \mathbb N\to \mathbb N$$ and eliminators $$\frac{q : 1\to A\quad f : A\to A}{\text{rec}(q,f) : \mathbb N\to A}$$

Note that this is slightly different from require $f : \mathbb N\to A\to A$, but this is an equivalent, and often more convenient presentation.

So there is no reason why we can't have more than one eliminator, or that constructors/eliminators can't be more complicated. As a final example, function types have constructor $$\frac{f : A\to B}{\lambda f : B^A}$$ and eliminator $$\text{eval} : B^A\times A\to B,$$ where the only way to eliminate something of type $B^A$ is to pair it with something of type $A$.

Couchy
  • 2.3k
  • 2
  • 9
  • 39