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
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.
The promise and peril of adoption
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
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.
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.
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.