Stefan pushed to branch report/els-2017 at Stefan / Typer

Commits: d118f4c6 by Stefan Monnier at 2017-03-12T23:38:55-04:00 Add ELS17 reviews

- - - - -

1 changed file:

- + REVIEWS

Changes:

===================================== REVIEWS ===================================== --- /dev/null +++ b/REVIEWS @@ -0,0 +1,215 @@ +-*- org -*- +* ELS'17 +** ----------------------- REVIEW 1 --------------------- +PAPER: 14 +TITLE: Typer: An infix statically typed Lisp +AUTHORS: Pierre Delaunay, Vincent Archambault-Bouffard and Stefan Monnier + +Overall evaluation: 1 (weak accept) + +----------- Overall evaluation ----------- +The paper has merit in exploring the combination of mixfix syntax and lisp +style macros, and interleaved type inference and +macro-expansion. I recommend it for acceptance with some modifications. + +The text wastes two pages out of eight on explaining why macros are a good +idea, and how lisp parsing works: the first can be assumed as a given +in a Lisp-conference, and the second is relatively irrelevant and can also +mostly be assumed as a given. + +In contrast the text is quite light on details of the syntax and typing: it +assumes readers to be familiar with ML-family languages. In general this is +probably a fair assumption for any paper dealing with statically typed pure +functional languages, but possibly somewhat out of place +for a Lisp-conference. + +A paper obviously has a shelf-life far longer than the conference it appears +in, but some adjustment to expectations placed on the reader would be +beneficial. A small section exploring the costs and benefits of mixfix +syntax would be desirable as well. + +One of the most interesting parts of the presented language is the +interleaved type inference and macro-expansion, which the paper skims over +rather lightly. This would deserve elaboration, since it seems to be one of +the major features here. Syntaxes and parsers are a dime a dozen, though the +one presented is noteworthy for elegant integration of macros outside +S-expressions, but getting a proof-system out of macro-system by +interleaving it with type inference? That’s interesting. + +Detailed notes: + +Section 2.1 on S-expression parsing is not only largely needless, but +somewhat problematic as well. It seems to conflate structural parsing and +semantic analysis. + +Section 2.2 states that Lisp gets rid of difference between declarations and +expressions, which is manifestly not true for Common Lisp -- but that +difference is semantic, not structural: consider DECLARE and PROCLAIM, which +cannot appear in arbitrary places. Conflation of structure and semantics +again. From parsing point Lisp has only expressions, from execution point +this is not true. From the point of view of the paper this expressing this +distinction is meaningless, but having the language changed so that it +doesn’t actually state things that are untrue would be good. + +Section 2.2 also states that there are syntactic categories for symbols and +lvalues, but this is stretching those definitions and possibly +misunderstanding workings of SYMBOL-MACROLET and SETF-functions and macros: +they cannot be considered syntactic categories in any real +sense. Possibly a reflection of how assumptions built into mainstream CS +discourse don’t properly map 1:1 to fringe languages like Common +Lisp. However, as above, the distinction here doesn’t really matter for +the paper. + +Section 2.5 explores different macro implementation strategies, and is just +noise. The second bullet is overly vague and hard to understand. The third +bullet makes a weak and incorrect claim about particular implementation +strategy “typically implying that macros cannot be used in the file where +they are defined”. (That implementation strategy makes it more work, but not +terribly much so.) + +Recommend condensing entirety to 2.* sections: instead of trying to sort out +the problematic comparisons to Lisp just remove them. + +Section 3. Flippancy about hiding the scary Greek letter is out of place and +reads as somewhat condescending, which is probably not intentional. This is +the section that needs most clarification if audience is not assumed to be +fluent in ML-family languages. Given an audience of lispers use of +parenthesis should be clarified early on, instead of saved for section +4.2… :) + +Section 4 starts with a bizarre claim that Lisp’s parsing is in +3 steps. Some implementation might, but it’s an awfully strange way to look +at things. Again, the way Lisp may or may not do things doesn’t really +matter for this paper: keep the focus on Typer. + +Section 4.1’s contra-OCaml example near the end is tad confusing, possibly +due to overly tautological example. The note about altered precedence of ‘;’ +in OCaml is a good one, and deserves an example, but if possible some +clarification might be in order. + +Section 4.2 neglects to mention what [] actually do. Presumably they are +tuple of list constructors. + +Section 4.3 mentions a small set of default single-char tokens. If this set +can be user-extended, that’s worth a mention. + +Figure 3. Papers can be serious without using excessively terse +names. “arw”, “con”, “adt”. Not critical, but using readable names would +be nice. + +Section 5.1. Should at least mention which cases require special handling, +even if only function call elaboration is sketched out. + +Section 5.3. Why is “one big elaboration phase” a “significant downside”? It +seems to be one of the major strong points of the design. Would like to see +some elaboration, maybe a small example, on how the interleaved type +inference and macro expansion allow for macros to work as proof +tactics. This seems both novel and interesting. + +Section 6.3. Comparison to typed Racket mentions that this is a non-hygienic +system. It is not obvious to me that this is a deep property of the +presented macro-system: either this needs to be clarified, or the +intentional design choice should be mentioned up-front. + +Section 7. Does not actually discuss future work, so might just call +it Conclusions. + + +** ----------------------- REVIEW 2 --------------------- +PAPER: 14 +TITLE: Typer: An infix statically typed Lisp +AUTHORS: Pierre Delaunay, Vincent Archambault-Bouffard and Stefan Monnier + +Overall evaluation: -3 (strong reject) + +----------- Overall evaluation ----------- +This paper discusses some details about the language, Typer, which +seeks to integrate a variety of ideas of syntax with some ideas about +type systems. The paper has as an introduction to macros, a discussion +of the Typer reader, and a bit about its type system. The paper +includes no evaluation of any of its components. Each component is not +explained in enough detail to represent a contribution of +knowledge. Related work is treated carelessly. The intriguing parts of +the system are only hinted at with most of the paper time being +focused on minutiae and broad comments. + +--- Detailed Comments + +Sec 1 - Unprofessional writing + +1.47 - Many other static Lisps + +3 goals are poorly explained. (Why does "language is functional" mean +there should be infix?) + +Sec 2 - Prose is better than a list in a paper. + +2.19 - This assumes the reader already knows what you're talking about +and doesn't actually explain. + +2.23 - What is an "S-exp"? + +2.42 - This is trite. + +Sec 2.1 - I think you want to read the Honu paper. + +Sec 2.2 - Because Typed Racket does something doesn't make it good. + +Sec 2 - This whole section has no flow and is just a list of stuff. + +Sec 2.4 - Why does this actually matter though for your system or for +programmers? + +Sec 2.5 - What is the beginning of this section referring to? + +Sec 2 - This entire section was a waste of space. It doesn't really +add anything to your contribution and is not a novel explanation. + +3.11 - This is trite. + +Sec 3 - The repeated use of "Notice" and "Note" is bad style and +exposes that your explanation is not thorough or thought out. + +3.40 - What is this? + +Sec 3 - It would be interesting for you to elaborate what is +problematic about declarations being expressions. We don't know enough +about your language at this point to understand what the problems +could be. + +Sec 3 - The most important part of this section is not the run through +of your Haskell-like syntax; it is the discussion of the +macros. Unfortunately, you don't explain why a monad is necessary or +how we are supposed to understand the definition of `mylet`. In +particular, there appears to be no effect, so why the monad? + +4.21 - "You can think of" ... is very unprofessional + +Sec 4 - The choice of OPG is actually interesting, but the most +interesting part of the design choice is pushed to small bullets +rather than a true explanation of the trade-offs and analysis that led +to the choice. + +Sec 4.2 - I like these examples, but I would like to know exactly what +the numbers and the pairings are because you've explained OPGs that +way. At this point in the paper, its purpose is very unclear: is this +a paper about a type system? That's what the introduction made me +assume, but then I thought it was a paper about macros, but now I +think it is a paper about reading and parsing. The introduction does +not serve the paper by providing a guide to how the rest should be +read. + +5.56 - I don't understand this paragraph. How can you do that and why +do you want to? + +Sec 5.1 - This is bewildering because it seems like the type checker +is the most important part, but you say that it is outside of the +paper's scope! + +6.53 - I don't see any connection between closedness and phases. Phase +separation is about separate compilation and modularity. + +Sec 5 - The last paragraph is very bizarre because it throws in a +totally new topic that has never been hinted at before that seems +fascinating. Unfortunately, we have no explanation! +

View it on GitLab: https://gitlab.com/monnier/typer/commit/d118f4c6d975d600949b106547d996985384...