'Typing the Untyped: Soundness in Gradual Type Systems' by Ben Weissmann

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.

[jaredsmith]

That is by far the most accessible explanation of type variance I've ever seen. Nice!

[benjamingruenbaum]

A year later - TypeScript has `as const` and `const foo = [1, 2, 3] as const;` will error on `foo[10].toFixed(2);`

[yifumao]

Nice talk, esp. the part about variance.

[saltrocklamp]

I would love to see an updated version of this talk that includes at least some mention of Julia.