Partiality, revisited: the partiality monad as a quotient inductive-inductive type
Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the "right" notion of equality, weak bisimilarity. However, recent work by Chapman et a...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Published: |
Springer Verlag
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/38095/ |
| _version_ | 1848795596729614336 |
|---|---|
| author | Altenkirch, Thorsten Danielsson, Nils Anders Kraus, Nicolai |
| author_facet | Altenkirch, Thorsten Danielsson, Nils Anders Kraus, Nicolai |
| author_sort | Altenkirch, Thorsten |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the "right" notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications. |
| first_indexed | 2025-11-14T19:34:36Z |
| format | Article |
| id | nottingham-38095 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:34:36Z |
| publishDate | 2017 |
| publisher | Springer Verlag |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-380952020-05-04T18:38:00Z https://eprints.nottingham.ac.uk/38095/ Partiality, revisited: the partiality monad as a quotient inductive-inductive type Altenkirch, Thorsten Danielsson, Nils Anders Kraus, Nicolai Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the "right" notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications. Springer Verlag 2017-03-16 Article PeerReviewed Altenkirch, Thorsten, Danielsson, Nils Anders and Kraus, Nicolai (2017) Partiality, revisited: the partiality monad as a quotient inductive-inductive type. Lecture Notes in Computer Science, 10203 . pp. 534-549. ISSN 0302-9743 homotopy type theory quotient inductive-inductive type partiality partial computation https://link.springer.com/chapter/10.1007/978-3-662-54458-7_31 doi:10.1007/978-3-662-54458-7_31 doi:10.1007/978-3-662-54458-7_31 |
| spellingShingle | homotopy type theory quotient inductive-inductive type partiality partial computation Altenkirch, Thorsten Danielsson, Nils Anders Kraus, Nicolai Partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| title | Partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| title_full | Partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| title_fullStr | Partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| title_full_unstemmed | Partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| title_short | Partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| title_sort | partiality, revisited: the partiality monad as a quotient inductive-inductive type |
| topic | homotopy type theory quotient inductive-inductive type partiality partial computation |
| url | https://eprints.nottingham.ac.uk/38095/ https://eprints.nottingham.ac.uk/38095/ https://eprints.nottingham.ac.uk/38095/ |