Strange Loop

Typing the Untyped: Soundness in Gradual Type Systems

Recent years have seen an explosion of gradual type systems and superset languages that add types to previously untyped languages: TypeScript & Flow for Javascript, MyPy and Pyre for Python, Hack and PHP7 for PHP, Sorbet for Ruby, and many more. Implementing these type systems involves making tradeoffs between soundness (catching as many errors as possible) and completeness (not rejecting valid programs) that fundamentally impact the usability and usefulness of the type system.

In this talk, I'll examine a few of these tradeoffs that apply across many languages: type refinement and refinement invalidation, array out-of-bound errors, and variance (particularly array covariance). We'll look at what tradeoffs a gradual type system needs to make, what the advantages are to different approaches, and compare how various gradual type systems and more traditional static type systems handle these tradeoffs.

Ben Weissmann

Tulip

Ben "Fuzzy" Weissmann is a software engineer at Tulip, where he was the first employee and leads architecture on the Platform team, creating a platform for manufacturers to build apps that streamline their operations. His focus is on architecture, backend systems, and developer tooling. In the past, he's worked at Twitter, TripAdvisor, and the MIT Media Lab.