THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
Altenkirch, Thorsten; Danielson, Nils Anders; Kraus, Nicolai
Authors
Nils Anders Danielson
Dr NICOLAI KRAUS NICOLAI.KRAUS@NOTTINGHAM.AC.UK
Professor of Theoretical Computer Science
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
Presentation Conference Type | Edited Proceedings |
---|---|
Conference Name | 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software |
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 24, 2017 |
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. |
Contract Date | Mar 24, 2017 |
Files
partiality.pdf
(495 Kb)
PDF
You might also like
Monads need not be endofunctors
(2015)
Journal Article
Type theory in type theory using quotient inductive types
(2016)
Presentation / Conference Contribution
Normalisation by evaluation for dependent types
(2016)
Presentation / Conference Contribution
Notions of anonymous existence in Martin-Löf type theory
(2017)
Journal Article
Quotient inductive-inductive types
(2018)
Book Chapter
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search