Adjunctions for exceptions

TL;DR

This paper introduces a categorical algebraic framework to model the semantics of exceptions in programming languages, resolving the mismatch between syntax and semantics through a logic-based approach.

Contribution

It develops a novel categorical logic for exceptions using adjunctions and limit sketches, bridging syntax and semantics in a rigorous way.

Findings

A logic for exceptions closely aligned with their syntax is formulated.

Semantics of exceptions are modeled as categorical adjunctions.

The framework provides a robust foundation for reasoning about exceptions.

Abstract

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 solve 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.