ترغب بنشر مسار تعليمي؟ اضغط هنا

States and exceptions considered as dual effects

130   0   0.0 ( 0 )
 نشر من قبل Dominique Duval
 تاريخ النشر 2010
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

In this paper we consider the two major computational effects of states and exceptions, from the point of view of diagrammatic logics. We get a surprising result: there exists a symmetry between these two effects, based on the well-known categorical duality between products and coproducts. More precisely, the lookup and update operations for states are respectively dual to the throw and catch operations for exceptions. This symmetry is deeply hidden in the programming languages; in order to unveil it, we start from the monoidal equational logic and we add progressively the logical features which are necessary for dealing with either effect. This approach gives rise to a new point of view on states and exceptions, which bypasses the problems due to the non-algebraicity of handling exceptions.



قيم البحث

اقرأ أيضاً

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 way it becomes apparent that there is a duality, in the categorical sense, between exceptions and states.
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 cs of exceptions. With this inference system we prove several properties of exceptions.
An algebraic method is used to study the semantics of exceptions in computer languages. The exceptions form a computational effect, in the sense that there is an apparent mismatch between the syntax of exceptions and their intended semantics. We solv e this apparent contradiction by efining a logic for exceptions with a proof system which is close to their syntax and where their intended semantics can be seen as a model. This requires a robust framework for logics and their morphisms, which is provided by categorical tools relying on adjunctions, fractions and limit sketches.
291 - Dominique Duval 2018
In this short paper, using category theory, we argue that logical rules can be seen as fractions and logics as limit sketches.
114 - Dominique Duval 2013
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 uction system for a specification involving an effect without expliciting this effect.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا