Why study type theory?
Type theories in which every type is inhabited are far from being useless. True enough, through the eyes of logic they are inconsistent, but there are other things in life apart from logic.

A general purpose programming language has general recursion. This allows it to populate every type, but we would not conclude from this fact that programming is a useless exercise, would we?

In the theory of programming languages types are used as a safety feature ("A well typed program does not go wrong" sad a famous man), as an organizational device, and a tool for program analysis. None of these purposes requires that there be an empty type.

Type inference is only one aspect in which type theory relates to programming languages. Some other uses of types in programming languages are:


Specification: before the programmer starts writing code he writes down the type of the program he is after. He specifies (although usually not fully) what he wants. This is also useful for communication between programmers.
Modularization: when several pieces of software need to be assembled together we have to make sure they fit. One way of doing this is to speficy the interfaces through which the pieces connect. This can be done with types.


Dependent types appear in programming languages, but in limited form (because general dependent types cannot be handled automatically by the compiler). For instance, an ML-style module is a dependent sum, while a polymorphic type can be seen as a dependent product.

You ask what is gained by studying type theory? Clarity of mind where there was only Visual Basic before. Ability to write 30000 lines of code without making it look like the Flyng Spaghetti Monster. Inner peace and feeling of superiority over the unfortunate users of Lisp.