Dylan McDermott

Drafts

1. The pullback theorem for relative monads.
   Nathanael Arkor and Dylan McDermott.
   Last updated: April 2024.
   arXiv
   abstract

   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 show that the pullback theorem for relative monads holds in any 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).

2. Relative monadicity.
   Nathanael Arkor and Dylan McDermott.
   Last updated: April 2024.
   arXiv
   abstract

   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 V-functor j : A → E, a V-functor r : D → E is j-monadic if and only if r admits a left j-relative adjoint and creates j-absolute colimits. 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-)monadicity of the composite of a V-functor with a (j-)monadic V-functor.

3. Higher-order algebraic theories.
   Nathanael Arkor and Dylan McDermott.
   Last updated: January 2021. See Chapter 4 of Nathanael's thesis for a more recent account.
   PDF
   abstract

   Algebraic theories give a presentation-free categorical formulation of universal algebraic structure: objects equipped with first-order operators, subject to equational laws. Similarly, higher-order algebraic theories describe objects equipped with higher-order, variable-binding operators, such as logical quantifiers or λ-abstraction. While higher-order structures abound in mathematics and computer science, there exists no systematic treatment in the spirit of that for first-order structure. This has led to a proliferation of variations of higher-order theory, and consequently a lacklustre general understanding. We take the first steps to rectify this, defining a notion of multisorted higher-order algebraic theory and carrying out a development analogous to that of the first-order setting. In addition to unifying various previous notions, we (1) establish a correspondence between higher-order algebraic theories and a class of (relative) monads, whose algebras describe the closed-term structure of the corresponding theories; (2) prove that the categories of higher-order algebraic theories, and of the term algebras for a higher-order algebraic theory, are locally strongly finitely presentable; (3) give a new explanation for the apparent asymmetry between models of algebraic theories in the category of sets, and models in arbitrary cartesian categories.

Publications

1. The formal theory of relative monads.
   Nathanael Arkor and Dylan McDermott.
   Journal of Pure and Applied Algebra, 2024. doi:10.1016/j.jpaa.2024.107676
   arXiv
   abstract

   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 V-Cat of categories enriched in a monoidal category V, though many of our results are new even for V = Set.

2. Galois connecting call-by-value and call-by-name.
   Dylan McDermott and Alan Mycroft.
   Logical Methods in Computer Science, 2024. doi:10.46298/lmcs-20(1:13)2024
   local PDF
   abstract

   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.

3. A type system with subtyping for WebAssembly's stack polymorphism.
   Dylan McDermott, Yasuaki Morita, and Tarmo Uustalu.
   ICTAC 2022. doi:10.1007/978-3-031-17715-6_20
   local PDF
   abstract

   We propose a new type system for WebAssembly. It is a refinement of the type system from the language specification and is based on type qualifiers and subtyping. In the WebAssembly specification, a typable instruction sequence gets many different types, depending in particular on whether it contains instructions such as br (unconditional branch) that are stack-polymorphic in an unusual way. But one cannot single out a canonical type for a typable instruction sequence satisfactorily. We introduce qualifiers on code types to distinguish between the two flavors of stack polymorphism that occur in WebAssembly and a subtyping relation on such qualified types. Our type system gives every typable instruction sequence a canonical type that is principal. We show that the new type system is in a precise relationship to the type system given in the WebAssembly specification. In addition, we describe a typed functional-style big-step semantics based on this new type system underpinned by an indexed graded monad and prove that it prevents stack-manipulation related runtime errors. We have formalized our type system, inference algorithm, and semantics in Agda.

4. Flexibly graded monads and graded algebras.
   Dylan McDermott and Tarmo Uustalu.
   MPC 2022. doi:10.1007/978-3-031-16912-0_4
   local PDF, slides
   abstract

   When modelling side-effects using a monad, we need to equip the monad with effectful operations. This can be done by noting that each algebra of the monad carries interpretations of the desired operations. We consider the analogous situation for graded monads, which are a generalization of monads that enable us to track quantitative information about side-effects. Grading makes a significant difference: while many graded monads of interest can be equipped with similar operations, the algebras often cannot. We explain where these operations come from for graded monads. To do this, we introduce the notion of flexibly graded monad, for which the situation is similar to the situation for ordinary monads. We then show that each flexibly graded monad induces a canonical graded monad in such a way that operations for the flexibly graded monad carry over to the graded monad. In doing this, we reformulate grading in terms of locally graded categories, showing in particular that graded monads are a particular kind of relative monad. We propose that locally graded categories are a useful setting for work on grading in general.

5. Flexible presentations of graded monads.
   Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu.
   ICFP 2022. doi:10.1145/3547654
   local PDF, slides
   abstract

   A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of monads that enable us to track quantitative information about the effects being modelled. Correspondingly, a large class of graded monads can be presented using an existing notion of graded presentation. However, the existing notion has some deficiencies, in particular many effects do not have natural graded presentations.

   We introduce a notion of flexibly graded presentation that does not suffer from these issues, and develop the associated theory. We show that every flexibly graded presentation induces a graded monad equipped with interpretations of the operations of the presentation, and that all graded monads satisfying a particular condition on colimits have a flexibly graded presentation. As part of this, we show that the usual algebra-preserving correspondence between presentations and a class of monads transfers to an algebra-preserving correspondence between flexibly graded presentations and a class of flexibly graded monads.

6. Canonical gradings of monads.
   Flavien Breuvart, Dylan McDermott, and Tarmo Uustalu.
   ACT 2022. doi:10.4204/EPTCS.380.1
   local PDF, slides
   abstract

   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.

7. What makes a strong monad?
   Dylan McDermott and Tarmo Uustalu.
   MSFP 2022. doi:10.4204/EPTCS.360.6
   local PDF, slides
   abstract

   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.

8. Galois connecting call-by-value and call-by-name.
   Dylan McDermott and Alan Mycroft.
   FSCD 2022. doi:10.4230/LIPIcs.FSCD.2022.32
   local PDF, slides
   abstract

   We establish a general framework for reasoning about the relationship between call-by-value and call-by-name.

   In languages with side-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 side-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 these properties. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the call-by-value and call-by-name interpretations of types. We then identify properties of side-effects that imply these maps form a Galois connection. These properties hold for some side-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 side-effects including divergence and nondeterminism.

9. Sweedler theory of monads.
   Dylan McDermott, Exequiel Rivas, and Tarmo Uustalu.
   FoSSaCS 2022. doi:10.1007/978-3-030-99253-8_22
   local PDF, slides
   abstract

   Monad-comonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monad-comonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.

10. Abstract clones for abstract syntax.
    Nathanael Arkor and Dylan McDermott.
    FSCD 2021. doi:10.4230/LIPIcs.FSCD.2021.30
    local PDF
    abstract

    We give a formal treatment of simple type theories, such as the simply-typed λ-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 λ-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β- and η-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.

11. Degrading lists.
    Dylan McDermott, Maciej Piróg, and Tarmo Uustalu.
    PPDP 2020. doi:10.1145/3414080.3414084
    local PDF, slides, Haskell code
    abstract

    We discuss the relationship between monads and their known generalisation, graded monads, which are especially useful for modelling computational effects equipped with a form of sequential composition. Specifically, we ask if a graded monad can be extended to a monad, and when such a degrading is in some sense canonical. Our particular examples are the graded monads of lists and non-empty lists indexed by their lengths, which gives us a pretext to study the space of all (non-graded) monad structures on the list and non-empty list endofunctors. We show that, in both cases, there exist infinitely many monad structures. However, while there are at least two ways to complete the graded monad structure on length-indexed lists to a monad structure on the list endofunctor, such a completion for non-empty lists is unique.

12. Extended call-by-push-value: reasoning about effectful programs and evaluation order.
    Dylan McDermott and Alan Mycroft.
    ESOP 2019. doi:10.1007/978-3-030-17184-1_9
    Winner of EAPLS Best Paper Award.
    local PDF, slides
    abstract

    Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy's call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs.

    We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the source language.

    We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.

13. Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics.
    Ohad Kammar and Dylan McDermott.
    MFPS 2018. doi;10.1016/j.entcs.2018.11.012
    local PDF, slides
    abstract

    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.

14. Call-by-need effects via coeffects.
    Dylan McDermott and Alan Mycroft.
    Open Computer Science, 2018. doi:10.1515/comp-2018-0009
    local PDF
    abstract

    Effect systems refine types with information about the behaviour of programs. They have been used for many purposes, such as optimizing programs, determining resource usage, and finding bugs. So far, however, work on effect systems has largely concentrated on call-by-value languages.

    We consider the problem of designing an effect system for a lazy language. This is more challenging because it depends on the ability to locate the first use of each variable. Coeffect systems, which track contextual requirements of programs, provide a method of doing this. We describe how to track variable usage in a coeffect system that can be instantiated for different reduction strategies, including call-by-need. We then add effects to the result, allowing work that has been done on effect systems for call-by-value languages to be applied to lazy languages.

15. Project Snowflake: Non-blocking Safe Manual Memory Management in .NET.
    Matthew Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, and Jonathan Balkind.
    OOPSLA 2017. doi:10.1145/3141879
    local PDF
    abstract

    Garbage collection greatly improves programmer productivity and ensures memory safety. Manual memory management on the other hand often delivers better performance but is typically unsafe and can lead to system crashes or security vulnerabilities. We propose integrating safe manual memory management with garbage collection in the .NET runtime to get the best of both worlds. In our design, programmers can choose between allocating objects in the garbage collected heap or the manual heap. All existing applications run unmodified, and without any performance degradation, using the garbage collected heap. Our programming model for manual memory management is flexible: although objects in the manual heap can have a single owning pointer, we allow deallocation at any program point and concurrent sharing of these objects amongst all the threads in the program. Experimental results from our .NET CoreCLR implementation on real-world applications show substantial performance gains especially in multithreaded scenarios: up to 3x savings in peak working sets and 2x improvements in runtime.

PhD thesis

• Reasoning about effectful programs and evaluation order.
  Submitted October 2019.
  thesis

Some talks

There is also a more complete list.

1. Flexible presentations of graded monads.
   Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu.
   ICFP 2022, Ljubljana, Slovenia.
   slides
2. Galois connecting call-by-value and call-by-name.
   Dylan McDermott and Alan Mycroft.
   FSCD 2022, Haifa, Israel.
   slides
3. Canonical gradings of monads.
   Flavien Breuvart, Dylan McDermott, and Tarmo Uustalu.
   ACT 2022, Glasgow, UK.
   slides
4. Higher-order algebraic theories.
   Nathanael Arkor and Dylan McDermott.
   Partout seminar, LIX, Paris (online), May 2022.
   slides
5. Flexible presentations of graded monads.
   Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu.
   MSP101 seminar, University of Strathclyde (online), April 2022.
   slides
6. Sweedler theory of monads.
   Dylan McDermott, Exequiel Rivas, and Tarmo Uustalu.
   FoSSaCS 2022, Munich, Germany.
   slides
7. What makes a strong monad?
   Dylan McDermott and Tarmo Uustalu.
   MSFP 2022, Munich, Germany.
   slides