8 ms·

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 wri

• 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".
        • mkehrt 12y ago
          Re Java generics: Nope. They came out of UPenn's featherweight java work, see here: http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf 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.
        • psygnisfive 12y ago
          One of the primary major players with generics in Java is Philip Wadler, a type theorist and one of the co-creators of Haskell. Generics comes straight out of type theory research, and normally its called parametric polymorphism, but mainstream programmers can't handle that funky terminology. Apple's work on Swift has openly acknowledge its debt to Haskell and contemporary work on type theory, and it shows. As for the rest, you'd have to ask the people who worked on them. 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.
• 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!