Partiality and Container Monads

Tarmo Uustalu, Niccolò Veltri

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelProgramming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings
RedaktørerBor-Yuh Evan Chang
Antal sider20
UdgivelsesstedCham
ForlagSpringer
Publikationsdato2017
Sider406-425
ISBN (Trykt)978-3-319-71237-6
DOI
StatusUdgivet - 2017
BegivenhedAsian Symposium on Programming Languages and Systems -
Varighed: 27 nov. 201729 nov. 2017

Konference

KonferenceAsian Symposium on Programming Languages and Systems
Periode27/11/201729/11/2017
NavnLecture Notes in Computer Science
Vol/bind10695
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Partiality and Container Monads'. Sammen danner de et unikt fingeraftryk.

Citationsformater