This search term appeared in my referer logs a few years ago: “lambda the ultimate makes me feel stupid”.
I used to feel that way — at least, I felt ignorant and despised. The denizens of LtU know an intimidating amount of theory, and some are quick to scorn anyone who doesn't, and demand that they read heaps of literature (often of dubious quality or relevance) before being permitted to talk. Not having read most of that literature, I accepted their evaluation, and felt ignorant.
But then battles of the War of Types erupted there, and λ the Ultimate became λT the Ultimate, or even System F the Ultimate. Anyone who dared suggest that dynamic typing was a reasonable basis for a language, or even a meaningful concept, faced voluminous condescension and condemnation. The seemingly knowledgeable scholars appeared to neither know nor care about the fundamental concepts of their field, and treated its greatest successes with learnèd disdain.
I do respect very much the elephant, and if your work dismisses him as an ill-formed dinosaur, it is not zoology.
(I don't think the dynamic typists gave a good account of themselves either; there was lots of handwaving about flexibility and little mention of the importance of simple semantics. But I found them less offensive, not only because I agree with them, but because they didn't demand the anathematization of the other side, nor of the object of study.)
The War of Types subsided, and LtU became once more a place of academic quiet, disturbed only by announcements of new PL papers. It still makes me feel ignorant at times, but it no longer makes me feel stupid. Sometimes it even makes me feel wise. Which is a much more dangerous emotion. When I feel stupid or ignorant, I study to become less so, but when I feel wise, I do nothing.
As a newcomer I can't decode which fundemental concepts and greatest successes you're talking about. Could you point me to where I can read about this specific success?
ReplyDeleteThe “fundamental concept” I'm talking about is datatypes. There is a strain of the static-type movement that insists “type” can only ever mean “classifying expressions” (which is what it means in type theory), and cannot mean “datatype” (which is what it means in programming languages). Rather than use a different word (like “datatype”?), they simply refuse to talk about types, especially if they're tracked dynamically.
DeleteThe “greatest successes” are the most expressive languages, which tend to be dynamically typed.
Thanks ffor sharing
ReplyDelete