Partiality and Container Monads

Tarmo Uustalu, Niccolò Veltri

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


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
Publication date2017
ISBN (Print)978-3-319-71237-6
Publication statusPublished - 2017
EventAsian Symposium on Programming Languages and Systems -
Duration: 27 Nov 201729 Nov 2017


ConferenceAsian Symposium on Programming Languages and Systems
SeriesLecture Notes in Computer Science


  • Martin-Löf type theory
  • monads of partiality
  • lifting monads
  • effectful computations
  • containers


Dive into the research topics of 'Partiality and Container Monads'. Together they form a unique fingerprint.

Cite this