13
$\begingroup$

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory.

In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator:

$$\frac{\Gamma \vdash M \colon 0}{\Gamma \vdash initial (M) \colon A}$$

From a denotational point of view, the equation $initial (M_1) = initial(M_2)$ is obvious (when the types make sense).

However, from that perspective I can also deduce that, when $M,M' \colon 0$, then : $M = M'$. This deduction seems stronger, although a particular model that shows it eludes me.

(I have some proof-theoretic intuition though: it doesn't matter which contradiction you use to obtain an inhabitant, but there might be different contradiction proofs.)

So my questions are:

  1. What are the standard equational laws for zero types?
  2. Are any of them classified as $\eta$ or $\beta$ laws?
$\endgroup$
12
$\begingroup$
  1. The standard equational rules for the empty type is, as you surmise, $\Gamma \vdash e = e' : 0$. Think of the standard set-theoretic model, where sets are interpreted by types: sum types are disjoint unions, and the empty type is the empty set. So any two functions $e,e' : \Gamma \to 0$ must also be equal, since they have a common graph (namely, the empty graph). .

  2. The empty type has no $\beta$ rules, since there are no introduction forms for it. Its only equational rule is an $\eta$-rule. However, depending on how strictly you wish to interpret what an eta-rule is, you may wish break this down into an $\eta$ plus a commuting conversion. The strict $\eta$-rule is:

    $$e = \mathrm{initial}(e)$$

    The commuting coversion is:

    $$C[\mathrm{initial}(e)] = \mathrm{initial}(e)$$

EDIT:

Here's why distributivity at the zero type implies the equality of all maps $A \to 0$.

To fix notation, let's write $!_A : 0 \to A$ to be the unique map from $0$ to $A$, and let's write $e : A \to 0$ to be some map from $A$ to $0$.

Now, the distributivity condition says that there's an isomorphism $i : 0 \simeq A \times 0$. Since initial objects are unique up to isomorphism, this means that $A \times 0$ is itself a initial object. We can now use this to show that $A$ itself is an initial object.

Since $A \times 0$ is an initial object, we know the maps $\pi_1 : A \times 0 \to A$ and $!_A \circ \pi_2$ are equal.

Now, to show that $A$ is an initial object, we need to show an isomorphism between it and $0$. Let's choose $e : A \to 0$ and $!_A : 0 \to A$ as the components of the isomorphism. We want to show that $e \circ !_A = id_0$ and $!_A \circ e = id_A$.

Showing that $e \circ !_A = id_0$ is immediate, since there is only one map of type $0 \to 0$, and we know that there is always an identity map.

To show the other direction, note $$ \begin{array}{lcll} id_A & = & \pi_1 \circ (id_A, e) & \mbox{Product equations} \\ & = & !_A \circ \pi_2 \circ (id_A, e) & \mbox{Since $A\times 0$ is initial} \\ & = & !_A \circ e & \mbox{Product equations} \end{array} $$

Hence we have an isomorphism $A \simeq 0$, and so $A$ is an initial object. Therefore maps $A \to 0$ are unique, and so if you have $e,e' : A \to 0$, then $e = e'$.

EDIT 2: It turns out the situation is prettier than I originally thought. I learned from Ulrich Bucholz that it's obvious (in the mathematical sense of "retrospectively obvious") that every biCCC is distributive. $\newcommand{\Hom}{\mathrm{Hom}}$ Here's a cute little proof:

$$ \begin{array}{lcl} \Hom((A + B) \times C, (A + B) \times C) & \simeq & \Hom((A + B) \times C, (A + B) \times C) \\ & \simeq & \Hom((A + B), C \to (A + B) \times C) \\ & \simeq & \Hom(A , C \to (A + B) \times C) \times \Hom(B, C \to (A + B) \times C) \\ & \simeq & \Hom(A \times C, (A + B) \times C) \times \Hom(B \times C, (A + B) \times C) \\ & \simeq & \Hom((A \times C) + (B \times C), (A + B) \times C) \end{array} $$

$\endgroup$
  • 1
    $\begingroup$ Regarding 1: I think of a zero type as an initial object. Initial objects may have multiple arrows into them, but can only have one arrow out of them. In other words, I don't immediately see any reason why being bi-CCC implies 0 to be subterminal. Is there one? $\endgroup$ – Ohad Kammar Jul 1 '11 at 16:14
  • $\begingroup$ Yes: the fact that the STLC with sums needs a distributive bi-CCC ($(X \times A) + (X \times B) \simeq X \times (A+B)$) to interpret it, and the uniqueness for the 0 type comes as the nullary version of that. (Try to write down the interpretation of the elimination rule for sums, and you'll see it.) $\endgroup$ – Neel Krishnaswami Jul 1 '11 at 16:36
  • $\begingroup$ I don't follow. The distributivity amounts to $initial : 0 \to A\times 0$ having an inverse. Why does that imply that $0$ is subterminal? $\endgroup$ – Ohad Kammar Jul 1 '11 at 17:03
  • $\begingroup$ Aha! Thanks for that proof! And for the patience, too! $\endgroup$ – Ohad Kammar Jul 3 '11 at 21:24
  • $\begingroup$ regarding edit 2: Left adjoints preserve colimits. If the category is Cartesian closed, then $(-)\times C$ is left adjoint to $(-)^C$ so $(A+B)\times C$ is the sum $A\times C + B\times C$. $\endgroup$ – Ohad Kammar Jul 28 '11 at 10:27
8
$\begingroup$

The equation $e = e' : 0$ only captures the fact that $0$ has at most one element so I don't think Neel is capturing the whole story. I would axiomatize the empty type $0$ as follows.

There are no introduction rules. The elimination rule is $$\frac{e : 0}{\mathtt{magic}_\tau(e) : \tau}.$$ The equation is $$\mathtt{magic}_\tau(e) = e' : \tau$$ where $e : 0$ and $e' : \tau$. Throughout $\tau$ is any type. The equation is motivated as follows: if you managed to form the term $\mathtt{magic}_\tau(e)$ then $0$ is inhabited by $e$, but this is absurd so all equations hold. So another way of achieving the same effect would be to pose the equation $$x : 0, \Gamma \vdash e_1 = e_2 : \tau$$ which is perhaps not so nice because it fiddles with the context. On the other hand, it shows more clearly that we are stating the fact that any two morphisms from $0$ to $\tau$ are equal (the $\Gamma$ is a distraction in a CCC).

$\endgroup$
  • 1
    $\begingroup$ Hi Andrej, the equation you suggest is derivable from the commuting conversion I gave. $\mathtt{magic}(e) = e'$ is derivable from $C[\mathtt{magic}(e)] = \mathtt{magic}(e)$, since $\mathtt{magic}(e)$ does not actually have to occur on the left term. The analogy is to $C[\mathtt{case}(e,x.\;e',y.\;e'')] = \mathtt{case}(e, x.\;C[e'], y.\;C[e''])$, where not using the result of a case-analysis is ok if you do the same in both branches. $\endgroup$ – Neel Krishnaswami Jul 1 '11 at 22:19
  • $\begingroup$ I should add, though, that I like the presentation with contexts better -- indeed, I think in general it's cleanest if you actually allow equations on sum values in the context! That's much nicer for actual proofs than games with commuting conversions, IMO. (IIRC, this is equivalent to adding the additional assumption of stable coproducts, but for all the models I can reasonably see caring about this holds.) $\endgroup$ – Neel Krishnaswami Jul 1 '11 at 22:23
  • $\begingroup$ Ah yes, excellent. It was too late for me to think about commuting conversions so I pretended you did not write that part. Now Ohad can have his pick. $\endgroup$ – Andrej Bauer Jul 2 '11 at 12:12
  • 1
    $\begingroup$ I was validating some structural ($\eta$, $\beta$, etc) rules in a class of models. While I know the set of equations I gave wasn't complete (you need CBPV with complex values and stacks for that), I wanted to at least capture the standard equations that will be used to prove completeness if I did have enough equations. In other words, I wanted the standard equational laws for zero types. $\endgroup$ – Ohad Kammar Jul 29 '11 at 6:18
  • 1
    $\begingroup$ There are no standard equational laws for zero types. Logicians have always been afraid of the empty universe of discourse, and computer scientists have always been afraid of the empty type. They even named a non-empty type "void" to deny the empty type. $\endgroup$ – Andrej Bauer Jul 29 '11 at 19:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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