Subsumption and impredicative types with Richard Eisenberg

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.Special Guest: Richard Eisenberg.Links:The Wikipedia article on subtyping and subsumption — "[...] a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype [...] In type theory the concept of subsumption is used to define or evaluate whether a type S is a subtype of type T. "Explanation of Levity Polymorphism on StackOverflow — This concept is briefly touched in the episode.The GHC proposal arguing for stricter subsumption judgement. — This proposal initiated a large part of the work that Richard is talking about. The changes that it brought about will be included in GHC 9.0.A short explanation of Impredicative Types on the Haskell Wiki — "Impredicative types take this idea to its natural conclusion: universal quantifiers are allowed anywhere in a type, even inside normal datatypes like lists or Maybe. [...] However, impredicative types do not mix very well with Haskell's type inference [...]"The Quick Look Impredicativity GHC proposal. — The goal of this proposal was to significantly enhance the current state of impredicative types in Haskell. It has been accepted, implemented and will also be available in GHC 9.0.