6
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$ Jul 13 at 9:43
  • $\begingroup$ Yeah I had the class of systems like MLTT and HoTT in mind. $\endgroup$ Jul 13 at 12:00
5
$\begingroup$

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).

$\endgroup$
3
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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 (discussed at nCafé: 1 2 3) 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.

$\endgroup$

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.