TY - GEN
T1 - Partiality and container monads
AU - Veltri, Niccolò
N1 - 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.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85035057965
U2 - 10.1007/978-3-319-71237-6_20
DO - 10.1007/978-3-319-71237-6_20
M3 - Conference contribution
SN - 9783319712369
T3 - Lecture Notes in Computer Science
SP - 406
EP - 425
BT - Programming Languages and Systems
A2 - Chang, Bor-Yuh Evan
PB - Springer, Cham
T2 - 15th Asian Symposium on Programming Languages and Systems, APLAS 2017
Y2 - 27 November 2017 through 29 November 2017
ER -