ﻻ يوجد ملخص باللغة العربية
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 programmers language for exceptions and we prove that it has the required behaviour with respect to n-ary functions and conditionals.
This paper presents equational-based logics for proving first order properties of programming languages involving effects. We propose two dual inference system patterns that can be instanciated with monads or comonads in order to be used for proving
We define a proof system for exceptions which is close to the syntax for exceptions, in the sense that the exceptions do not appear explicitly in the type of any expression. This proof system is sound with respect to the intended denotational semanti
It is well established that equational algebraic theories, and the monads they generate, can be used to encode computational effects. An important insight of Power and Shkaravska is that comodels of an algebraic theory T -- i.e., models in the opposi
In this short note we study the semantics of two basic computational effects, exceptions and states, from a new point of view. In the handling of exceptions we dissociate the control from the elementary operation which recovers from the exception. In
This note is about using computational effects for scalability. With this method, the specification gets more and more complex while its semantics gets more and more correct. We show, from two fundamental examples, that it is possible to design a ded