Partiality, revisited: The partiality monad as a quotient inductive-inductive type

Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Citations (Scopus)
143 Downloads (Pure)

Abstract

Capretta’s delay monad can be used to model partial computations, but it has the “wrong” notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the “right” notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory—a higher inductive-inductive type—we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publication20th International Conference, FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
EditorsJavier Esparza, Andrzej S. Murawski
PublisherSpringer
Pages534-549
Number of pages16
ISBN (Electronic)9783662544587
ISBN (Print)9783662544570
DOIs
Publication statusPublished - 16 Mar 2017
Event20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10203
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
Country/TerritorySweden
City Uppsala
Period22/04/1729/04/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Partiality, revisited: The partiality monad as a quotient inductive-inductive type'. Together they form a unique fingerprint.

Cite this