# 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?

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

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.