=========================================================================== popl15 Review #213A Updated 24 Jul 2014 10:30:43pm EDT --------------------------------------------------------------------------- Paper #213: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: D. Reject Confidence: X. I am an expert in this area ===== Comments for the Authors ===== PAPER SUMMARY: TypeScript is an optionally typed dialect of JavaScript that flags certain kinds of errors at compile-time but does not provide any guarantees about run-time behavior. While optional type systems provide valuable programming support, there are of course situations for which sound types are desirable (e.g. checking correctness and enabling optimizations). This paper presents the design and implementation of StrongScript, a language that combines optional typing, in the style of TypeScript, with traditional "concrete" types. The paper reports that the implementation of StrongScript results in performance improvements on five microbenchmarks compared to an already-optimizing engine. OVERALL EVALUATION: Pros: + combining optional and concrete types could be useful for scripting languages + starting with TypeScript, a system that is used in practice, is good approach Cons: - unclear exactly how StrongScript differs from TypeScript - unclear what are the main challenges in combining optional and concrete types - weak evaluation Languages like TypeScript, Dart, and Hack provide value to programmers by helping to catch certain bugs and by enabling basic IDE support, so trying to extend these optional, unsound languages with the benefits of static types is a worthy goal. This is promising project, but unfortunately I do not think the presentation makes clear the technical contributions compared to related projects nor does the evaluation demonstrate the maturity of the tool. As a result, I do not think this paper is ready for publication. The first major problem is that the presentation does not make a clear case for what the language design aims to achieve. The discussion and comparison to TypeScript is vague and scattered throughout the paper. What is needed is a set of clear, well-chosen, realistic examples to demonstrate what one would like StrongScript to achieve that TypeScript doesn't. Furthermore, a clear comparison of the type systems is needed to explain why TypeScript makes the choices it does, what are the key challenges posed by combining optional and concrete types, and what are the aspects of StrongScript that address the challenges. The second major problem is that the evaluation of the implementation is very premature. To argue for the utility of StrongScript, larger benchmarks need to be studied both in terms of the guarantees and performance provided by concrete type annotations in StrongScript. MORE COMMENTS AND QUESTIONS: p.1: Why mention field accesses as the only parts of a program that can be optimized using type information? p.1: Instead of defining a property called "trace preservation", the discussion could instead talk about a Curry-style type system, where the static semantics are defined after the dynamic semantics are set (and hence cannot affect the behavior of programs). p.1: Does the "guarantee" for optional types (namely, "local guarantees that uses of a variable are consistent with declarations") mention anything about the dynamic behavior of the program? p.1: Why not refer to what StrongScripts adds as "gradual types" rather than "concrete types"? Is it because downcasts will not be inserted implicitly, only explicitly by the programmer? p.1: Isn't "trace preservation for optional types" trivial? It is for TypeScript, so why not for StrongScript? p.2: What does "fully optional typed" mean? And when annotated with concrete types, p.1 says "not trace-preserving" but p.2 says "will be trace preserving." p.2: Might want to preview the relationship to the recent formalization in [1]. p.2: It may be worth explaining some of the practical benefits of optional typing in languages like Hack, Dart, and TypeScript. Section 2: I find the background on optional and gradual typing to be longer than necessary to identify and motivate the current work. p.3: I find the term "type holes" to be strange. Instead, perhaps say "sources of unsoundness." p.3: Is it significant that, compared to Point, public has been dropped from the constructor of CPoint? p.3: Interface names X and Y would be more helpful than P and T. The variable names in the examples are not helpful. p.3: Perhaps break up the examples with some kind of section headers to identify what important features are being highlighted. p.4: "... and the run-time will still check all their uses." I thought optionally types did not provide any run-time guarantees. p.4: It strikes me as quite unusual that PtList is implemented as a subclass of Point. Is this example adapted from an existing benchmark? p.4: What are the interesting high level aspects of the StrongScript design? How does it compare to [1]? Is StrongScript just like [1] but with the three unsound rules changed? What effect do these changes have on programs that pass the TypeScript checker? p.4: Footnote 4 might make an analogy to "instance variables." p.4: Footnote 5 does not acknowledge that type abbreviations and syntactic sugar can alleviate much of the syntactic overhead of mu-types. Section 4.2: It is hard to get a high level idea of the design of StrongScript and how it relates to the formalization in [1]. Can there an explicit comparison be made between the two systems (in terms of typing rules and syntax) and their effect on programming examples? p.4: "Method stripping" is more commonly referred to as "method extraction". p.6: What evidence is being cited for the claim that "structural subtyping is rather brittle"? p.6: What does the mention of Thiemann refer to? p.6: The current work "ignore[s] references" but earlier in the paper Typed Racket was knocked for not support mutation. p.6: "Type annotations appearing in fields and method definitions in a class definition cannot contain undefined or function types." Why not? This seems to impose a rather severe restriction on programming. Section 5: The discussion in this section would be easier to follow if a more careful comparison between StrongScript and [1] had been made earlier. TODO look for proofs in Supp Material p.9: Many of the examples in the Implementation are used to compare StrongScript with TypeScript. This is the kind of comparison that should appear much earlier in the paper. p.10/11: How many lines of code are the benchmarks? What kinds of interesting type annotations are there? What kinds of errors are flagged in StrongScript but not in TypeScript? It's hard to conclude that the "type system does not limit expressiveness" based on these benchmarks. GRAMMATICAL PROBLEMS AND TYPOS: p.1: "Their design is geared" ==> "These designs are geared" p.1: strange to describe type annotations as "second class citizens" > p.1: "limitation" ==> "limitations" > p.1: "they central" ==> "they are central" > p.1: "as valid" ==> "are valid" > p.1: "capture" ==> "captures" p.1: "a any" ==> "an any" > p.2: "extended Truffle" ==> "extended the Truffle" > p.2: "properties access" ==> "property access" > p.2: "these language" ==> "these languages" > p.2: "Decades research" ==> "Decades of research" > p.2: "unlike TypeScript" ==> "unlike TypeScript," p.3: "in [1], we" > p.3: "erased, errors" > p.3: "declaration amongst" ==> "declarations in" > p.3: "expect, here" > p.3: "in covariantly" > p.3: "implicitly cast" ==> "implicitly casts" > p.3: "to in all" > p.3: "the first add" > p.3: "type-check" ==> "type checking" > p.3: "describing as" > p.3: "We also we omit" ==> "We also omit" p.3: "TypeScript, everything" p.3: "any, all" p.3: "local" typechecking usually means something different in the context of type systems (as in local, or bidirectional, type inference). > the sentence "while, at runtime." is incomplete p.4: "la" ==> "a la" (with accents) > p.4: "these static type information" p.4: "looses" p.4: "isolate" > p.4: "synch" ==> "sync" > p.4: "form" ==> "from" > p.4: "this is concrete, the" p.4: "mode, we do not" > p.5: "This because" ==> "This is because" > p.5: "add much baggage" ==> "add too much baggage" > p.5: "make easy" ==> "makes it easy" > p.5: "binding are" ==> "bindings are" > p.5: "These annotation" ==> "These annotations" p.10: "TruffleSS" ==> "TruffleJS" p.10: "supporting" ==> "supported" > p.11: "validate" ==> "validated" FZ: didn't change the typos not marked by > because I don't believe they are typos. =========================================================================== popl15 Review #213B Updated 22 Aug 2014 12:06:07am EDT --------------------------------------------------------------------------- Paper #213: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: C. Weak paper, though I will not fight strongly against it Confidence: Y. I am knowledgeable in this area, but not an expert ===== Comments for the Authors ===== Summary ======= This paper presents StrongScript, a variant of TypeScript that allows for sound type checking of parts of the code appropriately annotated by the developer. In addition to TypeScript's dynamic type 'any' and optional types, StrongScript allows expressions to be given concrete class types, which are checked soundly. To guarantee soundness, casts are inserted at the boundaries between concrete and non-concrete types. Since only class types can be concrete, these casts can be implemented efficiently using JavaScript's 'instanceof' operator, without any additional tagging. The paper formalizes the type system and states safety and trace preservation theorems. With concrete class types, the language implementation can fixed offsets for field accesses, rather than computing object structure at runtime. The paper presents a prototype implementation of this strategy on the TruffleJS optimizing runtime. This implementation showed some performance improvement on a small set of benchmarks. Evaluation ========== Allowing for greater soundness in gradually-typed languages without sacrificing performance is an important problem, and this paper has some nice ideas in this direction. It is also nice to see that the authors have gone out of their way to maintain compatibility with TypeScript, easing the transition for developers. That said, I have some concerns about the formalism in the paper, particularly handling of higher-order functions. Also, the experimental evaluation is far too limited to determine any potential for performance improvements due to the technique. It seems that many rules and cases for handling function values are missing from the paper. In JavaScript, functions are objects like any other, and the expression grammar in Section 5 has a function as a type of expression that could, e.g., be used as the base expression for a field update. Similarly, function types t_1 ... t_n -> t are included in the type grammar. But, after giving the standard function subtyping rule SFunc, many other cases for functions are missing: > * There is no TGet or TUpdate rule for the case when the base > * expression has a function type. Presumably these cases would be > * handled similarly to TGetAny and TUpdateAny, but those rules don't > * match. > * Similarly, there is no appropriate type system rule for deleting a > * property of a function, nor any rules in the dynamic semantics for > * update, get, or delete operations on functions. FZ: add comment in the impl section. > * Most crucially, the dynamic semantics lacks any rules for casting > * to a function type, though such casts are allowed by the > * expression syntax. FZ: YES, we should not ignore this. Email sent to discuss the issue. > This last case is key since handling casts of function types would > require richer run-time type information than what is built in to > JavaScript, and hence these casts could be costly at runtime. At the > same time, I don't see how one can avoid these casts or introducing > wrappers while also maintaining soundness, since it seems one can > write functions with parameters or return values of concrete types, > e.g., function (x: !Point) { ... }. All in all, treatment of function > values is a major issue that, as far as I can see, is missing from the > paper. Do the authors have a proof of the safety theorem? I don't > see how a proof could be completed without addressing these issues > with functions. FZ: TODO: Agreed. Make clear that functions might get wrapped as in other gradual typing systems, but method invocation on class based objects won't, and there is the gain. > Regarding the the ENew rule in Figure 4, shouldn't the type tag for > the resulting object be !C rather than C? I don't see how the > system could work with a type tag of C here. FZ: yes, fixed. > TypeScript programs often use ambient declarations to use third-party > JavaScript libraries in a more typed manner. How are such > declarations handled in StrongScript? Do concrete types exist for > ambiently-declared classes? I don't immediately see a straightforward > answer. > At the end of page 6, the paper discusses the need for ad-hoc > reduction rules for method invocation, in order to correctly perform > runtime checks of parameter and return types. The issue is mentioned > again at the introduction of evaluation contexts. I do not understand > the issue here; an example is sorely needed. > On page 10, the intrinsics are described as being no-ops on > non-supporting engines, but I believe they need to be "return this". > Also, couldn't these additional calls actually decrease performance on > non-supporting engines if they don't get inlined by the JIT? Regarding the experiments, five hand-picked benchmarks is not nearly enough to make any conclusions regarding performance improvement. The so-called conventional wisdom amongst VM designers mentioned by the authors is worth serious consideration: part of the motivation for creating the Dart language from scratch was to improve performance compared to JavaScript, and yet the language designers (VM performance experts) still allowed types to be fully optional. Given the limited nature of benchmarking performed, and the conventional wisdom, it seems more likely than not that the observed performance improvements will not hold up across more benchmarks and runtimes. While the paper is well-written and understandable overall (the background section on gradually-typed languages is particularly nice), it contains numerous grammatical errors (a few of which are listed below) and requires careful proofreading and copy-editing. Minor comments ============== > * p.1, col. 2, bullet 1: "easy typeable StrongScript" => "easily typeable in StrongScript" > * p.1, col. 2, bullet 5: limitation -> limitations > * Sec. 2, 1st para: "Decades research" -> "Decades of resesarch" > * Sec. 2, col. 2, code example: call to 'f' should be call to 'id' > * Sec. 3, 1st sentence: semicolon before "we recall it here." In general, many commas need to be replaced with colons or semicolons. > * Sec. 3, 2nd para: StrongScript Starting -> StrongScript, starting > * p.3, 2nd column, near top: "In none of the cases above the ..." -> "The TypeScript compiler does not emit a warning in any of the cases above" > * p.4, 2nd column, 2nd code example: should object literal have field y=3 instead of val=3? > * Section 4.4, last sentence: Please add a citation to the referenced Thiemann work. =========================================================================== popl15 Review #213C Updated 4 Sep 2014 3:52:07pm EDT --------------------------------------------------------------------------- Paper #213: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: B. OK paper, but I will not champion it Confidence: Y. I am knowledgeable in this area, but not an expert ===== Comments for the Authors ===== This paper presents StrongScript, an extension to JavaScript that parallels TypeScript, but has a type system with actual static guarantees, unlike TypeScript's. On one hand, I like this goal and I find the unsound nature of TypeScript unappealing, but on the other hand, I do not think that I represent the average JavaScript programmer particularly well. As such, my main concern with this paper is the lack of an evaluation of how well one would expect such JavaScript programmers to react to this language. Put in overly strong words, if there is no interest in StrongScript from the JS community, then what value is there in this paper? The paper itself doesn't offer up a particularly compelling answer to this question, as the design is very heavily influenced by details of JS itself. I have three more minor complaints: - The proofs for the theorems do not seem to be present (or pointed to some other tech report somewhere). Have they been done? - JS has a very strange notion of variables, allowing them to be manipulated in a dynamic way that doesn't seem to be captured by the semantics in the paper. Does this cause problems for StrongScript? - I believe that the TypeScript design has a (strange to me but apparently important to the TypeScript community) design constraint that the output of the TypeScript compiler be something that ordinary JavaScript developers can read (and that various tools like debuggers work well with). There is some mention of this in the paper in the beginning of 6.2 where it says that the output of the StrongScript compiler is idiomatic JS code, but the paper doesn't explicitly discuss this design constraint (either to explain how StrongScript doesn't follow it and why that's okay, or to say that it does). Typos. Section 3, pg 3, "Extends declaration amongst interface" is grammatically incorrect. > Opposite column: "In none of the cases above the TypeScript compiler > emit a warning." is also gramatically incorrect. Page 4: "checking la Java" should be "checking a la Java". In 6.2, something seems to have gone wrong leading to a period at the beginning of a line (following "TruffleSS"). > On page 11, near the bottom of the right column "Of course, this > should be validate on other engines." is missing a "d" at the end of > "validate". =========================================================================== popl15 Review #213D Updated 5 Sep 2014 11:15:35am EDT --------------------------------------------------------------------------- Paper #213: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: C. Weak paper, though I will not fight strongly against it Confidence: Z. I am not an expert; my evaluation is that of an informed outsider ===== Comments for the Authors ===== TypeScript is an "optional" type system for JavaScript. Type annotations are used to flag errors statically, but the type system is unsound as casts are not checked at runtime (this is by design). This paper extends TypeScript to StrongScript by adding "concrete" types, which are actually enforced by runtime checking. Formalization of the dynamic and static semantics of StrongScript is based on an object-oriented language without references. The paper proves that a typed program can get stuck only due to a runtime cast or due to method access on an optionally or untyped field. Additionally, optional types preserve the runtime behavior of unannotated programs (because casts to optional types are ignored at runtime) and the paper claims to show that optional type checking is as strong as concrete type checking, when used extensively. Evaluation: StrongScript builds in the direction of gradual typechecking. The key difference is that it also supports TypeScript's optional types, which are sound to the extent that programmer-inserted casts are sound. Consequently, it embodies a very flexible type system. Nonetheless, I find it hard to be excited by the work. This is largely because I don't see any significant insight in the paper, technical or conceptual. Once the primary goal is set, the rest of the paper looks routine. Moreover, I don't understand some of the technical details. Technical points: - I don't understand the difference between method access and field access in the dynamic semantics, which seems to make the bulk of Section 5 and also requires an exception to standard evaluation context semantics. Indeed, in your dynamic semantics, the rules EGETANY and EGETOPT (for field access at any and optional types) are special cases of the rule EMETHAPPCHECK (for method access). The same is not true of rules EGET and EMETHAPPNOCHECK for field and method access at concrete types. The latter is due a subtyping premise in the rule EMETHAPPNOCHECK, but I don't understand why this premise is needed. It seems that your typing rules TGET and TOBJ should make the premise redundant. - Why can't methods take functions as arguments? Is it just to avoid higher-order contracts in the implementation? > - In Theorem 1, the condition \Gamma |- e'': t looks wrong. e'' > appears in an evaluation context but t is the type of the whole > expression (with the evaluation context). Is a proof of the theorem > available? FZ: It should have been Gamma |- e'': t'' (with t'' - In the example program on page 2, what is the function f()? - At the beginning of Section 3, you say that TypeScript erases types at runtime and does not catch errors at runtime. This looks wrong. TypeScript compiles to JavaScript, which does handle runtime errors and carries types at runtime. - Foonote 4 is placed too late in the paper. It should show up when the annotation "public" is used for the first time on page 3.