Position Paper : Performance Evaluation for Gradual Typing

Gradually typed programming languages aim to improve software maintenance by allowing programmers to selectively add type annotations to untyped programs. Run-time checks ensure that these typed portions interact soundly with unannotated parts of the program. These checks, however, may introduce unacceptable performance overhead. The extent of the overhead has not been systematically studied and no common methodology exists to diagnose such problems. In this position paper, we propose an idea for a framework for evaluating the performance of a gradual type system. 1. The Gradual Typing Promise Gradually typed programming languages promise to improve software maintenance for untyped scripting languages. Using such systems, programmers may selectively add type annotations to their existing untyped programs. The annotated parts are checked, and run-time contracts or casts ensure that they safely interact with the remaining untyped portions. Programmers use gradual type systems in order to realize software engineering benefits from types such as enforcing documentation, guiding refactoring, and catching regressions. In addition, the gradual typing promise implies that as programmers add type annotations, their program will continue to run. This part of the promise is held up by allowing typed and untyped code to link together with inserted run-time checks. For a gradual type system to be a net benefit, it should also allow gradually typed programs to remain performant as they are incrementally converted. Therefore, it is desirable for a gradual type system to promise low overhead for interoperation. In our experience, existing gradual type systems (including the systems we maintain) fail to meet this criterion. Gradual type systems in the literature report slowdowns of 72x (Rastogi et al. 2015), 10x (Vitousek et al. 2014), and 4x (Takikawa et al. 2015) in programs due to the insertion of dynamic checks. Practical users of gradual type systems have also reported 25-50x slowdowns. To make gradual type systems live up to their promises, we must (1) diagnose what kinds of programs and what degree of “typedness” leads to performance problems, and (2) identify the tools, language features, or implementation techniques that will help eliminate the overhead. This position paper focuses on the diagnostic side, and outlines some potential solutions. 2. The State of Gradual Type System Evaluation Despite a wealth of literature on gradual typing, there is a dire lack of performance evaluation efforts. As mentioned, several projects have reported slowdowns on example programs, and others have explored the cost of the checking mechanism itself (Allende et al. 1 http://docs.racket-lang.org/math/array.html 3.22±0.09 3.02±0.05 3.79±0.12 3.08±0.13 4.33±0.03 1.9±0.03 3.8±0.08 3.18±0.06 4.12±0.06 1.87±0.14 3.75±0.11 2.82±0.11 2.19±0.04 4.18±0.09 1.85±0.06 2.9±0.02 3.66±0.07 2.76±0.05 2.16±0.05 4.22±0.05 1.83±0.06 2.85±0.03 2.78±0.11 2.15±0.05 1.06±0.01 2.87±0.02 2.69±0.12 2.07±0.03 1.05±0.03 2.82±0.03 1.06±0.01