=========================================================================== ECOOP 2015 Review #30A Updated 10 Feb 2015 8:27:14pm EST --------------------------------------------------------------------------- Paper #30: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: 3. Weak accept Reviewer expertise: 2. Some familiarity ===== Paper summary ===== This paper presents StrongScript, which is an extended type system for TypeScript, an extension of JavaScript with optional types. TypeScript's type system is unsound by design and its optional types will be discarded when TypeScript's compiler emits JavaScript code. StrongScript improves TypeScript by adding concrete types into the system and enabling sound type checking on concrete types. This results into a gradual type system that treats concrete types as static types which provide strong safety guarantee. Concrete types also enable statically determinable object layouts, leading to aggressive compiler optimizations. The paper formally presents the type rules and important properties of the system. Finally, an evaluation shows that the addition of type information leads to speedups. ===== Comments for author ===== This is a well-written paper: the idea is clearly presented with examples given at various points to ease understanding; the type rules are also well formalized. However, I have several major problems listed as follows. (1) The paper is on the lower end in novelty, especially in the context of a large body of related work on gradual types as well as extensions of JavaScript. TypeScript already has optional types, and the only contribution of this paper is the addition of concrete types and nominal subtyping. (2) The evaluation focuses only on the performance aspect. How easy/difficult is it to add annotations to convert a TypeScript program to a StrongScript program? For some benchmarks, there is a large number of annotations added (e.g., 186 for oct-deltablue), which indicates non-trivial programming efforts. (3) The performance evaluation leaves a lot to be desired. The optimizations rely on a modified JavaScript runtime. How exactly did you modify the runtime to exploit the type information? The performance improvements are not very clear in many cases. Are they real improvements or execution noises? The authors did not measure deviations among running times, which makes the reported speedups less convincing. =========================================================================== ECOOP 2015 Review #30B Updated 29 Jan 2015 4:35:28am EST --------------------------------------------------------------------------- Paper #30: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: 4. Accept Reviewer expertise: 4. Expert ===== Paper summary ===== This paper addresses the issue of adding concrete types to TypeScript. Currently, TypeScript types are considered to be structured, statically checkable documentation, rather than providing any run-time guarantees. In this paper, TypeScript is extended with a new type constructor !C inhabited at run-time by objects with class D, where D is a subtype of C. Such concrete types are more like Java types, in that they constrain the run-time inhabitants. The paper presents a type system in which objects can be given one of three types: any (for dynamically typed variables), C (documenting the unenforced intent that the object should be an instance of C) or !C (enforcing that the object must be an instance of C). The subtyping relation is then defined, such that any is unrelated to C and !C, and !C <: C. A type system and operational semantics is provided, and the usual type safety results are claimed. Experimental evidence is provided for the ability of concrete types to be optimized, by providing unchecked offset-based field access to objects of concrete type. This optimization results in 2-32% performance improvement on the chosen benchmarks. ===== Comments for author ===== Points in favor: * The paper is tackling an interesting problem, that of applying techniques from gradual typing / contracts to a real-world language. The results are solid, and explore an interesting part of the design space for gradual type systems. Points against: * The paper appears to have been submitted in something of a hurry, and there are numerous typographic errors which should really have been caught before submission. More seriously, the type safety theorems are presented without proof, or even much of a discussion of how the proofs were performed. Are they mechanized in a proof assistant, or typed up anywhere? I'm not expecting a conference paper to provide full proofs, but a sentence explaining how the reader can access the proofs, and whether they were mechanized or pen-and-paper would be useful. * The type system seems ad hoc in places. For example, field update is only allowed on non-function types, and it would be helpful to know why. The obvious reason would be method overriding, but this is banned (again, without comment) by [TClass]. Is this to allow static method dispatch on concretely typed objects? Detailed comments: Some discussion of why any is not the top type would be useful, and of the reason for distinguishing any and Object. In the experimental work, can you optimize numeric variables, to allow the unboxed representation to be used? I'm guessing not, at least not without some additional flow analysis to find variables of type !number which are never cast to object type. Subtyping is not reflexive or transitive, for example there is no derivation for !C <: Object. I think this is just a mistake, and that reflexivity should be added, and [SOptInj] should be "if C <: D then !C <: D" and ditto [SClass]. [TObj] surely has some preconditions. I'd expect something like "If Gamma |- O[s]:C[s] for each s in fields(C) then Gamma |- { O | !C} : !C" and "Gamma |- { O | any } : any". If subtyping is made transitive, and there is a top type, then [TCast] can be simplified to "if Gamma |- e:top then Gamma |- e:t". This rule has the advantage of not suffering the "stupid casts" problem from Featherweight Java. [TDelete] only allows delete on any, which seems quite restrictive. The operational semantics adds some extra dynamic checks above those provided by JS, for example delete{O | !C}[s] fails if s is a field of C. Did you include the penalty of these extra checks in your experimental results? Grammar, typos: (there were more than reported here): p.3: “exploratoty” "their productivity..." is orphaned. p.4: "Strongtalk like..." "semantiucs cast" -> "semantic cast" p.5: "that unneccessarily strong" "typed to untyped" -> "untyped to typed" =========================================================================== ECOOP 2015 Review #30C Updated 31 Jan 2015 3:45:15am EST --------------------------------------------------------------------------- Paper #30: Concrete Types for TypeScript --------------------------------------------------------------------------- Overall merit: 3. Weak accept Reviewer expertise: 4. Expert ===== Paper summary ===== In this paper, the authors propose an alternate design for TypeScript, a version of JavaScript with optional typing, called StrongScript. In addition to the optional types of TypeScript, StrongScript also contains concrete types which, unlike optional types, do not allow for interactions with arbitrary values that do not conform to the expectations of their type annotations. Thus, these concrete types provide the programmer with strong guarantees about how concretely typed values are used, and those strong guarantees can be utilized by the compiler for optimizations and the like. The authors also propose a formal property called trace preservation, where untyped versions of programs and versions of the same program annotated with optional types evaluate to the same value. They detail how stricter type systems like those found in gradual typing systems cannot satisfy a similar property, since values expecting certain types cannot interact with non-conforming dynamic values, and thus a dynamic error signalling the type error will occur that did not happen in the original, untyped program. While concrete types cannot directly be trace preserving (since they will produce errors via non-conforming dynamic values), the authors also claim that a strengthening property similar to trace preservation holds between fully optionally-typed versions of a program and the same program where all types are converted to concrete types. ===== Comments for author ===== Overall, the system described seems to add a sorely-needed layer to TypeScript (or similar optionally-typed systems) that provides types that are not merely annotations that are not checked on the typed-untyped boundary, but that provide guarantees for program behavior that can be used to for program understanding, to drive optimizations, etc. where there is a need to know that misuses of the typed values by untyped code will be caught and rejected. The interplay between untyped, optionally typed, and concretely typed code provides a nice path from untyped to typed programming. However, I did see a couple of major issues that I'd like to see addressed. For example, in your model, ECastFun _does_ introduce a wrapper, and I expect that your implementation would also need to introduce wrappers for untyped functions being used at concrete types. This isn't a surprise, since the stricter checking of higher-order types requires delaying those checks, but the previous sections read as if you won't end up needing them at all. In fact, on p.7, you mention that concrete types "do not support the notion of wrapped values", which just seems to contradict this. Similarly, you mention earlier in the paper that your interface types are structural, so it seems, like function types, you would need some sort of wrapping, i.e., annotating a class with a concrete interface type requires wrapping parts of the class to ensure that, say, the types of methods are adhered to. However, interfaces don't appear in the model, and I don't see this discussed in your implementation section. Are interfaces not allowed to appear within concrete types? If they are, then you may get into issues with allowing width subtyping with them and the fact that methods/fields not mentioned in a type are not prevented from being added or deleted (p. 11). See Takikawa et al., OOPSLA 2012, for more. Is it the case that a mixture of concrete interface and function types to form features like mixins might run into similar problems as described in that paper? If not, why not? Typos: - p.3: exploratoty -> exploratory - p.5: "when developers put contracts that" [are] "unnecessarily strong"