Related papers: A Recipe for State-and-Effect Triangles
Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads have been suggested which provide a more fine-grained model…
Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning…
Recent advances in programming languages study and design have established a standard way of grounding computational systems representation in category theory. These formal results led to a better understanding of issues of control and…
In this essay, I present the advantages and, I dare say, the beauty of programming in a language with set-theoretic types, that is, types that include union, intersection, and negation type connectives. I show by several examples how…
Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the…
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…
Large pre-trained language models have recently been expanded and applied to programming language tasks with great success, often through further pre-training of a strictly-natural language model--where training sequences typically contain…
Computer programs are often factored into pure components -- simple, total functions from inputs to outputs -- and components that may have side effects -- errors, changes to memory, parallel threads, abortion of the current loop, etc. We…
In semantics and in programming practice, algebraic concepts such as monads or, essentially equivalently, (large) Lawvere theories are a well-established tool for modelling generic side-effects. An important issue in this context are…
We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational…
Most often, in a categorical semantics for a programming language, the substitution of terms is expressed by composition and finite products. However this does not deal with the order of evaluation of arguments, which may have major…
Monadic programming presents a significant challenge for many programmers. In light of category theory, we offer a new perspective on the use of monads in functional programming. This perspective is clarified through numerous examples coded…
This thesis revolves around an area of computer science called "semantics". We work with operational semantics, equational theories, and denotational semantics. The first contribution of this thesis is a study of the commutativity of…
In order to gain a better understanding of the state space of programs, with the aim of making their verification more tractable, models based on directed topological spaces have been introduced, allowing to take in account equivalence…
From every pair of adjoint functors it is possible to produce a (possibly trivial) equivalence of categories by restricting to the subcategories where the unit and counit are isomorphisms. If we do this for the adjunction between effect…
In the quest to give a formal compositional semantics to natural languages, semanticists have started turning their attention to phenomena that have been also considered as parts of pragmatics (e.g., discourse anaphora and presupposition…
Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation include monads, type-and-effect systems, and capability…
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…
Completeness proofs in categorical semantics usually proceed by building a syntactic category whose composition is given by substitution. For untyped effectful Call-by-Value languages, this runs into a basic obstacle: there is no canonical…
We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution cost, nondeterminism, global store and interaction with a…