Comment by tomp | Hacker News Reader

Comment by tomp | Hacker News Reader

Judging by the first paragraph, the author has a very biased, even aggressive preference for static languages and a contempt for anyone that disagrees with him. I don't like that, and I find that the best and most convincing arguments are those that show understanding of the opposite side. People using aggression or logical fallacies in their arguments are usually the people who can't use logic to convince others.

" ... types (static types, of course, there being no other kind) ... "

This is the statement I'm referring to above. It strikes me as completely misguided and wrong. Most languages that I know of, even most statically typed languages, know dynamic types. Java has instanceof. C++ has virtual dispatch (which is based on an objects dynamic type). Even C (untagged) unions usually have some (bit)field that allows the running program distinguish the type of data in the union.

I believe that in general, types are properties of data, which rarely exists at compile time. Thus, almost all types are dynamic. Statically typed languages simply restrict the data that can be stored in variables to a particular type and subtypes thereof.

There are no dynamic types, but there may be dynamic typing. All those so called dynamic typed languages are actually statically uni-typed and figure out at run time the so called dynamic type. Types are not properties of data, types are proofs about your program. In general type safety provides proofs of preservation of types and that your program won't get stuck due to types. The perception you have about types is exactly the problem that Prof Harper is trying to avoid in his students.

Then maybe all this conflict really is "a problem of grammar", as Harper himself asserts. For me, the word type has a differenn meaning than for you. Maybe we should instead be using the expressions static type (compile-time proof) and dynamic type (runtime properties of data, which Harper calls class, though I prefer not to use this word as its meaning is already too overloaded in CS).

What you're calling a dynamic type is what he'd call a canonical form. If your typing system has product types, then you should be able to prove that anything with a product type evaluates down to an ordered pair.

Harper has somewhat... unorthodox views on the subject (and has had them for a long time). Here's the HN discussion of the essay he links to in that parenthetical: http://news.ycombinator.com/item?id=2346590. Quite a few also-prominent PLs researchers comment negatively in the comments on his post as well.

In general I find Harper's "positive" opinions on the design of ML better than his "negative" opinions on why everything that isn't ML is doing it wrongwrongwrong, but he's definitely quite intelligent and usually has some good points.

The author is not talking with the snide condescension of an Internet troll who, after reading the first chapter of a book, feels he's been clued into a grand truth. He's talking with the snide condescension of one of the world's top researchers in the field. Or, rather, he's not putting effort into communicating to people who don't have some background in PL theory and some familiarity with many of these arguments.

Professor Harper typically spends two lectures in his undergraduate PL class developing the idea of dynamic typing, and then demolishing it. If you turn to the section on 'Static "Versus" Dynamic Typing' in his book (http://www.cs.cmu.edu/~rwh/plbook/book.pdf -- currently section 22.3, but subject to change), you'll find a summary of his argument. Basically, what dynamically-typed languages do is not really "type-checking" but "run-time tag checking."

You brought up a really good point though -- C and Java aren't really statically-typed languages. Getting a null-pointer error is just not possible in a type-safe language.

He may be one of the world's top researchers in the field, but on this point his view is not the consensus view of PLs researchers; other top researchers in the field think that Harper is wrong on the subject. On the other hand it's mostly a semantic dispute over who owns the word "type", which has historically come from multiple sources in mathematics and engineering. The C view of types is closer to the comp-arch view of "typed registers", which isn't really a proof so much as a statement about data-representation capabilities ("this register can hold floats").

It's unsurprising Harper doesn't like that view, because he objects to the entire line of machine-oriented CS thinking, on both the engineering and the theory sides. For example, he thinks computational complexity theory should ditch Turing machines and be refounded on the basis of functional programming.

Hmm, yes "type" can mean a lot of things, but would many dispute that the languages with the most evolved type systems are those discussed in the post(ML, ocaml, haskell, F#) plus scala? (Leaving aside coq, agda which I'm not familiar with

http://blog.tmorris.net/a-brief-point-on-static-typing/

http://james-iry.blogspot.com/2010/05/types-la-chart.html

That chapter doesn't seem to be provide any arguments for redefining what the words "dynamic typing" mean other blind assertions of the same sort that he used in his blog posts. I appreciate that he has a potentially useful mathematical formalism, but thats no reason to go about redefining words in relatively common usage - and especially not to be rude about it.

Reply on news.ycombinator.com