<p>[Note 2020-02-08: I updated the definition of nihilistic types so that it relies less on the type <code>Empty</code>.]</p>

<p>A <a href="https://twitter.com/andrejbauer/status/1225702461471690752?s=20" rel="nofollow noreferrer">discussion on Twitter</a> prompted the following question, which I have never seen considered before.</p>

<p><strong>Definition:</strong> Say that a type <code>T</code> is <strong>inhabited</strong> if there exists a closed term of type <code>T</code>, and  <strong>empty</strong> otherwise.</p>

<p>We assume that there is an empty type, or else the rest of the question is not very interesting. For instance, we might have the type <code>Empty</code> which is in fact empty.</p>

<p><strong>Definition:</strong> Say that a type <code>T</code> is <strong>nihilistic</strong> if every closed term <code>t</code> of type <code>T</code> contains a subexpression of an empty type.</p>

<p>I think (but have not thought carefully) that a type is nihilistic if and only if every <em>normalized</em> closed terms contains a subexpression of an empty type.</p>

<p>Clearly, every empty type is nihilistic.</p>

<blockquote>
  <p><strong>Question:</strong> <em>Which inhabited types are nihilistic, if any?</em></p>
</blockquote>

<p>For example <code>Empty → Empty</code> seems like a good candidate for a nihilistic type.</p>

CC BY-SA 4.0
2020-02-07T22:25:08.957Z
Though this might be somewhat flexible, do you have a type system in mind for your question, say System F?
cody
CC BY-SA 4.0
2020-02-07T22:53:45.147Z
System F sounds complicated. Try simply typed $\lambda$-calculus first. In any case, I think the question isn't that complicated.
Andrej Bauer
CC BY-SA 4.0
2020-02-08T04:49:30.950Z
could you please give an example of a term which belongs to the said nihilistic type?
Apoorv
CC BY-SA 4.0
2020-02-08T06:56:58.917Z
@ApoorvIngle: $\lambda x : \mathsf{Empty} . x$ has type $\mathsf{Empty} \to \mathsf{Empty}$ and it contains the subexpression $x$ of type $\mathsf{Empty}$.
Andrej Bauer
CC BY-SA 4.0
2020-02-08T07:08:47.937Z
Hi Andrej, I like this question. I think that `(T → Empty) → Empty` is also nihilistic by this definition, for any `T`, so that's a big source of nihilistic types.
Noam Zeilberger
CC BY-SA 4.0
2020-02-08T07:11:13.983Z
I think I got my definition slightly wrong, let me fix it.
Andrej Bauer
CC BY-SA 4.0
2020-02-08T07:57:57.540Z
This question also vaguely reminds me of the notion of "nowhere-unit typing" from http://noamz.org/papers/imploid-flows.pdf, which is inspired by the notion of "nowhere-zero flow" in graph theory.  That's defined as a property of typings rather than of types, but in a sense it corresponds to a dual form of "ultranihilism": a nowhere-unit typing of a term is one such that no subterm is assigned a type above the unit type, i.e., every subterm receives an empty type.
Noam Zeilberger
CC BY-SA 4.0
2020-02-08T15:29:51.090Z
Hmm.. if `T` is nihilistic, then so is `T' -> T`.  As for inhabited nihilistic types, not sure how to caracterize them exhaustively, but it seems that intuitively, if `T'` is empty, then `T' -> T` should be inhabited.
Stefan
CC BY-SA 4.0
2020-02-09T14:49:34.417Z
@Stefan: can you *prove* any of your observations?
Andrej Bauer
CC BY-SA 4.0
2020-02-09T23:24:54.957Z
@AndrejBauer: No, the first was wrong (I think it's true that `T' -> T` is nihilistic if `T` is empty since the term will be a function whose body is a term which must have type `T`, but it doesn't generalizes to the case where `T` is nihilistic) and the second just seems like it should be true (if you turn "`T'` is empty" into "there's a closed term `P : T' -> Empty`" and `Empty` accepts the principle of explosion, then you can use `P` to build a term of type `T' -> T`).
Stefan
CC BY-SA 4.0
2020-02-12T20:22:37.247Z
@AndrejBauer: Thanks for the example. I do not understand why you would need an `Empty` type, Isn't $\cdot, x : Empty \vdash M : \tau$ vacuously true for all $M, \tau$? Sec 3.2: https://doi.org/10.1016/0890-5401(88)90009-0 OR i am missing something..
Apoorv
<type-theory>
Which types are nihilistic?
Andrej Bauer
# Which types are nihilistic?

(Asked by: username_0 on 2020-02-07)

[Note 2020-02-08: I updated the definition of nihilistic types so that it relies less on the type `Empty`.]

A [discussion on Twitter](https://twitter.com/andrejbauer/status/1225702461471690752?s=20) prompted the following question, which I have never seen considered before.

**Definition:** Say that a type `T` is **inhabited** if there exists a closed term of type `T`, and **empty** otherwise.

We assume that there is an empty type, or else the rest of the question is not very interesting. For instance, we might have the type `Empty` which is in fact empty.

**Definition:** Say that a type `T` is **nihilistic** if every closed term `t` of type `T` contains a subexpression of an empty type.

I think (but have not thought carefully) that a type is nihilistic if and only if every *normalized* closed terms contains a subexpression of an empty type.

Clearly, every empty type is nihilistic.

> **Question:** *Which inhabited types are nihilistic, if any?*

For example `Empty → Empty` seems like a good candidate for a nihilistic type.

**Tags:** type-theory
> **Comments:**
> **username_1**: Though this might be somewhat flexible, do you have a type system in mind for your question, say System F?  
> **username_0**: System F sounds complicated. Try simply typed $\lambda$-calculus first. In any case, I think the question isn't that complicated.  
> **username_2**: could you please give an example of a term which belongs to the said nihilistic type?  
> **username_0**: @ApoorvIngle: $\lambda x : \mathsf{Empty} . x$ has type $\mathsf{Empty} \to \mathsf{Empty}$ and it contains the subexpression $x$ of type $\mathsf{Empty}$.  
> **username_3**: Hi Andrej, I like this question. I think that `(T → Empty) → Empty` is also nihilistic by this definition, for any `T`, so that's a big source of nihilistic types.  
> **username_0**: I think I got my definition slightly wrong, let me fix it.  
> **username_3**: This question also vaguely reminds me of the notion of "nowhere-unit typing" from http://noamz.org/papers/imploid-flows.pdf, which is inspired by the notion of "nowhere-zero flow" in graph theory.  That's defined as a property of typings rather than of types, but in a sense it corresponds to a dual form of "ultranihilism": a nowhere-unit typing of a term is one such that no subterm is assigned a type above the unit type, i.e., every subterm receives an empty type.  
> **username_4**: Hmm.. if `T` is nihilistic, then so is `T' -> T`.  As for inhabited nihilistic types, not sure how to caracterize them exhaustively, but it seems that intuitively, if `T'` is empty, then `T' -> T` should be inhabited.  
> **username_0**: @Stefan: can you *prove* any of your observations?  
> **username_4**: @AndrejBauer: No, the first was wrong (I think it's true that `T' -> T` is nihilistic if `T` is empty since the term will be a function whose body is a term which must have type `T`, but it doesn't generalizes to the case where `T` is nihilistic) and the second just seems like it should be true (if you turn "`T'` is empty" into "there's a closed term `P : T' -> Empty`" and `Empty` accepts the principle of explosion, then you can use `P` to build a term of type `T' -> T`).  
> **username_2**: @AndrejBauer: Thanks for the example. I do not understand why you would need an `Empty` type, Isn't $\cdot, x : Empty \vdash M : \tau$ vacuously true for all $M, \tau$? Sec 3.2: https://doi.org/10.1016/0890-5401(88)90009-0 OR i am missing something..  

---

## 0 answers

