<p>To me, type theory bridges programming with models and proof theories. In particular, I can use category theory to think about programming languages when the underlying type theory has a categorical model (e.g. the intuitionistic type theory by Martin Löf).</p>
<p>On the other hand, type theory to programming is like (point-set) topology to analysis -- it gives you global insights (about &quot;all programs that you <em>can</em> write&quot;) instead of specific results (about some particular programs that someone wrote).</p>

CC BY-SA 4.0
2021-07-12T04:59:07.943Z
2021-07-12T04:59:07.943Z
ice1000
<p>&quot;<em>Types are the leaven of computer programming; they make it digestible.</em>&quot; Robin Milner</p>

CC BY-SA 4.0
2021-07-11T22:56:33.560Z
2021-07-11T22:56:33.560Z
Martin Berger
<p>I think that you've asked two slightly different questions which are both worth answering. Other answers are good for the question in the title, but I want to focus on the word &quot;fundamental&quot; in your second question.</p>
<p>For large fragments of most mainstream programming languages, there exists a <a href="https://arxiv.org/abs/2102.04672" rel="nofollow noreferrer">native type theory</a> (discussed at nCafé: <a href="https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html" rel="nofollow noreferrer">1</a> <a href="https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.html" rel="nofollow noreferrer">2</a> <a href="https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_3_1.html" rel="nofollow noreferrer">3</a>) which describes the behavior of common syntactic elements like expressions and subroutines under evaluation. Constructing the native type theory for a particular language is a non-trivial adventure, but even basic versions have been enlightening. Thus, type theory is fundamental to programming and software engineering, even if we aren't yet experts at examining those foundations.</p>

CC BY-SA 4.0
2021-07-12T17:03:12.470Z
2021-07-12T17:03:12.470Z
Corbin
<p>I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants.</p>
<p>Now, this made me wonder - how fundamental is Type Theory exclusively to the study of Programming Languages? It would be great if someone could share their insights on the issue.</p>

CC BY-SA 4.0
2021-07-13T09:43:34.100Z
The term "type theory" is used with different shades of meaning, from referring exclusively to systems like MLTT and HOTT which are logics and not fully featured programming languages (e.g. restricted recursion) to any phase during compilation that 'somehow' tries to find bugs by classifying program parts according to what they do. Can you clarify which shade of meaning you have in mind?
Martin Berger
CC BY-SA 4.0
2021-07-13T12:00:26.943Z
Yeah I had the class of systems like MLTT and HoTT in mind.
Arjo
<pl.programming-languages><type-theory><dependent-type>
How does type theory change how one thinks about programming?
Arjo
# How does type theory change how one thinks about programming?

(Asked by: username_0 on 2021-07-11)

I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants.

Now, this made me wonder - how fundamental is Type Theory exclusively to the study of Programming Languages? It would be great if someone could share their insights on the issue.

**Tags:** pl.programming-languages, type-theory, dependent-type
> **Comments:**
> **username_1**: The term "type theory" is used with different shades of meaning, from referring exclusively to systems like MLTT and HOTT which are logics and not fully featured programming languages (e.g. restricted recursion) to any phase during compilation that 'somehow' tries to find bugs by classifying program parts according to what they do. Can you clarify which shade of meaning you have in mind?  
> **username_0**: Yeah I had the class of systems like MLTT and HoTT in mind.  

---

## 3 answers

### Answer by username_2 on 2021-07-12. Score: 5

To me, type theory bridges programming with models and proof theories. In particular, I can use category theory to think about programming languages when the underlying type theory has a categorical model (e.g. the intuitionistic type theory by Martin Löf).

On the other hand, type theory to programming is like (point-set) topology to analysis -- it gives you global insights (about "all programs that you *can* write") instead of specific results (about some particular programs that someone wrote).


---

### Answer by username_1 on 2021-07-11. Score: 4

"*Types are the leaven of computer programming; they make it digestible.*" Robin Milner


---

### Answer by username_3 on 2021-07-12. Score: 1

I think that you've asked two slightly different questions which are both worth answering. Other answers are good for the question in the title, but I want to focus on the word "fundamental" in your second question.

For large fragments of most mainstream programming languages, there exists a [native type theory](https://arxiv.org/abs/2102.04672) (discussed at nCafé: [1](https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html) [2](https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.html) [3](https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_3_1.html)) which describes the behavior of common syntactic elements like expressions and subroutines under evaluation. Constructing the native type theory for a particular language is a non-trivial adventure, but even basic versions have been enlightening. Thus, type theory is fundamental to programming and software engineering, even if we aren't yet experts at examining those foundations.


---

