arXiv subjects

Dylan McDermott

Publications and source records attributed to Dylan McDermott.

11 recordsLinked to original sources

arXiv2026

Presheaves and cocompletions in formal category theory

We study the relationship between presheaf constructions and free cocompletions in the context of formal category theory, elucidating the coincidence between the two concepts in familiar settings. We show that, in a virtual equipment satisfying mild assumptions, free cocompletions under classes of weights are exhibited by presheaf constructions. We furthermore extend the theory of weighted colimits from enriched category theory to this setting, developing the concepts of atomicity and rank, and providing recognition theorems for presheaf objects, free cocompletions, and cocomplete objects. As an application of our methods, we construct free cocompletions, under arbitrary classes of colimit-small weights, of (possibly large) categories enriched in (not necessarily symmetric) monoidal categories and bicategories; this resolves a longstanding omission in the literature on enriched category theory.

math.CT↗

arXiv2026

Denotational reasoning for asynchronous multiparty session types

We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It enables us to prove the correctness of communication optimisations, in particular, those involving reordering of messages. Our development crucially relies on modelling message-passing as a computational effect. We apply grading, a paradigm for tracking computational effects, to asynchronous message-passing, demonstrating that multiparty session typing can be viewed as an instance of grading. We demonstrate the utility of our model by showing that it forms an adequate denotational semantics for a call-by-value asynchronous message-passing calculus, that ensures communication safety, deadlock-freedom and liveness in the presence of communication optimisations.

cs.PL↗

arXiv2024

The nerve theorem for relative monads

A fundamental result in the theory of monads is the characterisation of the category of algebras for a monad in terms of a pullback of the category of presheaves on the category of free algebras: intuitively, this expresses that every algebra is a colimit of free algebras. We establish an analogous result for enriched relative monads with dense roots, and explain how it generalises the nerve theorems for monads with arities and nervous monads. As an application, we derive sufficient conditions for the existence of algebraic colimits of relative monads. More generally, we establish such a characterisation of the category of algebras in the context of an exact virtual equipment. In doing so, we are led to study the relationship between a $j$-relative monad $T$ and its associated loose-monad $E(j, T)$, and consequently show that the opalgebra object and the algebra object for $T$ may be constructed from certain double categorical limits and colimits associated to $E(j, T)$.

math.CT↗

arXiv2023

Canonical Gradings of Monads

We define a notion of grading of a monoid T in a monoidal category C, relative to a class of morphisms M (which provide a notion of M-subobject). We show that, under reasonable conditions (including that M forms a factorization system), there is a canonical grading of T. Our application is to graded monads and models of computational effects. We demonstrate our results by characterizing the canonical gradings of a number of monads, for which C is endofunctors with composition. We also show that we can obtain canonical grades for algebraic operations.

cs.LO↗

arXiv2023

Relative monadicity

We establish a relative monadicity theorem for relative monads with dense roots in a virtual equipment, specialising to a relative monadicity theorem for enriched relative monads. In particular, for a dense $\mathbb V$-functor $j \colon A \to E$, a $\mathbb V$-functor $r \colon D \to E$ is $j$-monadic if and only if $r$ admits a left $j$-relative adjoint and creates $j$-absolute colimits. This provides a refinement of the classical monadicity theorem -- characterising those categories whose objects are given by those of $E$ equipped with algebraic structure -- in which the arities of the algebraic operations are valued in $A$. In particular, when $j = 1$, we recover a formal monadicity theorem. Furthermore, we examine the interaction between the pasting law for relative adjunctions and relative monadicity. As a consequence, we derive necessary and sufficient conditions for the ($j$-relative) monadicity of the composite of a $\mathbb V$-functor with a ($j$-relatively) monadic $\mathbb V$-functor.

math.CT↗

arXiv2023

The formal theory of relative monads

We develop the theory of relative monads and relative adjunctions in a virtual equipment, extending the theory of monads and adjunctions in a 2-category. The theory of relative comonads and relative coadjunctions follows by duality. While some aspects of the theory behave analogously to the non-relative setting, others require new insights. In particular, the universal properties that define the algebra object and the opalgebra object for a monad in a virtual equipment are stronger than the classical notions of algebra object and opalgebra object for a monad in a 2-category. Inter alia, we prove a number of representation theorems for relative monads, establishing the unity of several concepts in the literature, including the devices of Walters, the $j$-monads of Diers, and the relative monads of Altenkirch, Chapman, and Uustalu. A motivating setting is the virtual equipment $\mathbb{V}\text{-}\mathbf{\mathbb{C}at}$ of categories enriched in a monoidal category $\mathbb{V}$, though many of our results are new even for $\mathbb{V} = \mathbf{Set}$.

math.CT↗

arXiv2022

What Makes a Strong Monad?

Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that have free variables. Strength is non-trivial: it can be difficult to determine whether a monad has any strength at all, and monads can be strong in multiple ways. We therefore review some of the most important known facts about strength and prove some new ones. In particular, we present a number of equivalent characterizations of strong functor and strong monad, and give some conditions that guarantee existence or uniqueness of strengths. We look at strength from three different perspectives: actions of a monoidal category V, enrichment over V, and powering over V. We are primarily motivated by semantics of effects, but the results are also useful in other contexts.

cs.LO↗

arXiv2022

Galois connecting call-by-value and call-by-name

We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving properties like these. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We show that the call-by-value and call-by-name translations of expressions into call-by-push-value have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the call-by-value and call-by-name interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example computational effects including divergence and nondeterminism.

cs.PL↗

arXiv2021

Abstract clones for abstract syntax

We give a formal treatment of simple type theories, such as the simply-typed $\lambda$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $\lambda$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $\beta$- and $\eta$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.

cs.LO↗

arXiv2018

Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics

Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for type-and-effect systems involves a parameterised family of monads whose size is exponential in the number of effects. We derive such refined semantics from a single monad over a category, a choice of algebraic operations for this monad, and a suitable factorisation system over this category. We relate the derived semantics to the original semantics using fibrations for logical relations. Our proof uses a folklore technique for lifting monads with operations.

cs.PL↗

arXiv2017

A monadic solution to the Cartwright-Felleisen-Wadler conjecture

Given a programming language, can we give a monadic denotational semantics that is stable under language extension? Models containing only a single monad are not stable. Models based on type-and-effect systems, in which there is a monad for every set of operations in the language, are. Cartwright and Felleisen, and Wadler, conjectured such monadic semantics can be generated. We describe a new general method of constructing stable models from standard monadic models, based on factorizations of monad morphisms. We show that under certain conditions factorizations induce a monad for every set of operations, and explain why the conditions usually hold. We also describe preliminary work using fibrations for logical relations generated from these factorization systems for proving the correctness of the resulting model.

cs.PL↗