4 ms·

I am interested to hear about practical application of type theory and how it helped solve real world software and hardware problem better.

tel 12y ago
dons' suggestion, which I heartily second, is somewhat aimed at practical type theory: http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf Harper's thesis is that type theory is the backbone for language design. When you read his book you see him elaborate this and show how it applies to understanding and designing practical languages that work right.
psygnisfive 12y ago
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.
- raspasov 12y ago
  Thank you for the thoughtful response!

tel 12y ago

dons' suggestion, which I heartily second, is somewhat aimed at practical type theory: http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf Harper's thesis is that type theory is the backbone for language design. When you read his book you see him elaborate this and show how it applies to understanding and designing practical languages that work right.

psygnisfive 12y ago

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.

raspasov 12y ago
Thank you for the thoughtful response!