Wednesday, August 02, 2017

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.

Sunday, May 07, 2017

On the efficacy of online flamewars

Excavated from the drafts folder for no particular reason.

Isn't it great how, since the Brendan Eich affair, all his online defenders have become active labor rights organizers, fighting for workplace political freedom for all? Galvanized by the realization that not only CEOs but all workers deserve robust protections for their political beliefs, Eich's erstwhile defenders channeled all their passion into effective political action. Which is why Congress will vote this week on a bill with three key provisions: first, it outlaws any form of workplace discrimination based on political speech or activity conducted outside the office; second, it handsomely funds an investigative division of the FBI tasked specifically with working with the NLRB to track down and prosecute violators; third, by analogy with the Foreign Corrupt Practices Act and the 2003 Protect Act (which grants American prosecutors broad latitude to charge Americans who molest children while abroad), it makes it illegal for companies operating on American soil to subcontract work to overseas employers which restrict their workers' political rights.

There was never any danger that Eich's defenders would just basically forget about the whole affair and get on with their lives. Ha ha! Yeah that definitely couldn't have happened, given how deeply committed these people were to the principle of workplace political freedom. It's not like they only care about workers' rights when it's an incredibly wealthy white male celebrity who is being criticized.

Likewise, when the dead bloated corpse of patriarchy is laid to rest this fall, everyone will have to recognize that the great Twitter Flamewar of March 2014 was really the spike through its heart. No, not that one, I mean the other one, the one where we all wrote angry all-caps tweets at that one dude, he was totally mansplaining and stuff, you remember the one I'm thinking of.