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

[rebuttal] final version?

Browse Source
This commit is contained in:
Ben Greenman 2016-05-04 19:21:19 -04:00
parent 203fcf2fbf
commit 17ca97b697
1 changed files with 10 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
icfp-2016/rebuttal.txt
View File

@ -1,29 +1,26 @@
Thanks! Thanks!
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 the rich "simple" type systems of functional languages for augmenting the type systems of functional languages
via libraries that any programmer may implement and prove correct. via libraries that any programmer may implement and prove correct.
2. Typed Racket serves as the vehicle for a sample implementation for a 2. Typed Racket serves as the vehicle for a sample implementation of a
range of concrete augmentations because it allows us to fit the range of concrete augmentations because it allows us to fit the
entire core implementation into the paper (Sections 5.1 and 5.2). 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 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 Section 3 are new. That is precisely why this is a *pearl* and
not a research paper. not a research paper.
Like a functional pearl written in any other language, ours demonstrates Like any functional pearl, ours demonstrates a novel combination of
a novel combination of old ideas with concise, elegant code. old ideas.
* Any programmer can use our technique to implement a type system * Any programmer can use our technique to implement a type system
extension as a library. The Typed Racket implementation is validation. augmentation as a library. The Typed Racket implementation is validation.
* Our technique is compositional. All examples are local transformations * Our technique is compositional. All examples are implemented with local
that structurally traverse arbitrarily deep expressions to synthesize transformations. The macro expander composes these transformations into a
and check types in a hierarchical manner. complete structural recursive traversal.
* The guarantees for an augmented type system are as strong as the * The guarantees for an augmented type system are as strong as the
guarantees for a type system designed in a holistic manner. guarantees for a type system designed in a holistic manner.
@ -48,6 +45,8 @@ Thanks!
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
--- RA RB, re: translating the ideas to Typed Clojure, Scala, and Rust --- RA RB, re: translating the ideas to Typed Clojure, Scala, and Rust
These languages have sufficiently powerful syntax extensions.
Clojure's macros will run arbitrary Clojure code at compile-time. Clojure's macros will run arbitrary Clojure code at compile-time.
Scala's compiler plugin API [1] allows custom source code transformations. Scala's compiler plugin API [1] allows custom source code transformations.
Rust's compiler plugins [2] are on-par with Scala's. Rust's compiler plugins [2] are on-par with Scala's.
@ -92,26 +91,6 @@ Thanks!
We meant to use a unique sentinel value, such as a gensymed symbol. 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 --- RB, re: "most languages fail at runtime" on printf