Swarat Chaudhuri recently asked on Twitter what recent PL innovations have already made an impact in practice. I’ve been lucky enough to be part of a signal example of this: the rise of gradual typing. From its beginning 15 years ago, gradual typing is now part of everyday development practice for massive code bases at companies from Facebook to Microsoft to Stripe to Dropbox, all of which have developed their own gradual type systems. In this post, we cover the goals of gradual typing, why it’s had such an impact already, and what remains to be accomplished.
Typed vs untyped languages
Since the initial invention of programming languages in the late 1950s, language designers have divided on the question of how much information should be statically evident about the behavior of the program. In FORTRAN, what sorts of data was computed by particular expressions was evident from the syntax of the program, whereas in LISP this was not the case. While this distinction dates from the beginning of computing, the rise of so-called scripting languages such as JavaScript, Perl, PHP, Python, and Ruby in the late 1990s, especially for the development of network and web services, made the differences seem much more salient. Programmers trained in these new languages found their unstructured flexibility valuable, while programmers used to languages such a Java and C++, not to mention Haskell or ML, found the lack of static guarantees, optimizations, and tool support limiting. Thus was born a desire for synthesizing these two traditions into something new.
The birth of gradual typing
One spark for the emergence of gradual typing was the development of higher-order contracts by Robby Findler, which showed how to protect interesting invariants between components. Building on this and other work, four different papers, led by me, Jeremy Siek, Jacob Matthews, and Jessica Gronski respectively, synthesized these ideas and applied them to the problem of protecting the boundary between less-typed and more-typed parts of a program, creating the field of gradual typing.
These initial proposals took diverging approaches to how the static type system would integrate with untyped code, to the granularity of interaction, and to what guarantees were offered to programmers. But all of them agreed on one key idea: that interaction should preserve the guarantees from the types, and thus type soundness should be maintained for typed parts of programs.
Subsequent to this, there has been a flowering of academic work on gradual typing. Researchers investigated new type system features such as parametric polymorphism, new runtime representations that maintain tail calls, and new type system features to accommodate existing programs in languages ranging for Clojure to JavaScript.
The promise and peril of adoption
Since the initial development of gradual typing, major companies have adopted the ideas to improve the experience of developing in existing untyped languages. Most prominently, Facebook developed Hack, a type system for PHP, and Flow, a type system for JavaScript, and Microsoft developed TypeScript, also a type system for JavaScript. Similarly, Google developed the Closure Compiler for JavaScript, Dropbox has helped develop MyPy for Python, and recently Stripe released Sorbet for Ruby.
All of these are open-source tools that integrate statically typed code with existing programs, and all have been adopted substantially both inside and outside the companies that developed them. TypeScript is by far the most prominent of these and is now the 7th most popular language on GitHub, ahead of C.
However, all of these systems were developed with a distinct set of goals from the original work on gradual typing, leading to significantly different design choices. For almost all of these systems, the number one goal was increasing developer productivity via tooling such as autocomplete and refactoring support, tools that are easier to build given type information. Providing static guarantees or supporting type-driven optimization were not priorities. As a result, all of these systems abandoned the original goal of sound interoperation, instead choosing to simply ignore types at runtime.
This left the field of gradual typing in the odd state of seeing wide adoption, but with the central original concern being cast aside.
The problem of performance
Of course, a focus on sound interoperation has its downsides as well. Most notably, the dynamic checks required to enforce soundness have an inherent runtime cost. Additionally, when higher-order values such as functions, objects, or arrays flow between typed and untyped code, enforcing soundness requires not just checking but also adding wrappers that mediate between the two sides. These indirections, combined with dynamic checks, can have a substantial performance cost.
The first systematic effort to measure this cost was undertaken by Asumu Takikawa, Ben Greenman, and their colleagues at Northeastern, and their methodology has been widely adopted in just a few years. Their initial results revealed substantial performance problems for Typed Racket, but the combination of a method and a baseline has spurred numerous subsequent efforts which show that performance can be significantly improved using JIT compilers, nominal types, representation improvements, and custom-built compilers, among others.
Additionally, Michael Vitousek and colleagues noticed that a different and weaker enforcement strategy adopted for other reasons also had performance benefits, although it gives up on some fundamental parts of the soundness guarantee. When combined with sophisticated JIT compilers, this may already be able to eliminate problematic performance overhead.
Finally, the recent Sorbet system for Ruby from Stripe does enforce some aspects of the type system at runtime, demonstrating that the benefits of sound reasoning continue to be persuasive in industrial contexts.
Paving the typed cowpaths
Beyond the challenge of sound interoperation between typed and untyped code, one area of focus for gradual typing has been designing type systems that work well with how people program in languages like Racket, JavaScript, or Python. Although programmers in untyped languages have a discipline in mind when constructing programs, it’s not the same discipline as found in the Java or Haskell type systems. Instead, designers of gradual type systems have analyzed the idioms already used in existing programs so that type systems can accommodate real-world programming styles.
Because of this, new type system features have been developed, ranging from refinement of types based on conditional tests, to row polymorphism for class types, to complex hash table typing, to a resurgence of interest in set-theoretic type connectives such as union and intersection. The paths laid out by programmers, when paved into type system features, are a fruitful source of type system ideas. Remarkably, all of these features have seen use in industrial as well as academic systems — TypeScript has adopted almost all of these features and more.
Future re-unification?
Even though gradual typing is now a substantial part of the programming language landscape, much remains to be done. Most importantly, I hope that the two strands of effort, in academia and industry, can find a way to re-unify, gaining the benefits of soundness without sacrificing simplicity, predictability, and performance. We’ve already seen movement on multiple fronts, as TypeScript makes their type system more sound, Sorbet brings dynamic enforcement to an industrial gradual type system, and numerous academic projects investigate how to accelerate sound gradual typing.
Beyond the split over soundness, many questions remain to be answered. Can gradual typing provide a way to measure the impact of type systems? How well can gradual type systems support type-driven optimization? Can these techniques scale in practice to more sophisticated properties, such as the affine types of Rust? And what is the relationship of gradual types to logic, through the lens of the Curry-Howard correspondence?
Regardless of the answers to those questions, it seems clear that gradual typing is here to stay, and that the traditional split between typed and untyped languages is no longer so wide.
Bio: Sam Tobin-Hochstadt is an Associate Professor at Indiana University in the Center for Programming Systems. He studies gradual typing, language design, compiler optimization, and metaprogramming. He is a core developer of the Racket project and a member of TC39, the standards group for JavaScript.
Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.
