Why learn type theory?

[Craig Stuntz]

One thing that PFPL lacks is a preface or introduction explaining why one might want to learn this stuff. I guess by the time you're into your forth year at CMU, you pretty much know that. But the question does come up when I mention this group to other people, so I thought it might be worth exploring that idea. I don't have a great elevator pitch for it at the moment.

Of course, different people learn type theory for different reasons. For myself, I enjoy most kinds of math, but my principal motivation is the design and implementation of programming languages. Benjamin C. Pierce has a programming language-focused introduction which covers this angle fairly well in TTFP.

Answers to this cs.stackexchange question cover some of the extrinsic uses for type theory. http://cs.stackexchange.com/questions/48754/daily-applications-of-type-theory/48843#48843

Wikipedia's article on type theory is, perhaps surprisingly, not bad at all: https://en.wikipedia.org/wiki/Type_theory

Bob Harper does have a good, mathematically-focused introduction to the subject in his OPLSS 2012 talk: https://www.youtube.com/watch?v=9SnefrwBIDc&list=PL5FJyaC2WsVmiZHLVm7Z718vbHXUxLtHM&index=1

Feel free to chime in with your own opinion and other resources. I think it would be nice to produce summary of why it is worthwhile to learn this subject.

[Joseph Abrahamson]

I can try to wing it on a (longish) elevator pitch.

Formal languages, ways of writing down symbols which hold together in such a way to embody meaning, sit at the core of much of mathematics, programming, and language broadly. To give formal language a meaning is to translate the symbols and their collections into meaning within a domain such that the laws of the language reflect meaning in the domain. A type system is a formal language in its own right, but one designed to reflect meaning from the domain of other formal languages (statically) and, therefore, in studying them we can learn a lot about what governs formal languages generally.

It turns out that this idea provides benefits in mathematics and programming languages. In mathematics, the technique of types has given rise to several *alternative foundations to mathematics* of interest for philosophical and aesthetic reasons if nothing else. In programming languages, the technique of types gives rise to several (but not all) forms of *static analysis of code fragments* useful to describe and guide the logic of the program under constructions.

Studying type theory is to understand the techniques of types and can be a foundation for studying mathematical foundations in type theory or for better understanding (or even creating) programming languages which are amenable to and analyzed by systems of types. It also has a transformative effect on understanding formal languages, on working within them, on wielding logics. 

In my practical experience, types form an abbreviation to complex argument and design which can guide my work as a programmer often better than sketches, diagrams, and even smallish prototypes can. No matter the language I am working in by providing an abbreviated argument in the language of a friendly, nearby type system I can quickly begin to understand what it will take to build this thing and what it will take to be confident I've handled all of the edge cases.

[Shon Feder]

I think this a very nice pitch: it's admirably succinct and the focus on pragmatic issues makes it seem very approachable to me.

[Mark Farrell]

Hmm, I like this pitch. However, I feel like as though something about the role of type theory in constructive mathematics, the development of computer proof assistants, the formalization of mathematics on a computer, the modelling and verification of programming language design, the modelling of linguistic phenomena, recent connections to algebraic topology via category theory, etc. could be made a bit more explicit in the pitch.

[Jimmy Burrell]

Well done, Joseph. Succinct and to the point.