Summer of Programming Languages

> tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered.

He begins by first rigorously defining what he means by "type". In particular, it's a piece of information computed statically (i.e. using the syntax of a program alone, nothing of its "runtime") which constrains the eventual values the dynamics must take. A "type-safe" program is thus one where the dynamics correspond to the predictions of the statics—in particular, a program respects its type as it operates and the program "does not get stuck" i.e. does not hit an undefined state.

From here he notes the power of union types, types which are "either" A or B. Given a sufficiently large union type, one which reads "either this or that or this or that" for every possible result value of running a program then you can create a "safe" semantics for any language using this type—every program has this giant union type and every choice of dynamics ends up in this giant union type. He then notes that while this genuinely is "type safe" it's kind of boring. Further, all "dynamically typed" languages inherit this boringness since they expose no "interesting" static structure.

(Even if you dislike the argument above, and there's plenty that might cause someone to dislike it, it's worth noting that this line of thought arrives very smoothly at the concept of "hybrid typing" being explored by things like Typescript and Facebook's Hack.)

One of the primary things you could argue with at this point is that having more sophisticated types is interesting and valuable. To this end Harper focuses on what he calls the "Holy Trinity" of logic, type theory, and category theory. The idea is backed by the Curry-Howard-Lambek correspondence which shows that each of these fields is but an image of the other two. In Harper's (paraphrased) words: you know that something is genuine and lasting if you can show it exists in every branch of the Holy Trinity.

So he declares basically by fiat that things which reflect the Holy Trinity are interesting and things which do not are not. Obviously you can levy many arguments to disagree with him here.

But it's hard to declare that the things discovered in the Holy Trinity are boring. This is where cutting edge research on things like Homotopy Type Theory and general Dependent Types live. This produces compelling arguments to back up why "null pointers are a billion dollar mistake" [0] or why if-branching and booleans lack meaningful providence [1]. These ideas, even if they are stripped of their Ivory Tower gleam, are what are slowly percolating into mainstream languages with names like "Enum"++ in Swift and "Optional" in Java.

---

Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". But they are sometimes at odds since they place the brunt of what they demand of a language at different places. Ultimately, if Harper's program is successful many years from now we'll all use shadows of whatever futuristic grade of dependently typed language gives us maximal expressiveness while nesting it in an ecosystem of tooling and libraries which aid construction of interesting things. I have no idea if Harper's "one true language" exists, but it does seem like increasingly the world is moving that way... thus Harper's enthusiasm about Swift and Rust.

[0] http://qconlondon.com/london-2009/presentation/Null+Referenc...

[1] http://existentialtype.wordpress.com/2011/03/15/boolean-blin...

Technical books often define terms in a way convenient for the material and approach they are presenting, not in a way that is general to the field; particularly, if terms are used in different ways within the field at the time they are written, they typically have to choose for consistency within the book -- that doesn't make that definition the right one for the field, it simply means that's what the term means in the context of the work.

And, ultimately, the semantic argument is meaningless. It doesn't really matter whether you have static and dynamic types in different languages or you call the former "types" and the latter "tags" (except that the former terminology actually explains the difference in a way that tells you what the difference is every time you use the terms.) The substance is the same, and getting worked up over line-drawing regarding the boundary of "type" is a distraction from any discussion of substance.

However, the Rust team is trying to get 1.0 out the door, and higher-kinded types would be backwards compatible, so I don't think we'll be seeing them for a while. There's also questions about the overhead and syntax that would need to be resolved for them to make it in.

I forget who said this, but programming language design is basically "applied psychology", and if you admit that, your language will go further. For example, the difference between Python and many similar languages is that it looks nicer and is "intuitive" to read, and that contributes a large part (perhaps the largest part) to its popularity.