))
Subsumption and impredicative types with Richard Eisenberg
Archived series ("Inactive feed" status)
When?
This feed was archived on March 27, 2023 17:04 (
Why? Inactive feed status. Our servers were unable to retrieve a valid podcast feed for a sustained period.
What now? You might be able to find a more up-to-date version using the search function. This series will no longer be checked for updates. If you believe this to be in error, please check if the publisher's feed link below is valid and contact support to request the feed be restored or if you have any other concerns about this.
Manage episode 277078342 series 2809070
Content provided by Tweag I/O. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Tweag I/O or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://player.fm/legal.
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.
16 episodes
Share
