Dylan McDermott

Drafts

• Relative monadicity.
  Nathanael Arkor and Dylan McDermott.
  Last updated: May 2023.
  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 has a left j-relative adjoint and creates j-absolute colimits. We also establish a pasting law for relative adjunctions, and examine its interaction with relative monadicity. As a consequence, we derive necessary and sufficient conditions for the composite of a V-functor with a j-monadic V-functor to itself be j-monadic.

• The formal theory of relative monads.
  Nathanael Arkor and Dylan McDermott.
  Last updated: May 2023.
  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 qua trivial relative monad are stronger than the classical notions of algebra-object and opalgebra-object for a monad qua monad. 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.

• Galois connecting call-by-value and call-by-name. (Extended version.)
  Dylan McDermott and Alan Mycroft.
  Last updated: December 2023.
  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 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 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.

• 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

• Galois connecting call-by-value and call-by-name.
  Dylan McDermott and Alan Mycroft.
  Logical Methods in Computer Science. (To appear.)
  draft
  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 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 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.

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

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

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

• Canonical gradings of monads.
  Flavien Breuvart, Dylan McDermott, and Tarmo Uustalu.
  ACT 2022.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.

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

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

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

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

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

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

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

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

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

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