What is an uninhabited type?

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?

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

StackExchange Computer Science Q#134215, answer score: 3