> On Dec 4, 2015, at 5:06 PM, Matthew Butterick <m...@mbtype.com> wrote: > > Under Betteridge's Law, I was expecting that a paper so titled [1] would > conclude that the answer is no. But it does ultimately assert that "In the > context of current implementation technology, sound gradual typing is dead." > (With a silver lining that some new research questions have been discovered.) > > What is the upshot for those of us whose Racketeering is more in the > practical rather than research realm? On its face, this paper seems to tell > me "don't use TR." Is that accurate? Is there a category of practical > programs that TR remains suitable for? > > I ask this as one of the guinea pigs studied in the paper [2]. I originally > picked up TR because I was curious whether it would be suitable for a project > where performance is a key consideration. Instead, TR slowed it down. Though > I was relieved to learn that my bad programming was not entirely the culprit, > now I feel bad about helping kill TR.
Matthew, thanks for bringing up this title/result. As the author of this title (and the somewhat sharper edges in the prose), I owe the mailing list a general response. The title/paper are set up in this way to get the research community engaged. Typed Racket is the first and longest research development project in the gradual typing context (though the paper that Sam and I published did not use this phrase originally, which was coined in a parallel paper within a month of our design pub). For most of the time since 2006, a fair number of efforts in this direction have focused on plain theory or moved toward optional unsound typing (you may say Int -> Int but I mean Int -> Real, too bad for you). In particular nobody had any idea of how to measure whether a GT language would support the imagined gradual conversion of untyped programs into mostly typed ones. It is my opinion that semi-practical research questions such as this one call for a systematic evaluation, and I wanted to use the title/paper game to wake up the selection committee at POPL (our flagship conference in the research area). Well it did and the paper will appear there. — MAIN RESULT: The main result is really a method for measuring the “gradualness” of a GT language. We measure every possible way of tackling the conversion of an UNtyped program into a TYPED one for multi-module programs. The expectation is that (1) the top and the bottom should have approximately the same performance and (2) ideally the points (of partially converted programs) in between should perform well enough to be deliverable or at least useful. — COLLATERAL RESULT: As is, the evaluation method reveals that TR satisfies (1) but not (2). So if you use TR as intended — gradually convert a multi-module program into a partially typed one — you are extremely likely to experience serious performance problems. To the Racket/Typed Racket community, this collateral result is not a disaster. Instead it sets a research agenda, namely, to get TR to satisfy (2) linguistically (that is, as a language) or via IDE support that helps programmers identify and eliminate particularly bad trouble points in partially typed programs. Like everything in our language world, TR is a serious research effort meaning we are committed to invest a lot of energy and time into its realization. We will report progress as we make it and you’re likely to experience it before we say much about it, — Matthias -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
