A duality between exceptions and states
From MaRDI portal
Publication:2909735
DOI10.1017/S0960129511000752zbMATH Open1280.68120arXiv1402.1051OpenAlexW2101091770MaRDI QIDQ2909735FDOQ2909735
Authors: Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud
Publication date: 6 September 2012
Published in: MSCS. Mathematical Structures in Computer Science (Search for Journal in Brave)
Abstract: Computational effects may often be interpreted in the Kleisli category of a monad or in the coKleisli category of a comonad. The duality between monads and comonads corresponds, in general, to a symmetry between construction and observation, for instance between raising an exception and looking up a state. Thanks to the properties of adjunction one may go one step further: the coKleisli-on-Kleisli category of a monad provides a kind of observation with respect to a given construction, while dually the Kleisli-on-coKleisli category of a comonad provides a kind of construction with respect to a given observation. In the previous examples this gives rise to catching an exception and updating a state. However, the interpretation of computational effects is usually based on a category which is not self-dual, like the category of sets. This leads to a breaking of the monad-comonad duality. For instance, in a distributive category the state effect has much better properties than the exception effect. This remark provides a novel point of view on the usual mechanism for handling exceptions. The aim of this paper is to build an equational semantics for handling exceptions based on the coKleisli-on-Kleisli category of the monad of exceptions. We focus on n-ary functions and conditionals. We propose a programmer's language for exceptions and we prove that it has the required behaviour with respect to n-ary functions and conditionals.
Full work available at URL: https://arxiv.org/abs/1402.1051
Recommendations
Cites Work
Cited In (7)
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- Dynamic state restoration using versioning exceptions
- Title not available (Why is that?)
- Successes and failures in the construction of NESS-states
- Logical rules as fractions and logics as sketches
- Monads and adjunctions for global exceptions
- Deduction as reduction, from a categorical point of view
This page was built for publication: A duality between exceptions and states
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2909735)