[rebuttal] post-meething
This commit is contained in:
parent
7e601b0ad8
commit
053c44aa78
|
@ -1,30 +1,23 @@
|
||||||
0. We thank all three reviewers for their extensive comments.
|
0. Thanks!
|
||||||
This pearl is certainly intended for an audience with no knowledge of Lisp
|
|
||||||
or Racket and reviewer 3's remarks about the level of technical detail are
|
|
||||||
very welcome.
|
|
||||||
We will clarify the motivating example and give Section 3 a friendlier
|
|
||||||
introduction.
|
|
||||||
|
|
||||||
|
|
||||||
1. The purpose of this pearl is to describe a language agnostic technique
|
1. The purpose of this pearl is to describe a language agnostic technique
|
||||||
for augmenting a traditional type checker.
|
for augmenting a traditional type checker.
|
||||||
|
|
||||||
Typed Racket is irrelevant to our technique.
|
|
||||||
If this paper is accepted, we plan to use Rust for demos in the talk.
|
2. We use Typed Racket to illustrate the technique ONLY because the
|
||||||
|
choice allows us to fit the ENTIRE core implementation in Sections 5.1
|
||||||
|
and 5.2.
|
||||||
|
|
||||||
|
[[ Section 5 illustrates the power of Racket's macro expander,
|
||||||
|
but this has been shown many times before. ]]
|
||||||
|
|
||||||
|
|
||||||
2. Our secondary purpose was to advertise macros and show off a
|
3. It is correct that neither our elaboration mechanism nor our examples
|
||||||
concise implementation made possible by Racket.
|
in Section 3 are new. That is precisely why this is a PEARL.
|
||||||
The latter half of Section 5 is a list of features for GHC/Scala/...
|
|
||||||
developers to consider implementing.
|
|
||||||
|
|
||||||
Language implementors and users like Chris Done who stretch their favorite
|
Like a functional pearl written in any other language, our pearl demonstrates
|
||||||
language are the "adventurous readers" for whom we intended Section 5.
|
a novel combination of old ideas with concise, elegant code.
|
||||||
|
|
||||||
|
|
||||||
3. Reviewer B is correct that the elaboration mechanism is not new.
|
|
||||||
None of our applications are new either.
|
|
||||||
But we hope to have shown an interesting and useful combination of old ideas.
|
|
||||||
|
|
||||||
* Our technique can be implemented by language users i.e. as a library.
|
* Our technique can be implemented by language users i.e. as a library.
|
||||||
(The Typed Racket implementation is proof.)
|
(The Typed Racket implementation is proof.)
|
||||||
|
@ -44,7 +37,7 @@
|
||||||
|
|
||||||
We chose our examples to suggest theorems that a user might want to prove
|
We chose our examples to suggest theorems that a user might want to prove
|
||||||
about their own implementation of the technique.
|
about their own implementation of the technique.
|
||||||
This purpose will be made clearer.
|
|
||||||
|
|
||||||
================================================================================
|
================================================================================
|
||||||
=== END OF FORMAL RESPONSE. Detailed comments to reviewers (RA RB RC) follow.
|
=== END OF FORMAL RESPONSE. Detailed comments to reviewers (RA RB RC) follow.
|
||||||
|
@ -176,9 +169,8 @@
|
||||||
|
|
||||||
Besides removing casts, the library is also useful for early detection of
|
Besides removing casts, the library is also useful for early detection of
|
||||||
bugs when writing programs.
|
bugs when writing programs.
|
||||||
Our personal experience has been good.
|
Our personal experience has been good and we are currently in the process
|
||||||
We did ask Typed Racket users for feedback, but unfortunately got no response
|
of soliciting feedback from Typed Racket users
|
||||||
at the time (three months after the library was initially released).
|
|
||||||
|
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
@ -216,6 +208,6 @@
|
||||||
If permitted, we will reorganize to show how the examples run in Typed Racket
|
If permitted, we will reorganize to show how the examples run in Typed Racket
|
||||||
and compare to our library.
|
and compare to our library.
|
||||||
|
|
||||||
(Doing so is a little tricky, as some are runtime errors, some are type
|
(Doing so is a little tricky, as some examples cannot be run in Typed Racket,
|
||||||
errors, and Sec. 3.6 requires an elaborate work-around. But we can manage.)
|
others run with dynamic errors, and Sec. 3.6 requires an elaborate
|
||||||
|
work-around currently described in prose.)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user