Partiality, Revisited
From MaRDI portal
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.
Recommendations
- Monads and algebras in the semantics of partial data types
- Partiality and Container Monads
- scientific article; zbMATH DE number 1341476
- scientific article; zbMATH DE number 3285192
- Partial elements and recursion via dominances in univalent type theory
- scientific article; zbMATH DE number 1424053
- Partially monadic functors
- Monotone (co)inductive types and positive fixed-point types
- Monads, partial evaluations, and rewriting
- Quotients, inductive types, and quotient inductive types
Cites work
- General Recursion via Coinductive Types
- Generalizations of Hedberg's theorem
- Higher inductive types as homotopy-initial algebras
- scientific article; zbMATH DE number 1795226 (Why is no real title available?)
- Inductive types in homotopy type theory
- On the Cauchy completeness of the constructive Cauchy reals
- Operational semantics using the partiality monad
- Partiality, Revisited
- Quotient inductive-inductive types
- Quotienting the delay monad by weak bisimilarity
- Some Domain Theory and Denotational Semantics in Coq
- The independence of Markov's principle in type theory
- Type theory in type theory using quotient inductive types
Cited in
(23)- The delay monad and restriction categories
- The construction of set-truncated higher inductive types
- Type-theoretic approaches to ordinals
- Quotienting the delay monad by weak bisimilarity
- Partiality, Revisited
- Partiality, state and dependent types
- Quotienting the delay monad by weak bisimilarity
- scientific article; zbMATH DE number 7080198 (Why is no real title available?)
- Constructing higher inductive types as groupoid quotients
- The Scott model of PCF in univalent type theory
- Synthetic topology in Homotopy Type Theory for probabilistic programming
- Partiality and Container Monads
- Modalities in homotopy type theory
- Higher Structures in Homotopy Type Theory
- Streams of approximations, equivalence of recursive effectful programs
- Two-level type theory and applications
- Inductive and coinductive predicate liftings for effectful programs
- Representing guardedness in call-by-value and guarded parametrized monads
- Towards constructive hybrid semantics
- What monads can and cannot do with a bit of extra time
- Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
- Uniform Elgot iteration in foundations
- Initial algebras of domains via quotient inductive-inductive types
This page was built for publication: Partiality, Revisited
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988390)
