Hacker News Reader

Comment by freyrs3 | Hacker News Reader

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.

View on HN

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.

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.

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".

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

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.

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.

Reply on news.ycombinator.com