I would like to know about examples of type theory applications. For what purpose was type theory invented? Can you give me some motivations?

Question

I'm an undergraduate math student.

Answer 1

Type Theory was invented as a possible foundation for mathematics. It was later tied to the lambda calculus, and is now a prime example of the Curry-Howard Correspondence. Later yet, it was connected to category theory (especially higher category theory), and is a very active field of research. For more information, see here or here.

Here are some quick applications:

• Foundations of mathematics (as a computer friendly alternative to set theory)
• Programming Language theory (programming languages are made safer by type systems)
• Homotopy theory (somewhat surprisingly, cf. HoTT)

If you want more resources, a friend of mine made a github page all about learning type theory. Reading through the table of contents will give you an idea of why people care, and it will also have direct links to resources for learning the relevant material:

here's the github page

good luck!

---

I hope this helps ^_^