# Which types are nihilistic?

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

A discussion on Twitter 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.

• Though this might be somewhat flexible, do you have a type system in mind for your question, say System F?
– cody
Feb 7, 2020 at 22:25
• System F sounds complicated. Try simply typed $\lambda$-calculus first. In any case, I think the question isn't that complicated. Feb 7, 2020 at 22:53
• could you please give an example of a term which belongs to the said nihilistic type? Feb 8, 2020 at 4:49
• @ApoorvIngle: $\lambda x : \mathsf{Empty} . x$ has type $\mathsf{Empty} \to \mathsf{Empty}$ and it contains the subexpression $x$ of type $\mathsf{Empty}$. Feb 8, 2020 at 6:56
• 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. Feb 8, 2020 at 7:08