Every great idea in computing will be discovered twice, once by a logician and once by an computer scientist. In 1974, John Reynolds introduced a tiny programming language – the polymorphic lambda calculus – to model data abstraction; nine years later he introduced a theory to explain how to change the representation of an abstract type without changing the behaviour of the program. But before all that, in 1972, Jean-Yves Girard introduced exactly the same tiny programming language – now called System F – for a completely different reason having to do with second-order logic. Related ideas were introduced by the logician Roger Hindley and later by the computer scientist Robin Milner, and now serve as the basis of the type system for Haskell, OCaml, and F#.

Reynolds’s theory can be viewed as a magic trick: give me the type of a function and I will tell you a theorem that it satisfies, even though I know nothing about the function's definition other than its type. The GHC Haskell compiler routinely exploits this fact to optimize operations on lists. It’s even possible to write the function in a dynamically typed language, such as JavaScript, and then impose the type later in a way that ensures it will still satisfy the corresponding theorem. We have a research version of TypeScript, called TypeScript The Next Generation, which does just that. This talk will explain the magic.