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 \emph{choice polymorphism}. We give practical examples of its use, develop the underlying theory, and implement it in Quotient Haskell.
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
10:30 - 12:10 | |||
10:30 25mTalk | Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen DOI | ||
10:55 25mTalk | Quotient PolymorphismDistinguished Paper POPL DOI | ||
11:20 25mTalk | The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types POPL Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology DOI | ||
11:45 25mTalk | Welterweight Go: Boxing, Structural Subtyping, and Generics POPL Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google DOI | ||