3
$\begingroup$

What is an eliminator?

  • Are there any differences between an eliminator and an elimination form (such as $\pi_1$ and $\pi_2$ for binary products)?
  • Does every type have exactly one?
  • Is the type of the eliminator completely determined by the types of the constructors?

The motivation for this question is: I'm trying to understand a $\Pi$-type definition of $\mathbb{N}$ quoted from an answer on this site.

The definition, with the notation changed only slightly, is given below.

$$ \mathbb{N} \;\;{\small\text{is defined as}}\;\; \bigg(\Pi (N : *) \mathop. \Pi (A : *) \mathop. A \to (N \to A \to A) \to (N \to A)\bigg) : * $$

According to the body of the answer, $A \to (N \to A \to A) \to (N \to A)$ is the type of the eliminator of the natural numbers.

$\endgroup$
8
  • 3
    $\begingroup$ I don't understand the question. What exactly are you asking? $\endgroup$ Feb 12, 2022 at 5:04
  • 2
    $\begingroup$ The definition of $f$ is not correct (it loops). You need two cases: $f(x, g, 0) = x$ and $f(x, g S(n)) = g(x, g, f(x, g, n))$. The function $f$ is realizes primitive recursion, and is the proof relevant counter-part of induction. I don't understand what you're asking, by the way. $\endgroup$ Feb 12, 2022 at 7:14
  • 2
    $\begingroup$ I should point out that the definition of $\mathbb{N}$ given is not complete. It is insufficient for showing that $\mathbb{N}$ has the desired properties. You need something else in addition, such as parametricity. $\endgroup$ Feb 12, 2022 at 7:15
  • 2
    $\begingroup$ I misspoke: eliminators are proof relevant eliminations. Regarding $S$ and $0$, of course you need to define them as suitable $\lambda$-terms. And the recursor can also be similarly defined using just $\lambda$-terms. $\endgroup$ Feb 12, 2022 at 8:19
  • 2
    $\begingroup$ A constructor for X is a way of making things of type X, and an eliminator for X is a way of using things of type X to make other stuff (i.e. a way to make functions from X to other types). Is that the answer you're looking for? $\endgroup$ Feb 12, 2022 at 15:49

1 Answer 1

3
$\begingroup$

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$.


It's also interesting to note that $\mathbb N$ belongs to a class of inductive types, which means the eliminator has a specific form. $\newcommand{\mc}{\mathcal}$ Indeed, for an inductive type defined by an endofunctor $F:\mc C\to\mc C$ (where $\mc C$ is the category of types) (in the case of $\mathbb N$, $F(X) := X\times (X\to X)$), the inductive type is defined to be the initial algebra for $F$. If $A$ is initial for $F$, this briefly means that for every other type $X$, there is a unique map of algebras $F(A)\to F(X)$. This map is the eliminator for $A$.

$\endgroup$
5
  • $\begingroup$ How does this fit with the picture where product types have only one eliminator (of type $(P \to Q \to R) \to P \times Q \to R$? $\endgroup$ Feb 13, 2022 at 18:59
  • $\begingroup$ @JasonGross Should $R$ be universally quantified? $\endgroup$
    – Couchy
    Feb 13, 2022 at 19:08
  • $\begingroup$ all type variables in eliminators are always universally quantified. So, yes $R$ (and $P$ and $Q$) is universally quantified. $\endgroup$ Feb 14, 2022 at 16:55
  • $\begingroup$ The two pictures corresponds to viewing the product type as positive or negative. In polarized notation we can write them as $\otimes$ and $\&$, respectively. $\endgroup$
    – Trebor
    Feb 15, 2022 at 7:41
  • $\begingroup$ In linear logic they are not equivalent, but with weakening and contraction, they are, so we often confuse them. $\endgroup$
    – Trebor
    Feb 15, 2022 at 7:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.