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?

  • $\begingroup$ I believe that void is an uninhabited type. $\endgroup$ – Yuval Filmus Jan 11 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$ – Musa Al-hassy Jan 11 at 14:24

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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