Aside from PFPL, which is oriented towards implementors of programming languages, type theory has practical uses in the act of programming itself. That is to sa

Aside from PFPL, which is oriented towards implementors of programming languages, type theory has practical uses in the act of programming itself. That is to say, with an adequate type theory, you can at a minimum use it to help you construct proofs that your programs do what you want them to do. But that's doable with any meta-system for certified programming, TT is just one particular meta-system that has some nice properties. The more common practical uses are: 1) If you're using a statically typed language, knowing some basic TT will let you understand the hows and whys of its type system. This is especially true of static langs that have richer type systems, like Haskell. 2) Rich type systems actually help you program! a lot of people complain that type systems merely complain when you mess up -- which is helpful, because you now know you've messed, but not completely helpful because it feels like the types don't help you. The truth is,, this is mostly true only of BAD type systems. A GOOD type system can guide you to the right answer by making the number of possible programs very tiny. Instead of infinitely many programs, there might just be one or two. A GOOD type system can guide you to the right answer by making it possible for the computer to write parts of the program for you because the types make it obvious what the options are at any moment program construction. For specific examples, you'd have to look around. I don't have any offhand (nor am I trying to convince you to learn TT!). Conal Elliot and Edward Kmett no doubt have plenty of good examples, or could tell you who does.