Quotient Polymorphism
Abstract
Quotient types increase the power of type systems by allowing types to include equational properties. However, two key practical issues arise: code being duplicated, and valid code being rejected. Specifically, function definitions often need to be repeated for each quotient of a type, and valid functions may be rejected if they include subterms that do not respect the quotient. This article addresses these reusability and expressivity issues by introducing a notion of quotient polymorphism that we call choice polymorphism . We give practical examples of its use, develop the underlying theory, and implement it in Quotient Haskell.
Fields of Study & Subjects
Logic
programming
and type systems
Software Engineering and Design Patterns
Computability
AI Algorithms
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Volume
- 10
- Issue
- POPL
- Pages
- 659–687
- Publication date
- 8 January 2026
- Language
- EN