# Constructing terms of function types out of the empty type

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?

• 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$. Nov 30, 2014 at 20:33
• Related question: cstheory.stackexchange.com/questions/27303/… Dec 2, 2014 at 9:10
• @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. Dec 2, 2014 at 9:40
• @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. Dec 2, 2014 at 9:55
• 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. Dec 2, 2014 at 10:28

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 an initial 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.

In a plain type theory with just dependent functions and a universe, you can define:

$$\textbf 0 \equiv (A: \textrm{Type}) \rightarrow (B: \textrm{Type}) \rightarrow A \rightarrow B$$

Then you get a map: $$\textrm{0m} : (X: \textrm{Type}) \rightarrow \textbf 0 \rightarrow X$$ $$\textrm{0m}\,\, X\,\, z\, \equiv z\,\, \textbf 0\,\, X\,\, z$$

Note: This definition is impredicative, and thus requires some kind of super universe or other means to avoid Girard's paradox.

• Thanks. How's the bracketing in "$𝑧\ 0\ 𝑋\ 𝑧$"? I don't quite understand the role of passing something to $z$. Aug 29, 2021 at 12:22
• @Nikolaj-K Since $\textbf 0$ is really a function type, $z : \textbf 0$ is a function taking 3 parameters. Thus, we pass it 2 types and a term of the 1st type (as per the signature). The bracketing works as in Haskell, left associativity of calls. Aug 30, 2021 at 18:19
• IMO normally we name $0m$ as 'absurd' or $\bot\text{-elim}$ or something. Did you invent the name yourself, or is it borrowed somewhere else? Sep 3, 2021 at 18:27
• @ice1000 Yeah, I use it in my notes (as an abbreviation of "0 map"), and I have subcosciously used it here. Should I edit the answer? Sep 6, 2021 at 17:41