5
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ I believe that void is an uninhabited type. $\endgroup$ Jan 11, 2021 at 10:54
  • $\begingroup$ @YuvalFilmus What about void pointers or functions "returning" void ;-) @Hank Consider dependent types, or type families in Haskell, such as the type of all m-by-n matrices. Then when m and n are negative integers, then the type of m-by-n matrices is uninhabited. In programming, Fin n is used to denote the type of the first n-many non-negative integers; then Fin 0 is empty/uninhabited. $\endgroup$ Jan 11, 2021 at 14:24
  • 1
    $\begingroup$ @YuvalFilmus: no, void is just a misnomer for the unit type. If void were uninhabited, it would be impossible to write a function of type int → void. $\endgroup$ Jul 28, 2023 at 18:42

3 Answers 3

3
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$
7
  • $\begingroup$ I feel like while your definition of uninhabited is technically correct, there is a valuable distinction to be drawn between types that can actually be constructed and types that cannot. For example, a sum type variant that contains a type that cannot be constructed at all, can be eliminated from consideration while memory layout is being determined. $\endgroup$
    – rain
    Jul 28, 2023 at 19:42
  • $\begingroup$ What is your point? $\endgroup$ Jul 28, 2023 at 22:44
  • $\begingroup$ My point is that "In typed programming languages with recursion all types are inhabited" is not a very useful practical definition. In typed programming languages with recursion, there is a useful distinction between types which can have an actual value be constructed for them, and types which cannot. I don't know if there's a more specific term for it, but as a practitioner I call the latter "uninhabited" and everyone around me understands what I mean. $\endgroup$
    – rain
    Jul 29, 2023 at 2:55
  • $\begingroup$ Yes, there is a more specific way of saying what you are trying to say. One way to give operational semantics is to define a notion of value, which differs from expression, and to set up semantics so that closed expressions evaluate to values. In such languages there can be types that have no values, for instance if they allow empty sum types. ... $\endgroup$ Jul 29, 2023 at 21:27
  • $\begingroup$ ... However, this distinction depends on having a suitable notion of value, as well as on evaluation strategy – it is hardly an appropriate thing to mention when the OP is struggling with basics. It is better for the first to see how recursion is used to inhabit any type, and not to drag in nuances of operational semantics, $\endgroup$ Jul 29, 2023 at 21:27
2
$\begingroup$

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.

$\endgroup$

Your Answer

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

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