5
$\begingroup$

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)

$\endgroup$
  • 5
    $\begingroup$ You seem to acquire your "aha" moments mostly through stackexchange. $\endgroup$ – Sasho Nikolov Mar 11 '15 at 22:36
  • $\begingroup$ What is "type theory per se"? $\endgroup$ – Huck Bennett Mar 11 '15 at 22:50
  • $\begingroup$ @SashoNikolov - You are right. I'm mostly self taught as far as ToC is concerned. Cstheory.SE is the only place I'm aware of where group of qualified people have helped me attain multiple "aha" moments :-) $\endgroup$ – PhD Mar 12 '15 at 2:26
  • $\begingroup$ @HuckBennett - I meant the part of TT other than type inference. $\endgroup$ – PhD Mar 12 '15 at 2:27
  • $\begingroup$ @PhD The claim that "any kind of (automated) formal reasoning about [realistic programming languages is] nearly impossible" is misleading. You can reason about them, although the way the typing system plays a part in this is a bit different from type-theory. $\endgroup$ – Martin Berger Mar 12 '15 at 9:21
13
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Is "sad a famous man" meant to be "said Robin Milner"? If not, who else is supposed to have said this? $\endgroup$ – András Salamon Mar 12 '15 at 16:23
  • $\begingroup$ This makes sense. Two questions: 1.) Any good examples links for the specification part? 2.) We can do both, specification and modularization in OO languages. What really is the type theoretic insight in this case other than compile-time type checking? $\endgroup$ – PhD Mar 12 '15 at 17:33
  • $\begingroup$ OO is a special case of type theory. $\endgroup$ – Andrej Bauer Mar 12 '15 at 22:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.