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

[rebuttal] typo + redo detailed comments

Browse Source
This commit is contained in:
Ben Greenman 2016-05-03 23:16:39 -04:00
parent ddf5a59948
commit 992412f525
1 changed files with 48 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

152
icfp-2016/rebuttal.txt
View File

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