suzanne.soy/trivial
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[rebuttal] 2nd draft

Browse Source
This commit is contained in:
Ben Greenman 2016-05-03 15:10:11 -04:00
parent 522b407b53
commit 7e601b0ad8
1 changed files with 51 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
icfp-2016/rebuttal.txt
View File

@ -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.)