Reference. How to evaluate the performance of gradual type systems

A sound gradual type system ensures that untyped components of a program can never break the guarantees of statically typed components. This assurance relies on runtime checks, which in turn impose performance overhead in proportion to the frequency and nature of interaction between typed and untyped components. The literature on gradual typing lacks rigorous descriptions of methods for measuring the performance of gradual type systems. This gap has consequences for the implementors of gradual type systems and developers who use such systems. Without systematic evaluation of mixed-typed programs, implementors cannot precisely determine how improvements to a gradual type system affect performance. Developers cannot predict whether adding types to part of a program will significantly degrade (or improve) its performance. This paper presents the first method for evaluating the performance of sound gradual type systems. The method quantifies both the absolute performance of a gradual type system and the relative performance of two implementations of the same gradual type system. To validate the method, the paper reports on its application to 20 programs and 3 implementations of Typed Racket.

Cite

Cite as @greenman_etal_2019 (helia, typst) · \cite{greenman_etal_2019} (LaTeX)
BibTeX
bibtex · 11 lines
@article{greenman_etal_2019,
 title = {How to evaluate the performance of gradual type systems},
 author = {Greenman, Ben and Takikawa, Asumu and New, Max S. and Feltey, Daniel and Findler, Robert Bruce and Vitek, Jan and Felleisen, Matthias},
 year = {2019},
 url = {http://janvitek.org/pubs/jfp18.pdf},
 journal = {Journal of Functional Programming},
 volume = {29},
 publisher = {Cambridge University Press},
 doi = {10.1017/S0956796818000217},
 pages = {e4}
}
hayagriva YAML (typst)
yaml · 21 lines
greenman_etal_2019:
  type: article
  title: How to evaluate the performance of gradual type systems
  author:
  - Greenman, Ben
  - Takikawa, Asumu
  - New, Max S.
  - Feltey, Daniel
  - Findler, Robert Bruce
  - Vitek, Jan
  - Felleisen, Matthias
  date: 2019
  page-range: e4
  url: http://janvitek.org/pubs/jfp18.pdf
  serial-number:
    doi: 10.1017/S0956796818000217
  parent:
    type: periodical
    title: Journal of Functional Programming
    publisher: Cambridge University Press
    volume: 29
Cited by (1)

A Semantic Foundation for Sound Gradual Typing new_dissertation_2020

Gradually typed programming languages provide a way forward in the debate between static and dynamic typing. In a gradual language, statically typed and dynamically typed programs can intermingle, and dynamically typed scripts can be gradually migrated to a statically typed style. In a sound gradually typed language, static type information is just as reliable as in a static language, establishing correctness of type-based refactoring and optimization. To ensure this in the presence of dynamic typing, runtime type casts are inserted automatically at the boundary between static and dynamic code. However the design of these languages is somewhat ad hoc, with little guidance on how to ensure that static reasoning principles are valid. In my dissertation, I present a semantic framework for design and metatheoretic analysis of gradually typed languages based on the theory of embedding-projection pairs. I show that this semantics enables proofs of the fundamental soundness theorems of gradual typing, and that it is robust, applying it to different evaluation orders and programming features.
Web
Cites 56 works (1 here)
With notes (1)

Is Sound Gradual Typing Dead? takikawa_etal_2016

Programmers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, researchers have explored the idea of gradually-typed programming languages which allow the incremental addition of type annotations to software written in one of these untyped languages. Some of these new, hybrid languages insert run-time checks at the boundary between typed and untyped code to establish type soundness for the overall system. With sound gradual typing, programmers can rely on the language implementation to provide meaningful error messages when type invariants are violated. While most research on sound gradual typing remains theoretical, the few emerging implementations suffer from performance overheads due to these checks. None of the publications on this topic comes with a comprehensive performance evaluation. Worse, a few report disastrous numbers. In response, this paper proposes a method for evaluating the performance of gradually-typed programming languages. The method hinges on exploring the space of partial conversions from untyped to typed. For each benchmark, the performance of the different versions is reported in a synthetic metric that associates runtime overhead to conversion effort. The paper reports on the results of applying the method to Typed Racket, a mature implementation of sound gradual typing, using a suite of real-world programs of various sizes and complexities. Based on these results the paper concludes that, given the current state of implementation technologies, sound gradual typing faces significant challenges. Conversely, it raises the question of how implementations could reduce the overheads associated with soundness and how tools could be used to steer programmers clear from pathological cases.
PDF · Web · pldb
External (55)
  • On the cost of type-tag soundness (2018)
  • The Spectrum of Soundness and Performance (2018)
  • Sound Gradual Typing: Only Mostly Dead (2017)
  • Migratory Typing: Ten years later (2017)
  • Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems (2017)
  • Bindings as Sets of Scopes (2016)
  • Abstracting Gradual Typing (2016)
  • Space-Efficient Latent Contracts (2016)
  • Just-in-time Static Type Checking for Dynamic Languages (2016)
  • Feature-Specific Profiling (2015)
  • Pycket: A Tracing JIT For a Functional Language (2015)
  • Principal Type Schemes for Gradual Programs (2015)
  • Space-Efficient Manifest Contracts (2015)
  • Safe & Efficient Gradual Typing for TypeScript (2015)
  • Concrete Types for TypeScript (2015)
  • Blame and Coercion: Together again for the first time (2015)
  • Monotonic References for Efficient Gradual Typing (2015)
  • Towards Practical Gradual Typing (2015)
  • Design and evaluation of gradual typing for python (2014)
  • Gradual typing for Smalltalk (2014)
  • Tough Behavior in Repeated Bargaining Game, A Computer Simulation Study (2014)
  • Stabilizer: Statistically Sound Performance Evaluation (2013)
  • Calculating Threesomes, with Blame (2013)
  • Constraining Delimited Control with Contracts (2013)
  • Complete Monitors for Behavioral Contracts (2012)
  • Chaperones and Impersonators: Run-time Support for Reasonable Interposition (2012)
  • Gradual Typing for First-Class Classes (2012)
  • Space-efficient gradual typing (2010)
  • Threesomes, with and without blame (2010)
  • Operational semantics for multi-language programs (2009)
  • Thorn: Robust, Concurrent, Extensible Scripting on the JVM (2009)
  • Static Type Inference for Ruby (2009)
  • Producing Wrong Data Without Doing Anything Obviously Wrong (2009)
  • Practical Variable-Arity Polymorphism (2009)
  • Gradual Typing with Unification-based Inference (2008)
  • The Design and Implementation of Typed Scheme (2008)
  • Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic (Extended Report) (2007)
  • Ratios: A short guide to confidence limits and proper use (2007)
  • Pluto: or how to make Perl juggle with billions (2006)
  • Gradual Typing for Functional Languages (2006)
  • Interlanguage Migration: from Scripts to Programs (2006)
  • Code layout as a source of noise in JVM performance (2005)
  • Toward Type Inference for JavaScript (2005)
  • Catching bugs in the web of program invariants (1996)
  • Effective flow analysis for avoiding run-time checks (1995)
  • Bigloo: A Portable and Optimizing Compiler for Strict Functional Languages (1995)
  • Safe Polymorphic Type Inference for a Dynamically Typed Language: Translating Scheme to ML (1995)
  • Soft Typing with Conditional Types (1994)
  • Global Tagging Optimization by Type Inference (1992)
  • Common Lisp the Language (1990)
  • New Insights into Partial Evaluation: the SCHISM Experiment (1988)
  • Inferring Types in Smalltalk (1981)
  • MACLISP Reference Manual (1974)
  • Some Problems in Interval Estimation (1954)
  • Outline of a theory of statistical estimation based on the classical theory of probability (1937)
greenman_etal_2019 reference entries/refs/greenman_etal_2019/greenman_etal_2019.hel