Speaker

Richard Eisenberg

Abstract

Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. Yet support for existential types in many languages is tied to datatypes, requiring users to manually annotate the introduction and elimination of existentials. This talk presents recent work on type inference for existential types, eliminating the need for manual manipulation of existential types in expressions by using a bidirectional type inference algorithm.

We will then examine a case study of programming with linear types, showing that doing so is sometimes awkward, even though the linear types provide extra guarantees around resource usage. We can make working with linear types much more ergonomic through the use of linear *constraints*. Combining linear constraints with first-class, annotation-free existentials leads to more fluid programming without sacrificing running time or compile-time guarantees.

The talk is based on Haskell, but the inference work on existentials is widely applicable; the work on linearity may be more specific to Haskell's particular take on its implementation of linear types.

Bio

Richard is a Principal Researcher at Tweag. His research centers around how we can use static type systems to power high-assurance programming and avoid programmer mistakes, all without sacrificing ease-of-use or runtime efficiency. His language of focus is the pure functional language Haskell. Richard is a core contributor to Haskell's primary compiler, GHC, and he serves as the chair of the board of the Haskell Foundation. He lives in suburban Philadelphia with his wife and daughter.

Passcode: 583807; Video-off please during talk.

[Could not make it? Click on image below ↓  for recording]