Dear Haskell 09 author, I regret to inform you that your paper was not selected by the program committee to appear in the Haskell 09 Symposium. This year we received 31 submissions, of them, 12 were accepted. Overall, the quality of submissions was extremely high. Many good papers could not be included. I do hope that you will be able to attend the Symposium. I include below the reviewers' scores and comments. I hope they will offer you guidance in revising your paper. If you have any additional questions, please feel free to contact me. Thank you for submitting to Haskell 2009. Stephanie Weirich Haskell 2009 Program Chair --------------------------------------------- Paper: 15 Title: Controlling Non-Determinism in Type Rules using First-Class Guessing -------------------- review 1 -------------------- PAPER: 15 TITLE: Controlling Non-Determinism in Type Rules using First-Class Guessing OVERALL RATING: 2 (strong accept) REVIEWER'S CONFIDENCE: 4 (expert) Novelty: 3 (Quirky, attacks a new problem or proposes a completely new solution) ----------------------- REVIEW -------------------- Summary The paper describes a domain specific language (DSL) that aims to simplify the task of implementing type checkers/inferencers for new type systems. It is aimed at language researchers who are interested in experimenting with new type systems. Programs in the DSL are specifically designed to resemble the declarative specifications of type systems. One of the big challenges that the authors had to overcome is that such specifications are inherently non-deterministic (i.e., rules often require "guessing" of types), and the DSL mechanisms to manage this non-determinism. The solution is based on techniques similar to logic programming where unification variables stand for guess, and execution can be "suspended" until more information is available about a particular variable. What I Found Interesting I find the following aspects of this work interesting: (i) I think that the DSL presents a nice way to structure the implementation of a type checker, presenting the algorithm at a much higher level of abstraction then a typical implementation. (ii) It would be interesting to see what variety of type systems could be implemented in the DSL. The examples provided by the authors are certainly sufficient to illustrate that the DSL could be used in practice. However, given that the DSL is intended to help researchers experiment with new type systems, it would be interesting to see how well it works on other examples (e.g., qualified types, sub-typing, row unification, effect systems, etc.). (iii) The DSL is embedded in Haskell, and as such, it provides an interesting example of how to design DSLs in Haskell. Personally, I wished that the paper went into more detail about the concrete Haskell implementation of the DSL, which I think would have been more useful for my work Writing Style Overall, the paper is well written, and very well structured. My only complaint would be that I found some of the mathematical notation used hard to follow: in particular, I thought that the large number of super- and sub-scripts, in combination with the very short variable names (in greek!) made the rules and syntax harder to follow, despite the fact that it is more compact. -------------------- review 2 -------------------- PAPER: 15 TITLE: Controlling Non-Determinism in Type Rules using First-Class Guessing OVERALL RATING: -1 (weak reject) REVIEWER'S CONFIDENCE: 2 (medium) Novelty: 1 (Solid, extends existing work in a straightforward direction) ----------------------- REVIEW -------------------- This paper presents a domain specific language, Ruler, for implementing type inferencers, in which non-determinism is handled by explicit "defer" statements that introduce "guesses"--unknown metavariables--along with code to run once the guesses are resolved. There are features for committing a value to a guess, and for "fixating" a guess, which means essentially replacing it by a skolem constant--after fixation, it may not match any other value. There are examples of type inferencers specified in Ruler for simply typed lambda calculus, implicitly typed System F, and the FPH type system. There follows a long and heavy formalisation of Ruler itself. I found this paper tough going. The formal description of Ruler is complex, and the paper focusses more on describing it than motivating design choices. It didn't help me that the examples in section 2 were presented in a DIFFERENT language than the one formalised later on, as explained in section 4.2. Bits of the syntax were simply left out, "because it was clear from the context"---but not to me, when I was trying to understand the Ruler language itself! I'm actually still not clear what the status of Ruler is, in part because its concrete syntax seems to require many greek letters and other mathematical notation. Is there a real implementation? What does the actual concrete syntax look like... LaTeX source, or something else altogether? It's hard to judge how attractive the language really is to use, when the real concrete syntax is not presented, and parts of the specifications are omitted because they are obvious. p5: Two instantiations of the type of choose are given, but choose hasn't been defined! What is it? p9: I can't follow your explanation of force. I dare say there is interesting work here, but it is obscured by the complexity of the description. I'd like to see it simplified and presented with much more motivation for the design. -------------------- review 3 -------------------- PAPER: 15 TITLE: Controlling Non-Determinism in Type Rules using First-Class Guessing OVERALL RATING: -1 (weak reject) REVIEWER'S CONFIDENCE: 3 (high) Novelty: 2 (Average) ----------------------- REVIEW -------------------- This paper describes what is, in effect, a domain specific language called Ruler for constructing type inference engines in Haskell. My understanding from comments in the paper is that a preliminary version of Ruler was described in a previous publication and that this version describes new features (such as defer, fixate, commit, and force) that support non-determinism and "guessing". The paper begins with a sequence of examples that show how three increasingly sophisticated type inference engines can be described in Ruler, including an explicitly typed lambda calculus (which requires guessing to determine the type of the argument in a function application); implicitly typed System F (which requires additional guessing to determine appropriate instantiation and generalization over type variables); and then FPH (which requires still further guessing to support impredicative instantiation). The fact that Ruler is able to handle all of these examples provides good evidence that the language is general enough to handle a wide range of type system designs. The similarities between the original formulations of the type systems and the encodings in Ruler provides good evidence that the language is well-tuned to the needs of this particular domain. Some questions remain. For one thing, I don't have a good sense of how much benefit is obtained from using Ruler directly instead of building up a type inference engine in Haskell by hand, perhaps by using a custom library of combinators, including some to support guessing. Clearly, the concrete syntax of Ruler (i.e., the notation that the programmer actually uses to enter and maintain the description of a type system) makes it possible for the associated toolset to generate the attractive, mathematical displays that are shown in the paper. This would be much harder if the tools were expected to start with arbitrary Haskell code as their source. Then again, the Haskell fragment for type checking an application in the first column of Page 3 already seems quite clear as written and would not require me to learn a new language first. Perhaps this issue was addressed in the earlier paper, but I haven't been able to read that during this review process. If I wanted to build a new type inference engine, why would I choose to use Ruler that purpose, what advantages would that give me over Haskell, and where might I expect to run in to limitations? Another concern has to do with correctness: is the resulting type inference engine for FPH, for example, a faithful implementation of the FPH type system? Does it agree with the definition and the implementation provided by the original designers of FPH? I recognize that these are difficult questions to answer. I don't know how I would answer them definitively myself, although I think I might start by putting together a collection of test vectors (i.e., sample programs, including some that are well-typed and others that are not well-typed) and then compare the two implementations to see if they agree. I missed seeing any evaluation, even at this very informal level, as part of the paper. The fact that the code looks like the definition of the type system isn't a terribly persuasive argument, as the System F example illustrates: That system is known to be incomplete, and hence we can be completely certain that the generated type inferencer will not be entirely "correct" in that particular case. Finally, I would have liked the authors to have been more explicit in describing the intended role for the operational semantics that fills the last quarter of the paper. It seems like a solid technical development, but how is it expected to be used? Are you planning to build a Ruler interpreter? Are you wanting to provide tools for demonstrating equivalences between type systems expressed in different ways in Ruler notation? Are you looking for a way to validate your translation from Ruler in to Haskell? And given that Ruler already includes embedded Haskell fragments, why is the translation from Ruler into Haskell not enough already to give a suitable semantics? It feels like as if component of the work is part of a bigger and grander plan for future work that is not fully explained in this paper. In fairness to other submissions, I didn't do anything more than skim the appendices since these were beyond the twelve page limit. The two topics mentioned there, however, both seem interesting: static semantics would presumably allow direct type checking and validation of Ruler specifications without having to translate them in to Haskell first. "Soundness almost for free" suggests that a significant benefit might be obtained as a result of expressing a type inference algorithm in Ruler if this could provide a quick and "almost free" guarantee of soundness. Again this leads me to wonder if I have missed something important in the author's decision to spend time in the body of the paper on their operational semantics, when the topics in the appendix would appear to me to have more immediate benefit and impact. I regret that I was not able to understand these choices better from the paper. Overall, I think this paper presents strong technical work. The biggest strength is in presenting a very general language (with good evidence of applicability) for describing a broad range of type inference algorithms. The biggest weakness to me appears to be in the lack of methods for effective evaluation of Ruler descriptions. Trivia: Page 1: "such a guesses" should be "such guesses" "observe them, impose requirements" insert "and" after the comma Page 2: "We have proof-of-concept<,> Haskell-based" (added items enclosed in ) "This >is< information is given" (delete items between >...<) Page 3: The indentation of the code in the second column (fr_fresh, for example) looks wrong. Shouldn't the where clause be indented more than the main definition? "produces a>n< guess" It would probably be good to mention, at the outset of Sec 2.2, that type inference for implicitly typed System F is known to be undecidable, perhaps including a citation, instead of leaving this observation to the end of the section. Page 4: ">this< should then be equal to \tau_2" "during >the< execution and remain " Page 5: "Compare the FPH's declarative rules ... and be surprised ..." would probably be better as: "Comparing FPH's declarative rules ... shows ..." "the Gen.Lazy generalizes again" Page 7: "Thus, this leaves the gap wide open, and we close it with this work" might be better as: "This left a gap that we have attempted to close in this paper" "delay >the< execution" "but also on >the< scrutinizing >of< the" "from formal name to actual name" -------------------- review 4 -------------------- PAPER: 15 TITLE: Controlling Non-Determinism in Type Rules using First-Class Guessing OVERALL RATING: 1 (weak accept) REVIEWER'S CONFIDENCE: 3 (high) Novelty: 3 (Quirky, attacks a new problem or proposes a completely new solution) ----------------------- REVIEW -------------------- Technical summary: ================== The paper presents the Ruler framework for deriving type inference algorithms from type system specifications. The designer of the type system has to factor non-determinism in some way (not clear how) without having to eliminate it entirely (not clear how much non-determinism should remain) and then the framework can derive /some/ inference algorithm for that type system. Key to be able to handle advanced type systems is the ability to specify deferring the choice of values in the specification, and executing statements that depend on deferred "guesses" later, once the choices have been fixed from somewhere else. The FPH type system for first-class polymorphism is given as an extensive case study of the features of the Ruler framework. Short opinion: ============== The proposed work is novel, gives a very elegant way to handle non-determinism and deferring in type system specifications, and seems powerful enough to handle advanced type systems. It is also extremely interesting and I can see it being useful when experimenting with new type system features as it offers fast prototyping. (For example it proposes a new algorithm for FPH which is likely to be (almost) complete that (i) deviates from the MLF/FPH algorithm and (ii) is *solely* based on ordinary unification / generalization / instantiation *plus* (and here is the trick) deferring. That is very amusing!) On the other hand, it is not entirely clear which precisely is the task of the type system designer in refactoring the rules to write them within the framework (especially the removal of non-determinism), and related to that, when the resulting algorithms are complete with respect to the original specifications. The presentation is a bit confusing at several points too. Also the system presented as FPH is just some restriction of FPH -- though it is not hard to see that probably the full-blown one still can be expressed in Ruler. In conclusion, this work is publishable, but I believe it would greatly be improved if the authors addressed the previous issues, also to be described in detailed below. High-level comment: =================== From the introduction and the abstract the reader gets the impression that *non-syntax-directed* type systems are handled, and that there is an automatic derivation of algorithms for them. (The confusing word was "declarative" I guess) However, in all examples, the rules are syntax-directed and non-determinism is restricted to some form of guessing types. But later, once the semantics of defer are given, we see that it may encode pretty much arbitrary non-determinism. Then, the reader is left with an unclear opinion: Are non-syntax-directed type systems encodable? How much non-determinism fits there? In the whole paper we see *no* example of what Ruler *cannot* do (or what the derived inference engines would fail to type-check). Is there something that goes bad if we leave some *more* non-determinism in the rules? Not clear. Detailed comments: ================== Figure 2, pg 6: Give the types of the various functions and write the mkDeferValue and mkFixedValue fully applied to emphasize that (TGuess) and (TConst) accept arguments. pg 2, last para: The d-flag is explained (type has to be instance of Deferrable) but the u-flag is not. Unifiable? pg 3, lk_lookup code: I think that part of the figure is confusing and should be moved below, where non-determinism is explained. The reader never gets an explanation about what is the "f" argument in the "defer f" call, nor what is the type of "v". In the second to last paragrap the authors write: "produces an guess v". What is the type of v? Just a variable which is instance of Deferrable? pg 3, last sentence: "opaque guess variable ... wrapped into the domain of v" This is extremely vague. What is the "domain of v"? What is an "opaque guess variable"? pg 4, first column: I started getting disappointed when I noticed that the authors chose to manually impose a preference on where instantiations / generalizations happen. Is this an intrinsic limitation of the system? Couldn't "defer"-non-determinism solve it? pg 4, Figure 4: * In rule GEN.LAZY, would it make a difference if we put also G |- e : tau1 inside the defer guard statement? (On the other hand, I can see that we do not want to fixate tau1 too early in GEN.LAZY so that tau2 gets only just as polymorphic as we want, and not more. Neat :-) (BUT YOU NEVER EXPLAIN!) pg 5, FPH figure: * This is not a big point for the paper, since it makes no completeness claims but I do not immediately recognize the Figure 6 as the FPH type system: 1) there is no rule for generalization 2) instantiation happens only on variables 3) abstraction bodies may return (unboxed) polymorphic types Because of (1) and (2) the resulting type system is quite different. On the other hand, the syntax-directed version of FPH does fix the places of instantiation / generalization happens, so the full-blown FPH is also probably encodable (we would have to use some GEN.LAZY tricks but ok) pg 5, last sentence: "alternative of a type"??? pg 6, Figure 7: Explain in detail the non-deterministic choices in Rules INST.V and in the protected unboxing rules. Forcing and committing inside deferred statements is hard to understand. also: in BOXY.INST why return "b2" and not directly "b1"? Not clear. pg 8, para "The defer statement ..." "for outputs n*" should be "for outputs m*" pg 8, 2nd column, "The I monad ... support failure" <- "supports failure" pg 9, section 5: I am not sure that a direct operational semantics helps more than just giving the monadic translation (i.e. Haskell implementation). Or is there an abstract machine that executes Ruler implemented? (I think not) pg 11, Figure 17 and paragraphs below: From the text and the figure, it is not clear how non-deterministic choice is done. We just choose one of the choices. In real implementation terms does that mean that that the algorithm has to perform some kind of back-tracking? This issue deserves some discussion.