Partiality and Container Monads
Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review
We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this paper, we unveil the relationship between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.
Original language | English |
---|---|
Title of host publication | Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings |
Editors | Bor-Yuh Evan Chang |
Number of pages | 20 |
Place of Publication | Cham |
Publisher | Springer |
Publication date | 2017 |
Pages | 406-425 |
ISBN (Print) | 978-3-319-71237-6 |
DOIs | |
Publication status | Published - 2017 |
Event | Asian Symposium on Programming Languages and Systems - Duration: 27 Nov 2017 → 29 Nov 2017 |
Conference
Conference | Asian Symposium on Programming Languages and Systems |
---|---|
Periode | 27/11/2017 → 29/11/2017 |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 10695 |
ISSN | 0302-9743 |
Downloads
No data available
ID: 82321093