139 lines
5.8 KiB
Plaintext
139 lines
5.8 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 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 (Sections 5.1 and 5.2).
|
|
|
|
[[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.
|
|
|
|
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.
|
|
|
|
* Our technique is compositional. All examples are local transformations
|
|
that structurally traverse arbitrarily deep expressions to synthesize
|
|
and check types in a hierarchical 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.
|
|
|
|
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 systems are proven correct.
|
|
|
|
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.
|
|
================================================================================
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- RA RB, re: translating the ideas to Typed Clojure, Scala, and Rust
|
|
|
|
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.
|
|
|
|
[1] http://www.scala-lang.org/old/node/8656
|
|
[2] 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.
|
|
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".
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- RA, re: Dialyzer
|
|
|
|
The Dialyzer belongs in our discussion of related work.
|
|
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.
|
|
|
|
- We are seeking to catch more runtime errors statically and allow more
|
|
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.
|
|
|
|
But their technique would be very useful for Typed Racket.
|
|
|
|
|
|
-----------------------------------------------------------------------------
|
|
--- RA, re: using #false in interpretations
|
|
|
|
This was a careless error on our part.
|
|
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. 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.
|
|
|
|
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 and mismatched format specifiers.
|
|
It also complains when called on non-literal strings.
|
|
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".
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
--- RC, re: flow of Sec. 3
|
|
|
|
RC writes:
|
|
|
|
"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 an easy-to-fix weakness of our presentation.
|
|
We will clarify the problems solved by each example.
|
|
|