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

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!