Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
arXiv:1610.09254 · doi:10.1007/978-3-662-54458-7_31
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.
v1: 16 pages. v2: 17 pages, llncs style. Minor changes. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-54458-7_31
References in corpus (2)
Cited by in corpus (11)
- Interaction Trees: Representing Recursive and Impure Programs in Coq
- Two-Level Type Theory and Applications
- Quotient inductive-inductive types
- Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
- Large and Infinitary Quotient Inductive-Inductive Types
- Synthetic topology in Homotopy Type Theory for probabilistic programming
- Free Higher Groups in Homotopy Type Theory
- Connecting Constructive Notions of Ordinals in Homotopy Type Theory
- Inductive and Coinductive Predicate Liftings for Effectful Programs
- Big Steps in Higher-Order Mathematical Operational Semantics
- A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures