From 7e601b0ad80d60800258637bec724ca97834f850 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Tue, 3 May 2016 15:10:11 -0400 Subject: [PATCH] [rebuttal] 2nd draft --- icfp-2016/rebuttal.txt | 76 ++++++++++++++++++++++++++++-------------- 1 file changed, 51 insertions(+), 25 deletions(-) diff --git a/icfp-2016/rebuttal.txt b/icfp-2016/rebuttal.txt index 25c276a..49a0da6 100644 --- a/icfp-2016/rebuttal.txt +++ b/icfp-2016/rebuttal.txt @@ -6,10 +6,10 @@ introduction. -1. The purpose of this pearl is to describe a ==LANGUAGE AGNOSTIC== technique - for improving a typed language's ability to give compile-time feedback. +1. The purpose of this pearl is to describe a language agnostic technique + for augmenting a traditional type checker. - Typed Racket is ==IRRELEVANT== to our technique. + Typed Racket is irrelevant to our technique. If this paper is accepted, we plan to use Rust for demos in the talk. @@ -72,17 +72,18 @@ Section 6 : rekindle the fun of Sec. 1 after the long Sec. 5 - With the reviewers permission, we propose a different organization to - emphasize the useful applications: + With the reviewers' permission, we propose a different organization: - Section 1 : Same as before + Section 1 : same as before - Section 2 : Same + Section 2 : same as before Section 3 : same examples, - explicit comparisons to "vanilla Typed Racket", + explicitly compare to Typed Racket without our library, list desirable guarantees of each elaborations + Section 4 : same as before + Section 5 : basics of Racket macros in terms of `printf` Section 6 : internals of every example from Sec. 3 @@ -98,8 +99,8 @@ -------------------------------------------------------------------------------- --- RA RB, re: translating the ideas to Typed Clojure, Scala, and Rust - These languages have powerful syntax extension tools but are just missing - some of Racket's useful abstractions & guarantees. + These languages have equally powerful syntax extensions as Racket. + The tools are just less mature / less documented. * Clojure's macros are arbitrary rewrite rules interspersed with normal Clojure code run at compile-time. @@ -108,7 +109,7 @@ * Scala Macros may not be able to handle definitions, but can definitely handle type-safe printf for constant strings [2]. - Scala LMS [3] seems to be more powerful any either way Scala's + Scala LMS [3] seems to be more powerful. Either way Scala's compiler plugins [4] are at least as powerful as Racket's macros. * Rust's macros cannot implement our interpretation functions, but @@ -123,13 +124,12 @@ -------------------------------------------------------------------------------- ---- RA RB, re: (printf ~a) +--- RA RB, re: (printf "~a") Calling (printf "~a") raises an arity error in our implementation because "~a" is a valid format specifier yet `printf` is called with zero additional arguments. - Calling (printf "~b") would give the exact same error --- Racket functions - are not curried. + Calling (printf "~b") would give the same arity error. But (printf "~a") is definitely a typo. We intended to use "~s" instead. @@ -142,7 +142,22 @@ -------------------------------------------------------------------------------- --- RA, re: Dialyzer -TODO + The Dialzyer belongs in our discussion of related work --- either in the + intro or part of a dedicated section. + Its guarantee matches our third requirement for elaborations (statically + rejected programs will go wrong at runtime). + + The PEPM'13 paper you mention is interesting, but orthogonal to our + pearl. + + - We are seeking to catch more runtime errors statically and allow more + dynamically-correct programs that fail to typecheck as written. + Our strategy is to do so with local transformations. + + - Sagonas, Silva, and Tamarit are computing program slices to improve + the quality of type error messages. + + But their technique would be very useful for Typed Racket ----------------------------------------------------------------------------- @@ -156,23 +171,23 @@ TODO --- RA, re: how many casts and annotations were made redundant? We removed casts around every call to `regexp-match` we found in typed code. - But that was only 10 calls and unfortunately this is the biggest usability - success story: + But that was only 10 calls and unfortunately we found no typed programs + using SQL. - * Existing uses of printf, arithmetic, and vectors were already type-correct - - * Most casts on numeric values dealt with non-constants --- usually - variables bound as function parameters. - - * We found no typed programs using SQL. + Besides removing casts, the library is also useful for early detection of + bugs when writing programs. + Our personal experience has been good. + We did ask Typed Racket users for feedback, but unfortunately got no response + at the time (three months after the library was initially released). -------------------------------------------------------------------------------- --- RA, re: type error messages - The error messages have been very good. + The error messages have been surprisingly good. When we can immediately reject a program (due to out-of-bounds vector access, - etc) we also give a specific error message. + etc) we can give a specific error message and will show these in the + final version of the paper. When deferring errors to Typed Racket, the error message has always been triggered by a new annotation added to the original source code, so errors are typically caught earlier than normal. @@ -193,3 +208,14 @@ TODO We will say "many" languages instead of "most". + +-------------------------------------------------------------------------------- +--- RC, re: examples "don't really drive the point home" + + This is a weakenss of our presentation. + If permitted, we will reorganize to show how the examples run in Typed Racket + and compare to our library. + + (Doing so is a little tricky, as some are runtime errors, some are type + errors, and Sec. 3.6 requires an elaborate work-around. But we can manage.) +