diff --git a/icfp-2016/rebuttal.txt b/icfp-2016/rebuttal.txt index d24f983..b06880f 100644 --- a/icfp-2016/rebuttal.txt +++ b/icfp-2016/rebuttal.txt @@ -36,8 +36,8 @@ Thanks! in section 2. Specific guarantees like "the new division function raises - compile-time errors when called with a 0 denominators" are theorems - that may be stated and proven correct in the same was as Haskell's or + compile-time errors when called with 0 denominators" are theorems + that may be stated and proven correct in the same way as Haskell's or ML's type system is proven correct. The examples are chosen precisely because they suggest theorems that a @@ -49,121 +49,68 @@ Thanks! === END OF FORMAL RESPONSE. Detailed comments to reviewers (RA RB RC) follow. ================================================================================ --------------------------------------------------------------------------------- ---- RA RB RC, re: purpose & organization of pearl - - The pearl is currently organized as: - - Section 1 : examples, design goals, outline of pearl - - Section 2 : formalize intuition from Sec. 1, - get readers thinking: "how could I do this in my language?" - - Section 3 : motivating + useful + versatile examples - - Section 4 : justify "annotation free" claim from Sec. 1 - - Section 5 : basics of Racket macros, - full details of two examples from Sec. 3, - how to handle definitions, - checklist of useful Racket features - - Section 6 : rekindle the fun of Sec. 1 after the long Sec. 5 - - - With the reviewers' permission, we propose a different organization: - - Section 1 : same as before - - Section 2 : same as before - - Section 3 : same examples, - 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 - emphasis on Sec. 3.6 - - Section 7 : checklist of useful Racket features - - Section 8 : related work + implementation sketch for other languages - - Section 9 : conclusion - - -------------------------------------------------------------------------------- --- RA RB, re: translating the ideas to Typed Clojure, Scala, and Rust These languages have equally powerful syntax extensions as Racket. - The tools are just less mature / less documented. + The tools are just less mature and less documented. * Clojure's macros are arbitrary rewrite rules interspersed with - normal Clojure code run at compile-time. - The main difficulty will be parsing complicated syntax patterns and - being robust against renamings. + normal Clojure code run at compile-time. - * 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. Either way Scala's - compiler plugins [4] are at least as powerful as Racket's macros. + * Scala's Lightweight Modular Staging (LMS) [1] framework can implement + rewrite rules and compile-time partial evaluation. We believe it + can also simulate identifier macros; if not, Scala's compiler plugin API [2] + definitely can. * Rust's macros cannot implement our interpretation functions, but - their compiler plugins [5] are on-par with Scala's. + their compiler plugins [3] are on-par with Scala's. Sources: - [1] https://github.com/clojure/tools.macro - [2] http://docs.scala-lang.org/overviews/macros/overview.html - [3] https://scala-lms.github.io/ - [4] http://www.scala-lang.org/old/node/8656 - [5] https://doc.rust-lang.org/book/compiler-plugins.html + [1] https://scala-lms.github.io/ + [2] http://www.scala-lang.org/old/node/8656 + [3] https://doc.rust-lang.org/book/compiler-plugins.html -------------------------------------------------------------------------------- --- 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. + "~a" is a valid format specifier yet `printf` is called with zero additional + arguments. Calling (printf "~b") would give the same arity error. + These both compile in Typed Racket but fail at runtime. - But (printf "~a") is definitely a typo. + But writing (printf "~a") was a typo on our part. We intended to use "~s" instead. - (Both specifiers accept any value but format the result slightly differently) The final version of the paper will give actual error messages instead of - using ⊥. + using ⊥. -------------------------------------------------------------------------------- --- RA, re: Dialyzer - 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 Dialyzer belongs in our discussion of related work. + 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. + The PEPM'13 paper 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. + dynamically-correct programs that fail to typecheck as written. - Sagonas, Silva, and Tamarit are computing program slices to improve - the quality of type error messages. + the quality of type error messages. - But their technique would be very useful for Typed Racket + But their technique would be very useful for Typed Racket. ----------------------------------------------------------------------------- --- RA, re: using #false in interpretations This was a careless error on our part. - Instead of `#false` we mean to use a unique sentinel value. + We meant to use a unique sentinel value. -------------------------------------------------------------------------------- @@ -171,31 +118,25 @@ Thanks! We removed casts around every call to `regexp-match` we found in typed code. But that was only 10 calls and unfortunately we found no typed programs - using SQL. + using SQL. - Besides removing casts, the library is also useful for early detection of - bugs when writing programs. - Our personal experience has been good and we are currently in the process - of soliciting feedback from Typed Racket users + But aside from removing casts, the library is also useful for early detection + of bugs when writing programs. + Our personal experience has been good and we are currently soliciting + feedback from Typed Racket users -------------------------------------------------------------------------------- ---- RA, re: type error messages +--- RA, re: the quality of type error messages - The error messages have been surprisingly good. - When we can immediately reject a program (due to out-of-bounds vector access, - 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. + Compile errors raised by our implementation point out exactly what values + caused the local transformation to fail. These are easy to read. + Type errors raised in post-elaboration code are (so far) caused by introduced + type annotations. These errors are concise, but could use more context. --------------------------------------------------------------------------------- ---- RA, re: small comments - - Thanks for showing us the Formatting package! - We thought Template Haskell was the Haskell programmers' only way to safety. + e.g. the error for (printf "~b" 3.14) says that 3.14 has the wrong type, + but does not cite the format string "~b" as the reason why. -------------------------------------------------------------------------------- @@ -203,17 +144,20 @@ Thanks! gcc does indeed print a warning for invalid & mismatched format specifiers. It also complains when called on non-literal strings. + OCaml also catches printf type errors. - We will say "many" languages instead of "most". + We will say "many languages fail" instead of "most". -------------------------------------------------------------------------------- ---- RC, re: examples "don't really drive the point home" +--- RC, re: flow of Sec. 3 - 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. + RC writes: - (Doing so is a little tricky, as some examples cannot be run in Typed Racket, - others run with dynamic errors, and Sec. 3.6 requires an elaborate - work-around currently described in prose.) + "The example calls ... don't really drive the point home. + I would have expected a couple of examples along the + following lines: here is what I have to write without the + system and here is what I can write using the system." + + This is a weakness of our presentation. + We will clarify the problems solved by each example.