1
$\begingroup$

I would like some help choosing the rules for the empty type. I am trying to setup a typed lambda calculus with sums like in

Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums

Except, I am being explicit about type formation (that is, I am keeping track of a context, and applying rules to form types, in a similar way to page 554 of the homotopy type theory book). For example, here is one of my introduction rules for sum types:

$$\begin{array}{c} \Gamma\vdash x:A\hspace{1em}\Gamma\vdash B:\text{type}\\ \overline{\Gamma\vdash\text{inl}_{A+B}(x):A+B} \end{array}$$

My questions are (1) whether the following is appropriate for being an elimination rule for the empty type:

$$\begin{array}{c} \underline{\Gamma\vdash A:\text{type}\hspace{1em}\Gamma\vdash e:0}\\ \Gamma\vdash\text{abort}_{A}(e):A \end{array}$$

And (2) whether the following is appropriate for being a computation rule for the empty type:

$$\begin{array}{c} \Gamma,e:0\vdash x:A\\ \overline{\Gamma,e:0\vdash\text{abort}_{A}(e)=x:A} \end{array}$$

And if not, then what rules should I use ? I do not think my situation is helped by the fact that I do not understand the equational rule for the empty type in the above reference.

$\endgroup$
2
  • $\begingroup$ Terminologically, I would argue that there is no "computation" ($\beta$) rule for the empty type. A computation rule in general says that when you apply an elimination form to an introduction form, you get out the inputs of the introduction form. But there are no introduction forms for the empty type, hence there can be no computation rule. Your rule is more of a uniqueness ($\eta$) rule. $\endgroup$ Nov 20, 2020 at 15:32
  • 1
    $\begingroup$ I would be wary of including a rule like this in the judgmental equality. For instance, $abort_A(e) = suc(abort_A(e))$, so it can be unfolded indefinitely. This is a concrete reason not to consider it a "computation" rule like Mike said, since it makes computation diverge in inconsistent contexts (although that may not matter for your particular case). I have seen theories where judgmental equality becomes trivial in certain contexts (e.g. Logical Relations as Types), but it is more restrictive than "the context is inconsistent." $\endgroup$
    – Dan Doel
    Nov 20, 2020 at 23:20

1 Answer 1

1
$\begingroup$

Your elimination rule is correct. In a simple type theory (i.e. without dependent types), you could write the computation rule for the empty type as the following (note that this matches the rule in the paper you link, though the notation is a little different, and I've been explicit about the type $A$). $$\frac{\Gamma \vdash e : 0 \qquad \vdash A\ \mathrm{type} \qquad \Gamma \vdash a : A}{\Gamma \vdash \mathrm{abort}_A(e) \equiv a : A}$$ You will usually not have contexts of the form $\Gamma, x : A$ (or $\Gamma, e : 0$) in a simple type theory unless you're describing a variable-binding operator (like $\lambda$-abstraction). In the HoTT book, there are more rules of this form because they have dependent types (where you have to take more care about variable binding).

$\endgroup$
5
  • $\begingroup$ Thanks. But doesn't that say each element of A equals $abort_A (e)$ ? Also, is it ok to write $\Gamma \vdash A \_ type$ instead of $\vdash A \_ type$ above the line ? $\endgroup$ Nov 20, 2020 at 11:48
  • $\begingroup$ Essentially yes: if you have a term of the empty type in some context (which shouldn't be possible in general!), then every type is trivially inhabited in that context. (But this should never happen in a general context unless your type theory is unsound.) Categorically, this is saying that initial objects in distributive categories (and hence cartesian-closed categories) are strict. Yes, writing $\Gamma \vdash A\ \mathrm{type}$ is fine too: it's just not necessary in a simple type theory where the types cannot depend on the context. $\endgroup$
    – varkor
    Nov 20, 2020 at 11:54
  • $\begingroup$ Very interesting. $\endgroup$ Nov 20, 2020 at 11:59
  • 1
    $\begingroup$ It may be worth pointing out that the reason rules are usually phrased the way varkor did it, rather than the way that the OP did it with $e:0$ in the context below the line, is to make substitution admissible. $\endgroup$ Nov 20, 2020 at 15:34
  • $\begingroup$ I see, thanks . $\endgroup$ Nov 21, 2020 at 11:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .