Why study type theory?

Question

After reading the literature on type theory (especially the constructive kind - CTT) I'm left wondering "why" should one study type theory, specifically within the confines of "computing" in general?

I understand how type systems (loosely speaking) were created to avoid various paradoxes and the correspondence between philosophy, logic, lambda-calculus and the how it comes together for CTT to serve as a foundation of mathematics. Fair enough.

Now, functional programming (FP) languages like Haskell, Scala that can be used in large projects are based on an inconsistent logic - making any kind of (automated) formal reasoning about them nearly impossible - but that seems to be the very need/power of TT! E.g., theorem proving and proof assistants and the notion of programs as proofs. But none of this carries over to FP languages.

So my question is trying to understand the bigger role i.e., interplay of TT and computing taken together. Most FP languages have just "good enough" type systems (e.g., Haskell > Java). The problem of "type inference" is in some way similar to "logical inference" and doesn't seem all that complicated for simple types. I'm guessing things become undecidable after a particular threshold. Fair enough. I understand its need till this level. But is that it? It seems one can understand type systems/inference without really diving into the details of TT per se.

Since FP languages don't really borrow much from TT other than "type systems/inference", why bother studying the theory in depth especially within computation theory? It seems that after studying a good deal of TT, for fun, I'm still left wondering "what did I gain" - both as a theoretician and a software practitioner? What "is" the aha understanding that one gains at a deeper level - since very little of TT's power/awesomeness actually gets carried over to commercially viable FP languages (and not Agda, Epigram etc.,)?

(PS: Here's a similar question on Math.SE- but that's from a mathematical POV and I get that from that perspective. I'm struggling to see TT's importance when concerned about computing and software engineering in general)

Answer 1

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 they writes down the type of the program he is after. They specify (although usually not fully) what they 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.