What is an uninhabited type?

Question

https://en.wikipedia.org/wiki/Type_inhabitation

The wiki article above says,

To be sound, such a system must have uninhabited types.

What is the definition an uninhabitated type? Do all programming languages have uninhabited types? What would be an example in Haskell? Or C? Or Java? Or Python?

Answer 1

"Inhabited" is the properly constructive notion of "non-empty". The idea is that to demonstrate that a type is inhabited requires exhibiting a particular construction with that type, while 'non-empty' means merely demonstrating that it is impossible to demonstrate that there are no such constructions.

"Uninhabited" is the negation of this, and so is equivalent to being empty, even constructively.

Haskell does not have an uninhabited type. For instance undefined is a valid term of every type. C, Java and any language with general recursion is not going to qualify either, although C and Java have many other problems even being considered analogues of formal logic. Python doesn't even have types in the type theoretic sense (or it has a single type that classifies everything trivially).

The reason why void does not really qualify is that it is not a 'type with no values', but a type where you disallowed from naming/manipulating values, because those values would be trivial. It is analogous to the unit type, with one featureless value.

Answer 2

A type $A$ is inhabited if there exists a term $t$ of type $A$.

In typed programming languages with recursion all types are inhabited. Given any type A, consider the term f() where f : unit → A just calls itself:

function A f() { return f(); }

(Sure, f() cycles, but it has type A)

Side comment: the type void in C/C++ is inhabited, we just never get to observe its values. Indeed, since it is possible to implement a terminating function g : int → void, it cannot be the case that void is empty.

So, if we want to think of types as logical statements and their elements as proofs, then there ought to be a type that corresponds to False, and this type better be empty (because we cannot prove False).

Answer 3

An uninhabited type is a type which cannot have a representation at runtime no matter what you do, and enforces this is in a structural manner.

I'm going to use Rust as an example, because it does have uninhabited types. Rust has enums, for example:

enum Color {
    Red,
    Yellow,
    Rgb(u8, u8, u8),
}

And you can specify a color, e.g. Color::Red or Color::Rgb(255, 255, 255).

But what if you declare an empty enum:

enum Never {}

How would you construct a value of this enum? What goes after Never::?

The answer is "it cannot be done". There is no possible representation of Never in the language. This makes the type uninhabited.

---

What does "in a structural manner" mean? Another way to put it is "even disregarding encapsulation boundaries". A lot of code is written to uphold certain invariants outside of an encapsulation boundary.

For example, consider a file where the only contents are:

pub struct MyType(());

This type has no attached constructors, and the module doesn't have any functions that return MyType. In other words, MyType can be named as a type but cannot be constructed.

However, MyType can be represented at runtime, just not created at runtime. In other words, the lack of constructability of MyType is enforced via encapsulation boundaries rather than it being a property of the structure of MyType itself. This means that MyType is not uninhabited. But it might be the best you can do in many languages.

---

This is related to why enums are called "sum types" and structs are called "product types" -- the identity element of the sum operation is zero, and the identity element of the product operation is one.