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.
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.
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.
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.
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.
It's all pretty much exactly the same as done in academic type theory for decades.
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".
Pierce literally wrote the book on type theory.
Swift is written by type theorists; large chunks of the people who worked on it has a PhD (or part of one) in PL theory.
At any rate, C++, Scala, Rust, Java.. these are not languages that take type theory very seriously, and probably couldn't. It's certainly true that the popular imperative languages don't take TT seriously.
But so what? The comment was about general purpose languages, and type theory is demonstrably of use in implementing them. Just because most mainstream languages don't use type theory doesn't make that not true. It just means most mainstream languages do not make use of everything they could.
Oh well. Their loss.
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 ***
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
Goal: B * A
Context:
p : A * B
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
Goal: B * A
Context:
x : A
y : B
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)
swap :: A * B -> B * A
swap (x , y) = (y , x)
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
listInduction A P n c [] = n
listInduction A P n c (x :: xs) = c x xs (listInduction A P n c xs)
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!
Eg : if you're computing a speed ( m/s), then you'd better divide something that has a distance unit by something that has a time unit.