Quotient Haskell: Lightweight Quotient Types for All

Hewer, Brandon; Hutton, Graham

Abstract

Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.

• Journal Article Type: Article
• Conference Name: ACM SIGPLAN Symposium on Principles of Programming Languages
• Conference Location: London, United Kingdom
• Acceptance Date: Nov 7, 2023
• Online Publication Date: Jan 5, 2024
• Publication Date: Jan 5, 2024
• Deposit Date: Nov 8, 2023
• Publicly Available Date: Jan 11, 2024
• Journal: Proceedings of the ACM on Programming Languages
• Electronic ISSN: 2475-1421
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 8
• Issue: POPL
• Article Number: 27
• Pages: 785-815
• DOI: https://doi.org/10.1145/3632869
• Keywords: quotient types, refinement types, static verification
• Public URL: https://nottingham-repository.worktribe.com/output/27078391
• Publisher URL: https://dl.acm.org/journal/pacmpl
• Additional Information: Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). © 2024 Copyright held by the owner/author(s).