@inproceedings{ca2c622857654e9287978f385ce86192,
title = "Partiality and Container Monads",
abstract = "We investigate monads of partiality in Martin-L{\"o}f type theory, following Moggi{\textquoteright}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{\textquoteright}s notion of dominance. We provide several examples, putting particular emphasis on Capretta{\textquoteright}s delay monad and its quotiented variant, the non-termination monad.",
keywords = "Martin-L{\"o}f type theory, monads of partiality, lifting monads, effectful computations, containers, Martin-L{\"o}f type theory, monads of partiality, lifting monads, effectful computations, containers",
author = "Tarmo Uustalu and Niccol{\`o} Veltri",
year = "2017",
doi = "10.1007/978-3-319-71237-6_20",
language = "English",
isbn = "978-3-319-71237-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "406--425",
editor = "Chang, {Bor-Yuh Evan}",
booktitle = "Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings",
address = "Germany",
note = "Asian Symposium on Programming Languages and Systems, APLAS ; Conference date: 27-11-2017 Through 29-11-2017",
}