What is an uninhabited type?
&quot;Inhabited&quot; is the properly constructive notion of &quot;non-empty&quot;. 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.
&quot;Uninhabited&quot; 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.