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

[rebuttal] add reviews

Browse Source
This commit is contained in:
Ben Greenman 2016-05-02 22:51:04 -04:00
parent 8ec7a50bae
commit 8264cab37b
1 changed files with 144 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

144
icfp-2016/icfp-reviews.txt Normal file
View File

@ -0,0 +1,144 @@
===========================================================================
ICFP 2016 Review #94A
---------------------------------------------------------------------------
Paper #94: Functional Pearl: Do you see what I see?
---------------------------------------------------------------------------
Overall merit: B. OK paper, but I will not champion
it
Confidence: Y. I am knowledgeable in this area,
but not an expert
===== Paper summary =====
This pearl discusses a non-intrusive approach to improving
bug finding in the context of Typed Racket. The paper first
discusses how the approach is organised (by means of
an interpretation and elaboration function), showcases
a number of examples, and then details the elements of Racket
that make it possible. The authors believe the ideas can
be translated to Typed Clojure, Rust and Scala, but no evidence
is provided (and given that many Racket elements are exploited,
one may question this).
===== Comments for author =====
This is a nice paper, quite easy to read and convincing in the
first part of the paper. The second part where we get to
the implementation is a bit less clear, but remains convincing.
I would like to see a discussion of the relation of your work
with Kostis Sagonas’ Dialyzer for Erlang (see
Konstantinos F. Sagonas, Josep Silva, Salvador Tamarit:
Precise explanation of success typing errors. PEPM 2013: 33-42).
Note the inconsistent use of capitals in section headers.
Questions to the authors:
* I assume it is possible that #false is an element of “val”. So what
happens to your interpretation function?
* I wonder (on p3) why printf “~a” fails, is that because “a” is not a correct
qualifier? How are we supposed to know that then? I also do not understand
why (printf “~b” 2) would lead to a static type error.
* p5: did you investigate how many casts and annotations were made redundant?
* when you let programs fail to type check, do you have any issues with the
type error messages you provide, or have you not looked at this?
Small comments:
p1 footnote: rather thaN
p2c1: what is “wrong” in your third stated property?
p2c2: if you need an example of a language where it does not fail at runtime,
you can mention the Formatting package by Chris Done for Haskell.
p5c2: the result of (vector-length #(0 1 2)) is 3 on my install of Typed Racket.
p7c1: propAgated
===========================================================================
ICFP 2016 Review #94B
---------------------------------------------------------------------------
Paper #94: Functional Pearl: Do you see what I see?
---------------------------------------------------------------------------
Overall merit: B. OK paper, but I will not champion
it
Confidence: Y. I am knowledgeable in this area,
but not an expert
===== Paper summary =====
This paper shows how an elaboration technique can be used to interact with the Racket type checker to make it more precise, on a number of different examples.
===== Comments for author =====
The paper is unclear in its purpose. Is it about the elaboration mechanism? Is it about the use of this mechanism to add more static types? Or is it about the applications of this type-introducing elaboration mechanism that are in the paper?
I think the most interesting would be the latter. There have been languages with elaboration mechanisms like this one for a long time (once I saw someone add Hindley-Milner typing to Prolog, implemented in a few lines using Prolog's elaboration mechanism).
However, the paper is spending an awful lot of time on the former.
I would really like to see more details on everything that is done in section 3.6, this seems to be where the cool stuff is! But all we get to see is a glimpse at the top-level (which is very un-pearl-ish!).
Comments:
From the introduction, one gets the impression that the technique in the paper is just a library, but in section 2 you say that one also needs elaborators. Perhaps this is good to say in the intro already.
I miss a more honest discussion on how this technique relates to type systems. A pure type system based solution would be compositional (meaning that you can replace a sub-expression with another one of the same type, and everything still type checks, and if the expressions have the same meaning, the program will still do the same thing). A type system gives you guarantees.
It seems that with your technique, you have neither compositionality nor (easily definable) guarantees. (But your technique is still very useful!!)
"most languages fail at runtime" - AFAIK, printf type checking (reading the static string argument) exists in C (gcc).
What happens when you elaborate (printf "~b"), the same as just printf I suppose? Then, explain that the (printf "~a") fails is because "~a" is not a valid format.
5.4: In the intro, you claim the technique can also be implemented in languages like Scala, but these languages do not have the same sophisticated macros as Racket. ?
===========================================================================
ICFP 2016 Review #94C
---------------------------------------------------------------------------
Paper #94: Functional Pearl: Do you see what I see?
---------------------------------------------------------------------------
Overall merit: C. Weak paper, though I will not fight
strongly against it
Confidence: X. I am an expert in this area
===== Paper summary =====
The pearl describes a small Typed Racket library for detecting value
errors and expressing polymorphism over values. The idea is to help
the type-checker not through manual type annotations, but through a
collection of upstream interpreters/elaborators that analyse and
annotate the program.
===== Comments for author =====
The pearl starts off quite promising - most if not all functional
programmers will know the problem of fighting the type-checker to make
it accept a working program. However, the paper quickly becomes
technical and as a consequence slightly unexciting. I couldn't help
feeling that this is a (short) research paper dressed up as a pearl.
The first time I struggled was on Page 1, when the first example was
discussed. I don't know about regular-expression matching in Racket
and the pearl wasn't very helpful either: I wondered why regexp-match
returned three strings when only one sub-string matched. I only
realized much later (on Page 3) that the sentence leading up to the
example was wrong. Also I stopped reading after the first paragraph
following the code, wondering why this example illustrates any
features of the library. When I finally continued reading, I noticed
that the actual example was given in the following paragraph. (In
other words, you shouldn't start a new paragraph at this point.)
Section 2 and the first part of Section 3 (Conventions) are rather
technical. I could have done without those - a more condensed
description of interpretations and elaborations is called
for. Sections 3.1-3.6 detail some examples. The example calls mostly
show interpretations and elaborations in action, but they 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. Finally, Section 5,
which details the implementation, wasn't very appealing to a
non-Racket programmer (perhaps my fault) as I felt that too much
specialist knowledge was needed.
Overall, I didn't fully understand why this was submitted as a
Functional Pearl, rather than a (short) research paper.