How important is decidability in programming tools?

Hoisted from the drafts folder because the discovery that TypeScript's system is Turing-complete is making the rounds.

It's a common assumption in the programming language community that practical type systems should be decidable. Or, at least, it used to be: in the early 2000s, I had a grad school colleague who spent a lot of time trying to invent restrictions that made the type system of Cecil decidable, and people seemed to feel that his formalization of Cecil would be unreasonable if he could not solve this problem.

Over a decade later, it's well-known that Java with generics and wildcards was undecidable for years before people even realized it. Furthermore, devising restrictions to the type system that achieve decidability seems to be an open research problem.

Did hundreds of thousands of Java programmers experience an existential crisis when Java with generics was found to be undecidable? Are they waiting with bated breath for researchers to solve this urgent problem? I'm pretty sure 99.99% of them don't know that the problem exists and won't notice if it's ever fixed.

Meanwhile, the PL research community has mostly gotten bored of object-oriented languages and type systems thereof, and moved on to other things. And the functional programming community (or some fraction thereof) has embraced Scala, whose type system is also undecidable.

Conversely, it is well-known that in ML, it is possible to write a program by hand on a single sheet of paper that will take longer than the lifetime of the universe to typecheck, because Hindley-Milner is superexponential in the worst case.

What is the practical difference between a typechecker that can hang until the universe is a cold, featureless void of uniformly distributed entropy and a typechecker that can hang forever? In both cases, you would hit Ctrl-C after a decent interval and rewrite your program. Would it make much difference if ML's type system were undecidable? Probably not.

I remember standing up at an ECOOP talk one year and asking a question along those lines. The researchers had made a big deal about the importance of decidability for the problem they were solving, and I asked why it was so important. The presenters seemed to think the question was ridiculous and I'm pretty sure everyone else in the room thought so too. I probably didn't word my question well — I wasn't a good researcher and I'm not proud of my time in academia — but I still think I was basically right that one time.

The important thing is that tools have tractable runtimes for the programs that people want to write. Unfortunately, "tractable runtime for reasonable programs" is much harder to demonstrate using the formal and empirical tools that exist today than "decidable for all syntactically valid programs". And the gap in available intellectual tools has led a research community to handcuff itself needlessly in hunting for useful results.

Academics, children, gender

Two posts at Crooked Timber worth reading: on the childlessness of women vs. men academics; on the increasing duration of the professorial track in recent decades.

Off-the-cuff reaction #1: If you're a woman academic who wants to have children and get on the tenure track at a competitive research university, you should look for a man who's likely to stay home and take care of the kids. With all that entails. Unfortunately, most women's libidos are wired by culture to respond most strongly to men who are at least somewhat aggressive, ambitious, and dominating. Alas, these traits do not correlate strongly with the tendency to become a stay-at-home husband.

(Off-the-cuff reaction #1.5: Perhaps women who find their libidos wired in this tragic fashion could resolve this conundrum the way that men have traditionally resolved the converse conundrum. Let the sensitive house-husband raise the kids; cheat on him periodically with aggressive, dominating men. In case the "converse conundrum" for men is not obvious: most men are wired, by culture, to respond to perky taut-bodied young women who hang on their every word, which does not usually describe a wife after she's had a few children. The traditional male solution has been to cheat on the wife with a younger woman. I leave it to the reader to puzzle out whether I am seriously suggesting that women academics cheat on their model-father husbands, or whether I am suggesting that women academics should reconcile their libidos with their circumstances. I am not sure which of these suggestions is more offensive, but they seem like the obvious alternatives. Of course, the statistics tell us that most women academics are not having children, and hence probably not married to homemaker Dads, so this hypothetical situation isn't exactly representative of reality anyway.)

Off-the-cuff reaction #2: The inescapable conclusion of the second CT post is that, because of the asymmetry in male vs. female fertility, the current academic system is structurally biased towards men. The 22-34 window, during which you have to get your Ph.D. and then immediately work your ass off to get tenure, overlaps with most of a woman's prime childbearing years. This sounds utterly obvious but it has never before hit me with the same force.

We should move to a system in which junior faculty can take parental leave for a few years, sometime before the tenure review. Or, we should remove the stigma attached to getting your Ph.D. in your 30's instead of your 20's; and make it easier for grad students to take a few years off from the program after quals. Or all of the above. These reforms would have major benefits for men as well: not everyone fits into the classic 12-year career path anyway.

UPDATE: Inky points to a Nature article about a European Commission conference whose subject is promoting women in science.

Why we need elective calliagnosia

The Higher Education Chronicle notes that good-looking professors get better evaluations. Article ranges from hilarious...

Mr. Lang has always earned high marks from his students at Assumption College, but he doesn't consider himself a "Baldwin" (for the clueless, that's a term for a hot guy, popularized by the movie Clueless). Apparently, though, some of his students do. More than one of them has made comments about his "buns" on student evaluations.

Now the assistant professor of English says he's self-conscious about his looks and his teaching. "I work very hard at my teaching," he says, "and I am a little disturbed at the possibility that students are evaluating my courses based on such a superficial criterion." He wonders if he's as good a teacher as he thought he was, and he's afraid to turn his back to his classes to write on the chalkboard.

...to surprising...

Some male professors also may be dismayed about another finding of the study: "Good looks generated more of a premium, and bad looks more of a penalty, for male instructors," say Mr. Hamermesh and Ms. Parker in a paper about their findings, "Beauty in the Classroom: Professors' Pulchritude and Putative Pedagogical Productivity." According to their data, the effect of beauty (or lack thereof) on teaching evaluations for men was three times as great as it was for women.

I'll do what the Chronicle does not, and link to the original academic paper: summary at NBER; alternate link.

BTW the title of this post comes from a term used in Ted Chiang's marvelous story "Liking What You See: A Documentary", which appears in his collection Stories of Life, and Others (available in hardcover and paperback).

Wage discrimination and gender

Alas, a blog's recent series on wage discrimination and gender is quite informative; I hope someday the Alas folk will package this series up as a PDF, like David Neiwert's Rush series. The point that hits closest to home for me, as an apprentice scientist:

What the Nature study did was examine productivity (measured in terms of publications in scientific journals, how many times a person was a "lead author" of an article, and how often the articles were cited in scientific journals) and sex. Publication in peer-reviewed scientific journals is often considered to be the most objective and "concrete" sign of accomplishment in the sciences. These factors were then compared to how an actual scientific review panel measured scientific competence when deciding which applicants would receive research grants. Receiving grants like these are essential to the careers of scientific researchers.

The results? Female scientists needed to be at least twice as accomplished as their male counterparts to be given equal credit. For example, women with over 60 "impact points" - the measure the researchers constructed of scientific productivity - received an average score of 2.25 "competence points" from the peer reviewers. In contrast, men with less than 20 impact points also received 2.25 competence points. In fact, only the most accomplished women were ever considered to be more accomplished than men - and even then, they were only seen as more accomplished than the men with the very fewest accomplishments.

It probably wouldn't surprise the average layperson to learn that computer science is an overwhelmingly male profession. A 9-to-1 male to female ratio is a typical ballpark figure at all levels, from undergrad major enrollment through junior faculty, though it gets worse as you go up the ladder. Furthermore, my own specialization (programming languages and tools) is even more overwhelmingly male. When I go to the top conferences*, there will typically be a mere handful of women in a room of two hundred researchers.

I don't think these population numbers reflect disciplinary sexism. In fact, I think my profession's less sexist, on average, than society as a whole; and certainly the individual women researchers with whom I'm familiar are quite well-regarded. But the sobering studies cited by Alas do reflect disciplinary sexism (in science in general), and should lead us all to question the way we approach women and their work. Sexism in this context won't generally be a conscious act --- it could be a mere statistical differential in the probability that we'll cite particular papers, or chat with particular individuals at conferences, or chat about particular people's work with other people (the latter two are quite important for generating "buzz" around people's work).

This leads to an interesting question: should scientists practice a form of "personal affirmative action" for women researchers, whereby we consciously make an effort to pay extra attention to women and their research?

* Note for any curious scientists in other fields who may be reading this: conferences are a much bigger deal in computer science than in most other sciences. The year-or-more lag time for reviewing journal papers means that cutting-edge research is basically never published in journals. If you want to keep up, you must attend conferences, and publish your best research in them. As a result, the bar for conference publications is also much higher than in other fields: the top conferences in programming languages are well-known for rejecting even quite strong submissions because the competition's so intense.

Once you get a paper at a good conference, you may fill out the paper with all the details and tedious proofs, and attempt to publish the extended version in a journal; but this step's not strictly necessary to build a reputation. A fresh Ph.D. could get a faculty job at a top-ten institution without a single journal paper.