Subsumption and impredicative types with Richard Eisenberg


November 10th, 2020

43 mins 8 secs

Your Host
Special Guest

About this Episode

Subsumption, the process of figuring out whether one type is the subtype of another, is fundamental to GHC's type checker and was recently changed. In this episode, Richard Eisenberg explains what subtypes are, how subsumption works, and why some previously accepted programs will soon start to be rejected by GHC. He then talks about how these changes help with inferring impredicative types, an advanced form of polymorphism that basically allows you to put forall statements anywhere in a type signature such as inside of a list.

Music by Kris Jenkins.

Episode Links