220 lines
8.6 KiB
Plaintext
220 lines
8.6 KiB
Plaintext
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.
|
|
|
|
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.
|
|
|
|
[[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.]]
|
|
|
|
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.
|
|
|
|
Like any other functional pearl, ours demonstrates a novel combination
|
|
of old ideas with concise, elegant code (basically functional rewrite
|
|
rules on syntax).
|
|
|
|
* Any programmer can use our technique to implement a type system
|
|
extension as a library. (The Typed Racket implementation is
|
|
validation.)
|
|
|
|
* Our technique is compositional. All examples are local transformation
|
|
that structurally traverse arbitrarily deep expressions to synthesize
|
|
[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 proof obligations for such basic guarantees are stated explicitly
|
|
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
|
|
ML's type system is 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.
|
|
|
|
================================================================================
|
|
=== 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.
|
|
|
|
* 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.
|
|
|
|
* 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.
|
|
|
|
* Rust's macros cannot implement our interpretation functions, but
|
|
their compiler plugins [5] 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
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- 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 same arity error.
|
|
|
|
But (printf "~a") is definitely a typo.
|
|
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 ⊥.
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- 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 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
|
|
|
|
|
|
-----------------------------------------------------------------------------
|
|
--- 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.
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- 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.
|
|
|
|
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
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- RA, re: 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.
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- RA, re: small comments
|
|
|
|
Thanks for showing us the Formatting package!
|
|
We thought Template Haskell was the Haskell programmers' only way to safety.
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- RB, re: "most languages fail at runtime" on printf
|
|
|
|
gcc does indeed print a warning for invalid & mismatched format specifiers.
|
|
It also complains when called on non-literal strings.
|
|
|
|
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 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.)
|