7 ms·

So you want to learn type theory

169 points by psygnisfive 12y ago

dons 12y ago
Good list, I'd also recommend http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf for something designed for newcomers to the field
- jonsterling 12y ago
  Yeah, that's a great book for learning how the methodology of type theory and judgemental presentations can be used in presenting practical/everyday PL concepts. Incidentally, I spoke with bob and he mentioned he wants to write another book some day that does the same thing, but for "pure" type theory. I think that'd be a great book, particularly given bob's unique perspective on type theory (having spent a lot of time on both sides of the fence—proof theory vs realizability). but don't count on it anytime soon!
  - psygnisfive 12y ago
    I'll start added recommendations to the link, so keep 'em coming.
- Alex25 12y ago
  Thanks a lot! Useful!
geoka9 12y ago
Ask yourself why. You want to do CS, prove theorems, do theoretical research? Then, by all means, go for it! It's hip and you use a functional language to write software? Well... It's probably just a whim. But sure, give it a try.
- k__ 12y ago
  Well, of you want do implement a type system it could help too.
  - agumonkey 12y ago
    I just finished writing a tiny sexp based lambda interpreter, and was thinking of adding some restricted type inference and checking on top of it. Timing.
  - freyrs3 12y ago
    The academic type theory mentioned in this post is not really terribly important to implementing type systems for general purpose languages. There's this growing divide between the engineering discipline of type systems in general languages and the pure theory people who seem only interested in theorem provers and constructive math.
    - psygnisfive 12y ago
      This is really not true at all. Unless what you mean by "implementing type systems for general purpose languages" is a sort of weak, generally useless type system that punishes rather than helps. This is ESPECIALLY false of Pfenning and co's work, which is aimed specifically at understanding how to apply type theoretic techniques to the design of PLs, so that you get a PL with exactly the sort of stuff you want. I added a link to the page to PFPL, which is an entire book on how to implement programming languages using type theoretic tools. It even has sections on OO programming, if you're into that sort of thing. It's all the same toolkit, in the end.
    - mkehrt 12y ago
      So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift? It's all pretty much exactly the same as done in academic type theory for decades.
      - tree_of_item 12y ago
        It really isn't. Take a good long look at Java generics and ask yourself if they really came straight out of type theory research. They didn't, that's why they're so botched, and why Odersky wanted a do-over with Scala :] More seriously, Scala and Rust are the only things in your list that would actually claim to be influenced by academia. I'm sure Apple is not going for the type theorists with Swift, despite having some mildly interesting type structures like sum types, and C++'s "lambdas" obviously have very little to do with type theory, unless you want to make the very weak claim of "anything that has anything to do with the lambda calculus = type theory".
- j2kun 12y ago
  To be clear, most theoretical computer science research is not type theory. Not even close to it either.
  - seanmcdirmid 12y ago
    Even most PL research is not type theory; it is its own field.
- oldmanjay 12y ago
  No, don't ask yourself why. Just learn. It's one human activity that never requires a reason
  - kashif 12y ago
    no, don't do this. you have limited time focus what you learn just like everything else
  - bonobo 12y ago
    Time is a limited resource. As much as I'd love to learn everything that I find interesting, I can't find the time to learn all these subjects. The criteria I use to decide when to learn something or not are not like geoka9's, but I still have to ask myself why.
  - geoka9 12y ago
    What I meant is it would be impractical to pick one special topic of CS to study just because it happens to be a mode of the day. It's like deciding to study number theory ("because, you know, cryptography!") in isolation instead of following a sensible math curriculum ("I'm not particularly interested in math") and learning the discipline as it was meant to be learned. In short, I can't think of a "type system specialist" who is not a computer scientist. It sounds sort of like a "loop specialist" who can't program, or a "forehand specialist" who can't play tennis.
    - ufo 12y ago
      Type theory specialists outside of CS usually fit under the banner of "Logician". Thats why they go under your radar :)
  - billsossoon 12y ago
    Why does it hurt to ask why? Asking yourself why is also a means of learning. There are so many interesting things to learn, and they're all readily accessible to us. I find myself discovering a new fascinating subject I'd love to learn about each day, and by now the list of fascinating things has grown unmanageable. Asking "why?" can be a good means to to make sense of such a list. At a younger age, I was able to sustain great focus and effort on learning something without ever asking myself why. This approach helped me earn a doctoral degree on an obscure, esoteric topic without ever stopping to ask why. I assure you, I personally wish I'd asked why. Years later, I continue to enjoy learning. But since there are so many things to learn, I have the choice of learning many things superficially (the default when something new catches my interest daily), or really digging in and learning something in depth. At this stage in my life, with many things competing for my time and attention, learning something in depth requires considerably more motivation. And (for me) having an answer to "why?" helps me sustain that motivation.
- psygnisfive 12y ago
  So I think you're right that you should have a good reason. Fashion isn't enough. Don't learn TT cause its "cool", that would be stupid. For FP, tho.. I would say that you'll be a better functional programmer by knowing TT, even if you don't have a typed language. And if you do have a typed language, you'll want to understand your type system, so learning TT gives you the tools to do that properly. But there's more than just that. Types offer a lot to the programmer from a practical perspective. Forget the whole thing about using types to prove your code works. You can do that, you can do certified programming if you want. Learn Coq, it's great for that. But types offer you something else: *** types help you figure out what the right program is *** This is something that is often ignored or overlooked, but it's very important. Conor McBride (who's work you might want to look into once you know some TT) talks about this a lot. A relatively trivial, but easy-to-understand example of this would be the simple programming problem of writing a program that can take a pair of type `A * B` (where `` is the pair product) and return a pair of type `B A`. That is, the flips its argument's elements around. Ok this is simple and we all know what the program is, right, but let's do a little programming in Agda to see how types help you here. We'll start with a type declaration for the function, and the LHS of an equation that defines the function: swap :: A * B -> B * A swap p = {! !}0 Notice I put in this funny thing `{! !}0`. This is called a "hole": it's a part of the program that's missing. The 0 indicates its identity (this is hole 0). If we put the cursor in the hole, we can ask Agda to tell us about the hole, and it'll reply: Goal: B * A Context: p : A * B The goal is the type of the value we have to supply for the hole, the context is all the variables in scope, together with their types. Now, still with the cursor in the hole, we can ask Agda to pattern match on `p` and split the equation into as many patterns as it can. Because we have types, Agda knows all of the constructors that a type has, so it can automatically fill in the patterns for us. Since pairs have only one constructor, we simply get a slightly more complicated equation: swap :: A * B -> B * A swap (x , y) = {! !}0 Now let's again ask Agda about the hole: Goal: B * A Context: x : A y : B Notice: `p` is gone, because we matched on it, and instead we have `x` and `y`, new variables binding the elements of the pair, and their types. Now let's ask Agda to try filling in the hole a little bit. We can tell Agda to refine the hole, and because it knows the goal is a pair type, and pairs have exactly one constructor, it can chose that constructor to fill in part of the program for us: swap :: A * B -> B * A swap (x , y) = ({! !}1 , {! !}2) Now we have two new holes, with goal types B and A respectively, and the same contexts as before. We can again ask Agda to work on these holes, and it will fill in: swap :: A * B -> B * A swap (x , y) = (y , x) And we're done, we have a definition. And notice: the only code we wrote was to specify the type of `swap`, and put in an initial equation. The rest of the program came from Agda looking at the types, and then doing stuff based on that. This is a simple example, but it's exemplary of the "conversational" back and forth between the programmer and the type checker that you can get in a strongly typed program, where the types can actually help you FIND the right program. Just as another more obnoxious example, here's the the type for an induction principle for lists (also called dependently typed "fold", or dependently typed "reduce", or whatever): listInduction : (A : Set) (P : List A -> Set) -> P [] -> (forall (x : A) (xs : List A) -> P xs -> P (x :: xs)) -> forall (xs : List A) -> P xs listInduction A P n c xs = {! !}0 You can do the same thing as before, button mashing until you have no more holes, with this, and you get the right answer. In fact, there are exactly two right answers, and you can get both depending on a choice of which mashing you do. At no point do you actually have to figure out yourself that the following program is a solution: listInduction A P n c [] = n listInduction A P n c (x :: xs) = c x xs (listInduction A P n c xs) because the type FORCES that to be one of only two solutions. This kind of ability to button-mash and get a correct solution has actually lead people to compare dependently typed programming to playing a video game. The moral is: with strong types, the types HELP you, rather than smack you on the knuckles when you've messed up. So there really is something beyond just fashion and whim. It's actually practical!
molikto 12y ago
what about categorial semantics? hahaha!!!
- derriz 12y ago
  Walk away now. Type Theory derailed my PhD studies. Seduced by constructivism, Curry-Howard, Martin-Löf and especially Girard's Proofs and Types, I wasted two years and subsequently abandoned my postgraduate studies. It's comp. sci. flavoured esoteric nonsense.
  - molikto 12y ago
    is there anything in the world that is non-nonsense? so it is better to study pure-nonsense, just because it is pure
    - TheGrassyKnoll 12y ago
      I think they call it: 'death'
Pyret 12y ago
What's Type Theory and how's it different from Set Theory and Category Theory?
- chas 12y ago
  Type theory is a framework for doing logic that predates computers as we know them. If you have used first-order predicate logic before (e.g. ∀x∀y(P(f(x))→¬(P(x)→ Q(f(y),x,z)))), it performs a similar role to type theory and is the same sort of mathematical thing, it just has different properties. Logical frameworks are interesting to programmers and computer scientists because logical systems and programming languages/computation are related through the Curry-Howard correspondence. http://math.stackexchange.com/questions/166430/curry-howard-correspondence http://math.stackexchange.com/questions/166430/curry-howard-... This[1] isn't a perfect description of type theory in general because it is aimed at a particular branch of type theory called homotopy type theory, but I feel like it does a pretty good job of explaining the differences between type theory and set theory and what motivated those differences. [1]http://planetmath.org/11typetheoryversussettheory http://planetmath.org/11typetheoryversussettheory Category theory is a particularly abstract part of abstract algebra primarily concerned with extremely general mathematical structures. It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product. Category theory is often brought up when discussing type theory because there is a close relationship between these sorts of abstract structures like the one linking structs and conjunction and the structures that are described by type theory. In general, there is a close relationship between type theories and certain types of categories so you can learn interesting things about type theory from studying category theory and vice versa, but category theory contains many things which are not primarily useful for or associated with type theory.
  - JadeNB 12y ago
    > It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product. This sounds more like universal algebra (http://www.encyclopediaofmath.org/index.php/Universal_algebra http://www.encyclopediaofmath.org/index.php/Universal_algebr...) than category theory, which, almost by definition, is interested in studying structure-preserving morphisms, without too much attention to exactly what structure is being preserved.
deleted 12y ago
[deleted]
devty 12y ago
Nice!
raspasov 12y ago
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.
  - 12y ago

169 points by psygnisfive 12y ago

dons 12y ago

Good list, I'd also recommend http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf for something designed for newcomers to the field

jonsterling 12y ago
Yeah, that's a great book for learning how the methodology of type theory and judgemental presentations can be used in presenting practical/everyday PL concepts. Incidentally, I spoke with bob and he mentioned he wants to write another book some day that does the same thing, but for "pure" type theory. I think that'd be a great book, particularly given bob's unique perspective on type theory (having spent a lot of time on both sides of the fence—proof theory vs realizability). but don't count on it anytime soon!
- psygnisfive 12y ago
  I'll start added recommendations to the link, so keep 'em coming.
Alex25 12y ago
Thanks a lot! Useful!

geoka9 12y ago

Ask yourself why. You want to do CS, prove theorems, do theoretical research? Then, by all means, go for it! It's hip and you use a functional language to write software? Well... It's probably just a whim. But sure, give it a try.

k__ 12y ago
Well, of you want do implement a type system it could help too.
- agumonkey 12y ago
  I just finished writing a tiny sexp based lambda interpreter, and was thinking of adding some restricted type inference and checking on top of it. Timing.
- freyrs3 12y ago
  The academic type theory mentioned in this post is not really terribly important to implementing type systems for general purpose languages. There's this growing divide between the engineering discipline of type systems in general languages and the pure theory people who seem only interested in theorem provers and constructive math.
  - psygnisfive 12y ago
    This is really not true at all. Unless what you mean by "implementing type systems for general purpose languages" is a sort of weak, generally useless type system that punishes rather than helps. This is ESPECIALLY false of Pfenning and co's work, which is aimed specifically at understanding how to apply type theoretic techniques to the design of PLs, so that you get a PL with exactly the sort of stuff you want. I added a link to the page to PFPL, which is an entire book on how to implement programming languages using type theoretic tools. It even has sections on OO programming, if you're into that sort of thing. It's all the same toolkit, in the end.
  - mkehrt 12y ago
    So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift? It's all pretty much exactly the same as done in academic type theory for decades.
    - tree_of_item 12y ago
      It really isn't. Take a good long look at Java generics and ask yourself if they really came straight out of type theory research. They didn't, that's why they're so botched, and why Odersky wanted a do-over with Scala :] More seriously, Scala and Rust are the only things in your list that would actually claim to be influenced by academia. I'm sure Apple is not going for the type theorists with Swift, despite having some mildly interesting type structures like sum types, and C++'s "lambdas" obviously have very little to do with type theory, unless you want to make the very weak claim of "anything that has anything to do with the lambda calculus = type theory".
j2kun 12y ago
To be clear, most theoretical computer science research is not type theory. Not even close to it either.
- seanmcdirmid 12y ago
  Even most PL research is not type theory; it is its own field.
oldmanjay 12y ago
No, don't ask yourself why. Just learn. It's one human activity that never requires a reason
- kashif 12y ago
  no, don't do this. you have limited time focus what you learn just like everything else
- bonobo 12y ago
  Time is a limited resource. As much as I'd love to learn everything that I find interesting, I can't find the time to learn all these subjects. The criteria I use to decide when to learn something or not are not like geoka9's, but I still have to ask myself why.
- geoka9 12y ago
  What I meant is it would be impractical to pick one special topic of CS to study just because it happens to be a mode of the day. It's like deciding to study number theory ("because, you know, cryptography!") in isolation instead of following a sensible math curriculum ("I'm not particularly interested in math") and learning the discipline as it was meant to be learned. In short, I can't think of a "type system specialist" who is not a computer scientist. It sounds sort of like a "loop specialist" who can't program, or a "forehand specialist" who can't play tennis.
  - ufo 12y ago
    Type theory specialists outside of CS usually fit under the banner of "Logician". Thats why they go under your radar :)
- billsossoon 12y ago
  Why does it hurt to ask why? Asking yourself why is also a means of learning. There are so many interesting things to learn, and they're all readily accessible to us. I find myself discovering a new fascinating subject I'd love to learn about each day, and by now the list of fascinating things has grown unmanageable. Asking "why?" can be a good means to to make sense of such a list. At a younger age, I was able to sustain great focus and effort on learning something without ever asking myself why. This approach helped me earn a doctoral degree on an obscure, esoteric topic without ever stopping to ask why. I assure you, I personally wish I'd asked why. Years later, I continue to enjoy learning. But since there are so many things to learn, I have the choice of learning many things superficially (the default when something new catches my interest daily), or really digging in and learning something in depth. At this stage in my life, with many things competing for my time and attention, learning something in depth requires considerably more motivation. And (for me) having an answer to "why?" helps me sustain that motivation.
psygnisfive 12y ago
So I think you're right that you should have a good reason. Fashion isn't enough. Don't learn TT cause its "cool", that would be stupid. For FP, tho.. I would say that you'll be a better functional programmer by knowing TT, even if you don't have a typed language. And if you do have a typed language, you'll want to understand your type system, so learning TT gives you the tools to do that properly. But there's more than just that. Types offer a lot to the programmer from a practical perspective. Forget the whole thing about using types to prove your code works. You can do that, you can do certified programming if you want. Learn Coq, it's great for that. But types offer you something else: *** types help you figure out what the right program is *** This is something that is often ignored or overlooked, but it's very important. Conor McBride (who's work you might want to look into once you know some TT) talks about this a lot. A relatively trivial, but easy-to-understand example of this would be the simple programming problem of writing a program that can take a pair of type `A * B` (where `` is the pair product) and return a pair of type `B A`. That is, the flips its argument's elements around. Ok this is simple and we all know what the program is, right, but let's do a little programming in Agda to see how types help you here. We'll start with a type declaration for the function, and the LHS of an equation that defines the function: swap :: A * B -> B * A swap p = {! !}0 Notice I put in this funny thing `{! !}0`. This is called a "hole": it's a part of the program that's missing. The 0 indicates its identity (this is hole 0). If we put the cursor in the hole, we can ask Agda to tell us about the hole, and it'll reply: Goal: B * A Context: p : A * B The goal is the type of the value we have to supply for the hole, the context is all the variables in scope, together with their types. Now, still with the cursor in the hole, we can ask Agda to pattern match on `p` and split the equation into as many patterns as it can. Because we have types, Agda knows all of the constructors that a type has, so it can automatically fill in the patterns for us. Since pairs have only one constructor, we simply get a slightly more complicated equation: swap :: A * B -> B * A swap (x , y) = {! !}0 Now let's again ask Agda about the hole: Goal: B * A Context: x : A y : B Notice: `p` is gone, because we matched on it, and instead we have `x` and `y`, new variables binding the elements of the pair, and their types. Now let's ask Agda to try filling in the hole a little bit. We can tell Agda to refine the hole, and because it knows the goal is a pair type, and pairs have exactly one constructor, it can chose that constructor to fill in part of the program for us: swap :: A * B -> B * A swap (x , y) = ({! !}1 , {! !}2) Now we have two new holes, with goal types B and A respectively, and the same contexts as before. We can again ask Agda to work on these holes, and it will fill in: swap :: A * B -> B * A swap (x , y) = (y , x) And we're done, we have a definition. And notice: the only code we wrote was to specify the type of `swap`, and put in an initial equation. The rest of the program came from Agda looking at the types, and then doing stuff based on that. This is a simple example, but it's exemplary of the "conversational" back and forth between the programmer and the type checker that you can get in a strongly typed program, where the types can actually help you FIND the right program. Just as another more obnoxious example, here's the the type for an induction principle for lists (also called dependently typed "fold", or dependently typed "reduce", or whatever): listInduction : (A : Set) (P : List A -> Set) -> P [] -> (forall (x : A) (xs : List A) -> P xs -> P (x :: xs)) -> forall (xs : List A) -> P xs listInduction A P n c xs = {! !}0 You can do the same thing as before, button mashing until you have no more holes, with this, and you get the right answer. In fact, there are exactly two right answers, and you can get both depending on a choice of which mashing you do. At no point do you actually have to figure out yourself that the following program is a solution: listInduction A P n c [] = n listInduction A P n c (x :: xs) = c x xs (listInduction A P n c xs) because the type FORCES that to be one of only two solutions. This kind of ability to button-mash and get a correct solution has actually lead people to compare dependently typed programming to playing a video game. The moral is: with strong types, the types HELP you, rather than smack you on the knuckles when you've messed up. So there really is something beyond just fashion and whim. It's actually practical!

molikto 12y ago

what about categorial semantics? hahaha!!!

derriz 12y ago
Walk away now. Type Theory derailed my PhD studies. Seduced by constructivism, Curry-Howard, Martin-Löf and especially Girard's Proofs and Types, I wasted two years and subsequently abandoned my postgraduate studies. It's comp. sci. flavoured esoteric nonsense.
- molikto 12y ago
  is there anything in the world that is non-nonsense? so it is better to study pure-nonsense, just because it is pure
  - TheGrassyKnoll 12y ago
    I think they call it: 'death'

Pyret 12y ago

What's Type Theory and how's it different from Set Theory and Category Theory?

chas 12y ago
Type theory is a framework for doing logic that predates computers as we know them. If you have used first-order predicate logic before (e.g. ∀x∀y(P(f(x))→¬(P(x)→ Q(f(y),x,z)))), it performs a similar role to type theory and is the same sort of mathematical thing, it just has different properties. Logical frameworks are interesting to programmers and computer scientists because logical systems and programming languages/computation are related through the Curry-Howard correspondence. http://math.stackexchange.com/questions/166430/curry-howard-correspondence http://math.stackexchange.com/questions/166430/curry-howard-... This[1] isn't a perfect description of type theory in general because it is aimed at a particular branch of type theory called homotopy type theory, but I feel like it does a pretty good job of explaining the differences between type theory and set theory and what motivated those differences. [1]http://planetmath.org/11typetheoryversussettheory http://planetmath.org/11typetheoryversussettheory Category theory is a particularly abstract part of abstract algebra primarily concerned with extremely general mathematical structures. It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product. Category theory is often brought up when discussing type theory because there is a close relationship between these sorts of abstract structures like the one linking structs and conjunction and the structures that are described by type theory. In general, there is a close relationship between type theories and certain types of categories so you can learn interesting things about type theory from studying category theory and vice versa, but category theory contains many things which are not primarily useful for or associated with type theory.
- JadeNB 12y ago
  > It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product. This sounds more like universal algebra (http://www.encyclopediaofmath.org/index.php/Universal_algebra http://www.encyclopediaofmath.org/index.php/Universal_algebr...) than category theory, which, almost by definition, is interested in studying structure-preserving morphisms, without too much attention to exactly what structure is being preserved.

deleted 12y ago

[deleted]

devty 12y ago

Nice!

raspasov 12y ago

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.
- 12y ago