Skip to main content

Research Repository

Advanced Search

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type

Altenkirch, Thorsten; Danielson, Nils Anders; Kraus, Nicolai

Authors

Nils Anders Danielson



Abstract

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.

Citation

Altenkirch, T., Danielson, N. A., & Kraus, N. (2017). Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. In Foundations of Software Science and Computation Structures: FoSSaCS 2017 (534-549). https://doi.org/10.1007/978-3-662-54458-7_31

Conference Name 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software
Conference Location Uppsala, Sweden
Start Date Apr 22, 2017
End Date Apr 29, 2017
Acceptance Date Dec 22, 2016
Online Publication Date Mar 15, 2017
Publication Date Mar 16, 2017
Deposit Date Mar 24, 2017
Publicly Available Date Mar 29, 2024
Journal FOSSACS
Publisher Springer Publishing Company
Peer Reviewed Peer Reviewed
Pages 534-549
Series Title Lecture Notes in Computer Science
Series Number 10203
Series ISSN 0302-9743
Book Title Foundations of Software Science and Computation Structures: FoSSaCS 2017
Chapter Number 31
ISBN 978-3-662-54457-0
DOI https://doi.org/10.1007/978-3-662-54458-7_31
Public URL https://nottingham-repository.worktribe.com/output/832490
Publisher URL https://link.springer.com/chapter/10.1007%2F978-3-662-54458-7_31
Additional Information First Online: 16 March 2017; Conference Acronym: FoSSaCS; Conference Name: International Conference on Foundations of Software Science and Computation Structures; Conference City: Uppsala; Conference Country: Sweden; Conference Year: 2017; Conference Start Date: 24 April 2017; Conference End Date: 27 April 2017; Conference Number: 20; Conference ID: fossacs2017; Conference URL: http://www.etaps.org/index.php/2017/fossacs; Free to read: This content has been made available to all.

Files





You might also like



Downloadable Citations