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