3
$\begingroup$

If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we have the empty function in $\emptyset\to A$. This makes $\emptyset$ the initial object in the category of sets. By set extensionality, there is only this empty function and this also fits with cardinalities, where we like $|A^{\emptyset}|=|A|^{|\emptyset|}=1$. In logic, we usually take that form absurdum follows everything, ex falso quodlibet, and in the propositions interpretation for types, if $\bf 0$ denotes the empty type (or bottom type), we want a function ${\bf 0}\to \tau$ for all types $\tau$ too.

I've been told in some programs this would be done by defining alla

definition exfalso (a : Type) (x : 0) : a := "case x of -emptyspace-"

Now I try to construct the terms for function types involving the empty type over the standard theories you'd find in books, but I can't quite reproduce the good properties, see below. I wonder

Which type theories actually let you construct a term of a function type from the empty type, and then, is it unique?

My considerations (leading to more question) are this...

Take simply types lambda calculus. We have $(\lambda (x:\tau).x):\tau\to\tau$ and so $(\lambda (x:{\bf 0}).x):{\bf 0}\to{\bf 0}$. In any model of the type theory, this will be the empty function and so I'm okay with that. But how do I construct, from the typing rules of the theory, any type of ${\bf 0}\to{\bf \tau}$, where $\tau$ isn't ${\bf 0}$? And then, how is there only one? Depending on how the theory lets you define functions, I could imagine ${\bf 0}\to\mathrm{Nat}$ to have zero or an infinite number of terms (constant functions which can never take any input). I guess the cardinal arithmetic then only works out once we pass to the set theoretic model, where all those constant functions are, extensionally, the empty function. Is that right? In a type theory with booleans $\bf 2$, how many functions $\bf 0\to\bf 2$ are there? If $a,b:\bf 2$, are $\lambda x.a$ and $\lambda x.b$ generally two function of this type?

$\endgroup$
  • 2
    $\begingroup$ You need to be careful what kind of equality you have in mind when answering the question how many functions of type $\mathbf{0} \rightarrow \tau$ there are: syntactically e.g. $f = \lambda x^{\mathbf{0}}.3$ and $g = \lambda x^{\mathbf{0}}.17$ are distinct, but for extensional equalities $\cong$ they are equal, since for all inhabitants $M$ of $\mathbf{0}$ we have $fM \cong gM$. $\endgroup$ – Martin Berger Nov 30 '14 at 20:33
  • 1
    $\begingroup$ Related question: cstheory.stackexchange.com/questions/27303/… $\endgroup$ – Andrej Bauer Dec 2 '14 at 9:10
  • 1
    $\begingroup$ @MartinBerger, you still need to axiomatize something about $\mathbf{0}$ to be able to conclude that "for all inhabitants $M$ of $\mathbf{0}$ we have $f M \equiv g M$". And when you do, if you do it right, you don't need function extensionality, see my answer. $\endgroup$ – Andrej Bauer Dec 2 '14 at 9:40
  • $\begingroup$ @AndrejBauer Why do you need the equality (1) in your answer for something like $\lambda x^{\mathbf{0}}.17$? That term does not make use of $\mathsf{absurd}_A(E)$. All you need here is that $\mathsf{0}$ has no inhabitants. $\endgroup$ – Martin Berger Dec 2 '14 at 9:55
  • $\begingroup$ But how do you say "$\mathbf{0}$ has no inhabitants" in a type theory? Just because there is no constructor for $\mathbf{0}$ that does not mean you can actually use the fact that there are no inhabitants. You need an axiom somewhere. I used it to show that $f x$ and $g x$ are equal. Or to put it another way: how will you derive (using function extensionality if you wish) that any two functions $\mathbf{0} \to A$ are extensionally equal? I am not talking about a meta-theorem of the form "every two closed terms of type $\mathbf{0} \to A$ are equal", that's the wrong theorem to prove. $\endgroup$ – Andrej Bauer Dec 2 '14 at 10:28
2
$\begingroup$

I already answered how to construct such terms in a related question, so let me just amend that answer with some equations.

A standard type constructor which has constructors and eliminators, for instance $A \times B$ has pairing and projections, will have:

  • $\beta$-rules which says how destructors operate on constructors, for instance: $\pi_1 (a,b) \equiv a$,
  • $\eta$-rules which say that if we take a thing apart with destructors and put it back together we get the original thing, for instance: $(\pi_1\,u, \pi_2,u) = u$.

The empty type is special because it has no constructors, so where do equations come from? We can take the idea that $\mathbf{0}$ is the initial type and express it as an equation: $$\mathsf{absurd}_A(e_1) \equiv_A e_2 \tag{1}$$ where $\mathsf{absurd}_A : \mathbf{0} \to A$ is the eliminator (it could also be written as an empty case statement), $e_1 : \mathbf{0}$ and $e_2 : A$. The equation says that $\mathsf{absurd}_A(e_1)$ is equal to every term of type $A$, which is absurd, as it should be. The effect of the equation is that as soon as we have a variable $x : \mathbf{0}$ in the typing context, everything becomes trivial. In categorical language, slicing over $\mathbf{0}$ gives the terminal category -- which is just another way of saying that $\mathbf{0}$ is a terminal object.

We can now show that every two maps $f, g : \mathbf{0} \to A$ are equal, simply because $$x : \mathbf{0} \vdash f\,x \equiv \mathsf{absurd}_A(x) \equiv g\,x$$ and now by congruence rule for $\lambda$ and $\eta$-rule for functions $$f \equiv (\lambda x : \mathbf{0} \,.\, f\,x) \equiv (\lambda x : \mathbf{0} \,.\, g\,x) \equiv g.$$ Note however that (1) above is not the kind of equation that type theorists like, because it screwes up various algorithms for checking equality of terms.

$\endgroup$

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.