Abstract
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 |
| Subtitle of host publication | 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings |
| Editors | Bor-Yuh Evan Chang |
| Publisher | Springer, Cham |
| Pages | 406-425 |
| ISBN (Print) | 9783319712369 |
| DOIs | |
| Publication status | Published - 2017 |
| Event | 15th Asian Symposium on Programming Languages and Systems, APLAS 2017 - Suzhou, China Duration: 27 Nov 2017 → 29 Nov 2017 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Volume | 10695 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 15th Asian Symposium on Programming Languages and Systems, APLAS 2017 |
|---|---|
| Country/Territory | China |
| City | Suzhou |
| Period | 27/11/17 → 29/11/17 |
Bibliographical note
Funding Information:This research was supported by the ERDF funded Estonian national CoE project EXCITE and the Estonian Ministry of Education and Research institutional research grant IUT33-13.
Publisher Copyright:
© Springer International Publishing AG 2017.