Quotient Polymorphism
summary
Adds choice polymorphism for quotiented types to stop repeating equivalent functions and to accept valid-but-rejected code, implemented in Quotient Haskell on top of Liquid Haskell. Uses quotient inductive types (bags, multisets, sets) with implicit coercions between layers, pushes respectfulness checks to instantiation and solver discharge (SMT/Z3), infers quotient variables and uses anti-unification for their types, and lets examples like map, filter, and count/isMember typecheck where before they failed. Implementation and examples are on the project GitHub.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:01Subtyping vs quotient types
- 3:28Quotient inductive types
- 7:40Motivation
- 10:31Choice polymorphism
- 11:34Typing for variables
- 14:43Anti-unification
- 16:30Choose quantifier
- 18:37Choice polymorphic functions
- 21:51Fixing the is member function example
- 22:55Costed types example
- 24:27Conclusion
related talks
58mLiquidHaskell: Liquid Types for Haskell
34mLiquid Haskell: Verification with Refinement Types
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
23mBetter Defunctionalization through Lambda Set Specialization
16mVerifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
21mPolymorphic Type Inference for Dynamic Languages
45mFunctional Programming bits and pieces
14mThe Simple Essence of Monomorphization