{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T01:02:00Z","timestamp":1767920520355,"version":"3.49.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/Y010744\/1"],"award-info":[{"award-number":["EP\/Y010744\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    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\n                    <jats:italic toggle=\"yes\">choice polymorphism<\/jats:italic>\n                    . We give practical examples of its use, develop the underlying theory, and implement it in Quotient Haskell.\n                  <\/jats:p>","DOI":"10.1145\/3776665","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"659-687","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Quotient Polymorphism"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-8731-6963","authenticated-orcid":false,"given":"Brandon","family":"Hewer","sequence":"first","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9584-5150","authenticated-orcid":false,"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the International Conference on Mathematics of Program Construction.","author":"Abbott Michael","year":"2004","unstructured":"Michael Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. 2004. Constructing Polymorphic Programs with Quotient Types. In Proceedings of the International Conference on Mathematics of Program Construction."},{"key":"e_1_2_1_2_1","volume-title":"Quotient Inductive-Inductive Types. In International Conference on Foundations of Software Science and Computation Structures.","author":"Altenkirch Thorsten","year":"2018","unstructured":"Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. 2018. Quotient Inductive-Inductive Types. In International Conference on Foundations of Software Science and Computation Structures."},{"key":"e_1_2_1_3_1","volume-title":"International Conference on Foundations of Software Science and Computation Structures.","author":"Altenkirch Thorsten","year":"2017","unstructured":"Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. 2017. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. In International Conference on Foundations of Software Science and Computation Structures."},{"key":"e_1_2_1_4_1","volume-title":"Type Theory in Type Theory using Quotient Inductive Types. ACM SIGPLAN Notices, 51, 1","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch and Ambrus Kaposi. 2016. Type Theory in Type Theory using Quotient Inductive Types. ACM SIGPLAN Notices, 51, 1 (2016)."},{"key":"e_1_2_1_5_1","article-title":"Setoids in Type Theory","volume":"13","author":"Barthe Gilles","year":"2003","unstructured":"Gilles Barthe, Venanzio Capretta, and Olivier Pons. 2003. Setoids in Type Theory. Journal of Functional Programming, 13, 2 (2003).","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_1_6_1","article-title":"Refinement Types for Secure Implementations","volume":"33","author":"Bengtson Jesper","year":"2011","unstructured":"Jesper Bengtson, Karthikeyan Bhargavan, C\u00e9dric Fournet, Andrew D Gordon, and Sergio Maffeis. 2011. Refinement Types for Secure Implementations. ACM Transactions on Programming Languages and Systems, 33, 2 (2011).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the International Conference on Functional programming.","author":"Breitner Joachim","year":"2014","unstructured":"Joachim Breitner, Richard A Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2014. Safe Zero-Cost Coercions for Haskell. In Proceedings of the International Conference on Functional programming."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Conference on Interactive Theorem Proving.","author":"Cohen Cyril","year":"2013","unstructured":"Cyril Cohen. 2013. Pragmatic Quotient Types in Coq. In Proceedings of the International Conference on Interactive Theorem Proving."},{"key":"e_1_2_1_9_1","unstructured":"R. L. Constable S. F. Allen H. M. Bromley W. R. Cleaveland J. F. Cremer R. W. Harper D. J. Howe T. B. Knoblock N. P. Mendler P. Panangaden J. T. Sasaki and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Conference on Automated Deduction.","author":"de Moura Leonardo","year":"2015","unstructured":"Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Proceedings of the International Conference on Automated Deduction."},{"key":"e_1_2_1_11_1","volume-title":"Constructing Infinitary Quotient-Inductive Types. In International Conference on Foundations of Software Science and Computation Structures.","author":"Fiore Marcelo P","year":"2020","unstructured":"Marcelo P Fiore, Andrew M Pitts, and SC Steenkamp. 2020. Constructing Infinitary Quotient-Inductive Types. In International Conference on Foundations of Software Science and Computation Structures."},{"key":"e_1_2_1_12_1","volume-title":"Logical Methods in Computer Science, 18","author":"Fiore Marcelo P","year":"2022","unstructured":"Marcelo P Fiore, Andrew M Pitts, and SC Steenkamp. 2022. Quotients, Inductive Types, and Quotient Inductive Types. Logical Methods in Computer Science, 18 (2022)."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the Symposium on Principles of Programming Languages.","author":"Flanagan Cormac","year":"2006","unstructured":"Cormac Flanagan. 2006. Hybrid Type Checking. In Proceedings of the Symposium on Principles of Programming Languages."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the Conference on Programming Language Design and Implementation.","author":"Freeman Tim","year":"1991","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proceedings of the Conference on Programming Language Design and Implementation."},{"key":"e_1_2_1_15_1","volume-title":"REST: Integrating Term Rewriting with Program Verification (Extended Version). arXiv preprint arXiv:2202.05872","author":"Grannan Zachary","year":"2022","unstructured":"Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J Summers. 2022. REST: Integrating Term Rewriting with Program Verification (Extended Version). arXiv preprint arXiv:2202.05872"},{"key":"e_1_2_1_16_1","volume-title":"Subtyping Without Reduction. In International Conference on Mathematics of Program Construction.","author":"Hewer Brandon","year":"2022","unstructured":"Brandon Hewer and Graham Hutton. 2022. Subtyping Without Reduction. In International Conference on Mathematics of Program Construction."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the ACM on Programming Languages, 8, POPL","author":"Hewer Brandon","year":"2024","unstructured":"Brandon Hewer and Graham Hutton. 2024. Quotient Haskell: Lightweight Quotient Types For All. Proceedings of the ACM on Programming Languages, 8, POPL (2024), Article 27."},{"key":"e_1_2_1_18_1","volume-title":"On the Interpretation of Type Theory in Locally Cartesian Closed Categories. In International Workshop on Computer Science Logic.","author":"Hofmann Martin","year":"1994","unstructured":"Martin Hofmann. 1994. On the Interpretation of Type Theory in Locally Cartesian Closed Categories. In International Workshop on Computer Science Logic."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications.","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann. 1995. A Simple Model for Quotient Types. In Proceedings of the International Conference on Typed Lambda Calculi and Applications."},{"key":"e_1_2_1_20_1","volume-title":"Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL. In Certified Programs and Proofs: Third International Conference.","author":"Huffman Brian","year":"2013","unstructured":"Brian Huffman and Ond\u0159ej Kun\u010dar. 2013. Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL. In Certified Programs and Proofs: Third International Conference."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the Symposium on Applied Computing.","author":"Kaliszyk Cezary","year":"2011","unstructured":"Cezary Kaliszyk and Christian Urban. 2011. Quotients Revisited for Isabelle\/HOL. In Proceedings of the Symposium on Applied Computing."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification.","author":"Kawaguchi Ming","year":"2010","unstructured":"Ming Kawaguchi, Patrick M Rondon, and Ranjit Jhala. 2010. Dsolve: Safety Verification via Liquid Types. In Proceedings of the International Conference on Computer Aided Verification."},{"key":"e_1_2_1_23_1","volume-title":"Quotient Types in Type Theory. Ph. D. Dissertation","author":"Nuo Li.","unstructured":"Nuo Li. 2015. Quotient Types in Type Theory. Ph. D. Dissertation. University of Nottingham."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the Symposium on Implementation and Application of Functional Languages.","author":"Marmaduke Andrew","year":"2020","unstructured":"Andrew Marmaduke, Christopher Jenkins, and Aaron Stump. 2020. Zero-Cost Constructor Subtyping. In Proceedings of the Symposium on Implementation and Application of Functional Languages."},{"key":"e_1_2_1_25_1","volume-title":"International Conference on Theorem Proving in Higher Order Logics.","author":"Nogin Aleksey","year":"2002","unstructured":"Aleksey Nogin. 2002. Quotient types: A Modular Approach. In International Conference on Theorem Proving in Higher Order Logics."},{"key":"e_1_2_1_26_1","volume-title":"The Eighth International Workshop on Coq for Programming Languages.","author":"Paranhos Fabr\u0131cio S","year":"2022","unstructured":"Fabr\u0131cio S Paranhos and Daniel Ventura. 2022. Towards a Formalization of Nominal Sets in Coq. In The Eighth International Workshop on Coq for Programming Languages."},{"key":"e_1_2_1_27_1","article-title":"Defining Functions on Equivalence Classes","volume":"7","author":"Paulson Lawrence C","year":"2006","unstructured":"Lawrence C Paulson. 2006. Defining Functions on Equivalence Classes. ACM Transactions on Computational Logic, 7, 4 (2006).","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_2_1_28_1","volume-title":"Program Synthesis from Polymorphic Refinement Types. ACM SIGPLAN Notices, 51, 6","author":"Polikarpova Nadia","year":"2016","unstructured":"Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. ACM SIGPLAN Notices, 51, 6 (2016)."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the ACM on Programming Languages, 6, POPL","author":"Pujet Lo\u00efc","year":"2022","unstructured":"Lo\u00efc Pujet and Nicolas Tabareau. 2022. Observational Equality: Now For Good. Proceedings of the ACM on Programming Languages, 6, POPL (2022)."},{"key":"e_1_2_1_30_1","volume-title":"Liquid Types. In Proceedings of the Conference on Programming Language Design and Implementation.","author":"Rondon Patrick M","year":"2008","unstructured":"Patrick M Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proceedings of the Conference on Programming Language Design and Implementation."},{"key":"e_1_2_1_31_1","article-title":"Subtypes for Specifications: Predicate Subtyping in PVS","volume":"24","author":"Rushby John","year":"1998","unstructured":"John Rushby, Sam Owre, and Natarajan Shankar. 1998. Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Transactions on Software Engineering, 24, 9 (1998).","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_2_1_32_1","unstructured":"Mike Shulman. 2014. Higher Inductive-Recursive Univalence and Type-Directed Definitions."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Conference on Theorem Proving in Higher Order Logics.","author":"Slotosch Oscar","year":"1997","unstructured":"Oscar Slotosch. 1997. Higher Order Quotients and their Implementation in Isabelle HOL. In Proceedings of the International Conference on Theorem Proving in Higher Order Logics."},{"key":"e_1_2_1_34_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Conference on LISP and Functional Programming.","author":"Thompson Simon","year":"1986","unstructured":"Simon Thompson. 1986. Laws in Miranda. In Proceedings of the Conference on LISP and Functional Programming."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the International Conference on Interactive Theorem Proving.","author":"van Doorn Floris","year":"2017","unstructured":"Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. In Proceedings of the International Conference on Interactive Theorem Proving."},{"key":"e_1_2_1_37_1","volume-title":"Liquid Haskell: Haskell as a Theorem Prover. Ph. D. Dissertation","author":"Vazou Niki","year":"2016","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph. D. Dissertation. University of California San Diego."},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the International Conference on Functional Programming.","author":"Vazou Niki","year":"2015","unstructured":"Niki Vazou, Alexander Bakst, and Ranjit Jhala. 2015. Bounded Refinement Types. In Proceedings of the International Conference on Functional Programming."},{"key":"e_1_2_1_39_1","volume-title":"Abstract Refinement Types. In European Symposium on Programming.","author":"Vazou Niki","year":"2013","unstructured":"Niki Vazou, Patrick M Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In European Symposium on Programming."},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the International Conference on Functional Programming.","author":"Vazou Niki","year":"2014","unstructured":"Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In Proceedings of the International Conference on Functional Programming."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","author":"Vazou Niki","year":"2017","unstructured":"Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G Scott, Ryan R Newton, Philip Wadler, and Ranjit Jhala. 2017. Refinement reflection: complete verification with SMT. Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201331."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the ACM on Programming Languages, 3, ICFP","author":"Vezzosi Andrea","year":"2019","unstructured":"Andrea Vezzosi, Anders M\u00f6rtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proceedings of the ACM on Programming Languages, 3, ICFP (2019)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776665","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:06:40Z","timestamp":1767899200000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776665"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776665"],"URL":"https:\/\/doi.org\/10.1145\/3776665","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}