ITU

Partiality and Container Monads

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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 languageEnglish
Title of host publicationProgramming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings
EditorsBor-Yuh Evan Chang
Number of pages20
Place of PublicationCham
PublisherSpringer
Publication date2017
Pages406-425
ISBN (Print)978-3-319-71237-6
DOIs
Publication statusPublished - 2017
EventAsian Symposium on Programming Languages and Systems -
Duration: 27 Nov 201729 Nov 2017

Conference

ConferenceAsian Symposium on Programming Languages and Systems
Periode27/11/201729/11/2017
SeriesLecture Notes in Computer Science
Volume10695
ISSN0302-9743

Downloads

No data available

ID: 82321093