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$
7
  • 3
    $\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$ Nov 30, 2014 at 20:33
  • 1
    $\begingroup$ Related question: cstheory.stackexchange.com/questions/27303/… $\endgroup$ Dec 2, 2014 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$ Dec 2, 2014 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$ Dec 2, 2014 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$ Dec 2, 2014 at 10:28

2 Answers 2

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Thanks. How's the bracketing in "$𝑧\ 0\ 𝑋\ 𝑧$"? I don't quite understand the role of passing something to $z$. $\endgroup$
    – Nikolaj-K
    Aug 29, 2021 at 12:22
  • $\begingroup$ @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. $\endgroup$
    – DrunkCoder
    Aug 30, 2021 at 18:19
  • $\begingroup$ 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? $\endgroup$
    – ice1000
    Sep 3, 2021 at 18:27
  • $\begingroup$ @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? $\endgroup$
    – DrunkCoder
    Sep 6, 2021 at 17:41

Your Answer

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

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