Guarded Impredicativity

on YouTube ↗40m

" summary

Proposes guarded impredicativity: allow impredicative instantiation only when the forall appears inside a type constructor. Gives a precise algorithm (constraint generation + delayed instantiation, then elimination) and proves preservation of principal types, so inference remains decidable. Implements a prototype for GHC, runs across Hackage and requires only a handful of small edits (around fifteen packages) to compile, showing the feature is practical and interoperates with GHC extensions.

AI-written summary · about

" chapters (5)

1. 0:00Start
2. 2:15Instantiation
3. 9:22Workarounds
4. 28:09Principle Type
5. 36:51Summary

" related talks

• 45mDepending on TypesStephanie Weirich · Code Mesh 2015
• 31mParametricity The Essence of Information HidingKris Nuttycombe · LambdaConf 2015
• 33mStatically Typed InterpretersChristopher Hockenbrocht · LambdaConf 2017
• 39mDependent Types in HaskellStephanie Weirich · Strange Loop 2017
• 15mScalable Type Inference for Intrinsically-Typed BindersClément Pit-Claudel, Max Kurze, Sebastian Ertel · RocqPL 2026
• 50mOverlapping and Undecidable and Incoherent, Oh My!Jake Keuhlen · LambdaConf 2019
• 50mImplicits Inspected and ExplainedTim Soethout · Scala Days Berlin 2016
• 22mIs Space-Efficient Polymorphic Gradual Typing Possible?Taro Sekiyama, Atsushi Igarashi, Shota Ozaki · Scheme 2021