<p>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.</p>
<p>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?</p>
<p>In the theory of programming languages types are used as a <em>safety feature</em> (&quot;A well typed program does not go wrong&quot; sad a famous man), as an <em>organizational device</em>, and a tool for <em>program analysis</em>. None of these purposes requires that there be an empty type.</p>
<p>Type inference is only one aspect in which type theory relates to programming languages. Some other uses of types in programming languages are:</p>
<ul>
<li><p><strong>Specification:</strong> before the programmer starts writing code they writes down the type of the program he is after. They <em>specify</em> (although usually not fully) what they wants. This is also useful for communication between programmers.</p>
</li>
<li><p><strong>Modularization:</strong> when several pieces of software need to be assembled together we have to make sure they fit. One way of doing this is to <em>speficy the interfaces</em> through which the pieces connect. This can be done with types.</p>
</li>
</ul>
<p>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.</p>
<p>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.</p>

CC BY-SA 3.0
2015-03-12T16:23:12.827Z
Is "sad a famous man" meant to be "said Robin Milner"?  If not, who else is supposed to have said this?
András Salamon
CC BY-SA 3.0
2015-03-12T17:33:43.813Z
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?
PhD
CC BY-SA 3.0
2015-03-12T22:50:29.973Z
OO is a special case of type theory.
Andrej Bauer
CC BY-SA 4.0
2015-03-12T07:47:35.423Z
2022-11-15T09:47:22.757Z
2022-11-15T09:47:22.757Z
Andrej Bauer
<p>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?</p>

<p>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.</p>

<p>Now, functional programming (FP) languages like Haskell, Scala that can be used in large projects are based on an <em>inconsistent logic</em> - 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.</p>

<p>So my question is trying to understand the bigger role i.e., interplay of TT <em>and</em> 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. </p>

<p>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 <em>aha</em> understanding that one gains at a deeper level - since very little of TT's power/awesomeness actually gets carried over to <em>commercially viable</em> FP languages (and not Agda, Epigram etc.,)?</p>

<p><em>(PS: Here's a similar question on <a href="https://math.stackexchange.com/questions/567265/why-is-it-worth-spending-time-on-type-theory">Math.SE</a>- 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)</em></p>

CC BY-SA 3.0
2015-03-11T22:36:55.293Z
You seem to acquire your "aha" moments mostly through stackexchange.
Sasho Nikolov
CC BY-SA 3.0
2015-03-11T22:50:04.000Z
What is "type theory per se"?
Huck Bennett
CC BY-SA 3.0
2015-03-12T02:26:38.863Z
@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 :-)
PhD
CC BY-SA 3.0
2015-03-12T02:27:37.753Z
@HuckBennett - I meant the part of TT other than type inference.
PhD
CC BY-SA 3.0
2015-03-12T09:21:01.700Z
@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.
Martin Berger
<soft-question><computability><type-theory><big-picture><intuition>
Why study type theory?
PhD
# Why study type theory?

(Asked by: username_0 on 2015-03-11)

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](https://math.stackexchange.com/questions/567265/why-is-it-worth-spending-time-on-type-theory)- 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)*

**Tags:** soft-question, computability, type-theory, big-picture, intuition

> **Comments:**
> **username_1**: You seem to acquire your "aha" moments mostly through stackexchange.  
> **username_2**: What is "type theory per se"?  
> **username_0**: @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 :-)  
> **username_0**: @HuckBennett - I meant the part of TT other than type inference.  
> **username_3**: @username_0 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.  

---

## 1 answers

### Answer by username_4 on 2015-03-12. Score: 23

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.

> **Comments:**
> **username_5**: Is "sad a famous man" meant to be "said Robin Milner"?  If not, who else is supposed to have said this?  
> **username_0**: 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?  
> **username_4**: OO is a special case of type theory.  

---

