From 203fcf2fbfcb1646ff235522e7c22a990fac67b8 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Wed, 4 May 2016 17:38:08 -0400 Subject: [PATCH] [rebuttal] add todays matthias comments --- icfp-2016/rebuttal.txt | 115 ++++++++++++++++------------------------- 1 file changed, 45 insertions(+), 70 deletions(-) diff --git a/icfp-2016/rebuttal.txt b/icfp-2016/rebuttal.txt index b06880f..ee4872f 100644 --- a/icfp-2016/rebuttal.txt +++ b/icfp-2016/rebuttal.txt @@ -2,48 +2,44 @@ Thanks! 1. The purpose of this pearl is to describe a language-agnostic technique for augmenting the rich "simple" type systems of functional languages - ---via libraries that any programmer may implement and even prove correct. + via libraries that any programmer may implement and prove correct. 2. Typed Racket serves as the vehicle for a sample implementation for a - range of concrete augmentations, because it allows us to fit the ENTIRE - CORE IMPLEMENTATION into the paper. We will supply the remaining few - bits. The existing page limits accommodate this addition; more than - suffices; we just thought they were too obvious. + range of concrete augmentations because it allows us to fit the + entire core implementation into the paper (Sections 5.1 and 5.2). - [[The pearl also illustrates the power of Racket's macro expander once - again, but this has been shown many times before and is NOT the goal.]] + [[The pearl once again illustrates the power of Racket's macro expander, + but this has been shown many times before and is not the goal.]] 3. It is correct that neither our elaboration mechanism nor our examples in - Section 3 are new. That is precisely why this is a PEARL and NOT A - RESEARCH PAPER. + Section 3 are new. That is precisely why this is a *pearl* and + not a research paper. - Like any other functional pearl, ours demonstrates a novel combination - of old ideas with concise, elegant code (basically functional rewrite - rules on syntax). + Like a functional pearl written in any other language, ours demonstrates + a novel combination of old ideas with concise, elegant code. * Any programmer can use our technique to implement a type system - extension as a library. (The Typed Racket implementation is - validation.) + extension as a library. The Typed Racket implementation is validation. - * Our technique is compositional. All examples are local transformation + * Our technique is compositional. All examples are local transformations that structurally traverse arbitrarily deep expressions to synthesize - [check] types in a hierarchical manner. + and check types in a hierarchical manner. - * The guarantees for an augmented type system are as strong as a type - system designed in a holistic manner. + * The guarantees for an augmented type system are as strong as the + guarantees for a type system designed in a holistic manner. The proof obligations for such basic guarantees are stated explicitly - in section 2. + in Section 2. - Specific guarantees like "the new division function raises + Specific guarantees like "the augmented division function raises 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. + ML's type systems are proven correct. - The examples are chosen precisely because they suggest theorems that a - programmer might wish to prove. Doing so is, however, beyond the scope - of a pearl that demonstrates how unusual but elegant functional code - can achieve this highly desirable goal. + The code samples in Section 3 are chosen precisely because they suggest + theorems that a programmer might wish to prove. Doing so, however, is + beyond the scope of a pearl that demonstrates how unusual but elegant + functional code can achieve this highly desirable goal. ================================================================================ === END OF FORMAL RESPONSE. Detailed comments to reviewers (RA RB RC) follow. @@ -52,24 +48,12 @@ Thanks! -------------------------------------------------------------------------------- --- 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 and less documented. + Clojure's macros will run arbitrary Clojure code at compile-time. + Scala's compiler plugin API [1] allows custom source code transformations. + Rust's compiler plugins [2] are on-par with Scala's. - * Clojure's macros are arbitrary rewrite rules interspersed with - normal Clojure code run at compile-time. - - * 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 [3] are on-par with Scala's. - - Sources: - [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 + [1] http://www.scala-lang.org/old/node/8656 + [2] https://doc.rust-lang.org/book/compiler-plugins.html -------------------------------------------------------------------------------- @@ -77,23 +61,18 @@ Thanks! 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 same arity error. - These both compile in Typed Racket but fail at runtime. + arguments. Calling (printf "~b") would give the same arity error. + These both compile in Typed Racket and fail at runtime. - But writing (printf "~a") was a typo on our part. - We intended to use "~s" instead. - - The final version of the paper will give actual error messages instead of - using ⊥. + But writing (printf "~a") was a typo on our part. We intended to use "~s". -------------------------------------------------------------------------------- --- RA, re: Dialyzer 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). + Its guarantees match our third requirement for elaborations: + statically rejected programs will go wrong at runtime. The PEPM'13 paper is interesting, but orthogonal to our pearl. @@ -110,41 +89,36 @@ Thanks! --- RA, re: using #false in interpretations This was a careless error on our part. - We meant to use a unique sentinel value. + We meant to use a unique sentinel value, such as a gensymed symbol. -------------------------------------------------------------------------------- --- 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 we found no typed programs - using SQL. - - 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 + We removed casts around every call to `regexp-match` we found in typed code, + but that was only 10 calls. We have also found the library useful for + catching bugs in new code and have observed performance speedups on + microbenchmarks using fixed-size vectors, but a comprehensive experience + report is beyond the scope of the pearl. -------------------------------------------------------------------------------- --- RA, re: the quality of type error messages Compile errors raised by our implementation point out exactly what values - caused the local transformation to fail. These are easy to read. + caused the local transformation to fail. - Type errors raised in post-elaboration code are (so far) caused by introduced - type annotations. These errors are concise, but could use more context. - - 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. + Type errors raised in post-elaboration code are caused by introduced + type annotations on specific variables. -------------------------------------------------------------------------------- --- RB, re: "most languages fail at runtime" on printf - gcc does indeed print a warning for invalid & mismatched format specifiers. + gcc does indeed print a warning for invalid and mismatched format specifiers. It also complains when called on non-literal strings. - OCaml also catches printf type errors. + OCaml also catches printf type errors and as RA points out Haskell has a + library for safe formatting. We will say "many languages fail" instead of "most". @@ -159,5 +133,6 @@ Thanks! 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. + This is an easy-to-fix weakness of our presentation. We will clarify the problems solved by each example. +