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.

@article{paperbot2608,
  title = {Quotient Haskell: Lightweight Quotient Types for All},
  author = {Brandon Hewer and Graham Hutton},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632869}
}