Source-linked AI summary
Monads need not be endofunctors
Thosten Altenkirch, James Chapman, Tarmo Uustalu
TL;DR
Ordinary monads require endofunctors, leaving structures between different categories to be characterized. This paper develops relative monads and shows that arrows are a special case of them, while monadic constructions and extensions persist under stated conditions.
Problem
The paper asks how monadic structure and constructions can be generalized when the underlying functor maps between different categories rather than being an endofunctor.
Method
The paper develops relative monads, extends Kleisli and Eilenberg–Moore constructions, and uses left Kan extensions to obtain monoidal structure and extensions to monads.
Results
Arrows are relative monads on the Yoneda embedding, making them a special case of relative monads despite generalizing ordinary monads.
Takeaways & Limitations
Relative monads provide a framework for treating non-endofunctor structures, including arrows, with generalized monadic constructions.
Takeaways & Limitations
In general, no functor from the Kleisli category of a monad to that of its restriction can be defined because no canonical functor in the reverse direction is given.
Abstract
from arXiv · showhide
We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Under reasonable assumptions, relative monads are monoids in the functor category concerned and extend to monads, giving rise to a coreflection between relative monads and monads. Arrows are also an instance of relative monads.
1. Introduction
The paper introduces relative monads, a generalization for monad-like structures that are not endofunctors, motivated by finite-dimensional vector spaces and other programming examples. It develops their categorical constructions, monoidal characterization, extension to ordinary monads, and relationship with arrows.
- 1. Introduction: Relative monads generalize monads to monad-like entities whose underlying functors need not be endofunctors.This generalization arises naturally in dependently typed programming.
- 1. Introduction: Finite-dimensional vector spaces form a relative monad on the embedding Jf: Fin → Set, satisfying monad laws despite the category mismatch.The structure cannot generally extend to a monad on Set because arbitrary-set summation and decidable equality may be unavailable.
- 1. Introduction: The paper generalizes the Kleisli and Eilenberg–Moore constructions to relative monads and shows that they arise from relative adjunctions.These developments are presented in Section 2.
- 1. Introduction: Under suitable conditions, relative monads are monoids in [J, C], extend via LanJ to monads on C, and induce a coreflection between relative monads and monads.The induced skew-monoidal structure becomes properly monoidal under the stated well-behavedness conditions.
- 1. Introduction: Arrows are relative monads on the Yoneda embedding, making them a special case of relative monads despite generalizing ordinary monads.The paper also treats relative monad morphisms, monoid morphisms, and arrow morphisms categorically.
2. Relative monads and relative adjunctions
Relative monads generalize monads from endofunctors on one category to functors J between categories, with units and Kleisli extensions satisfying adapted monad laws. The section develops their morphisms, examples, relative adjunctions, and Kleisli and Eilenberg–Moore constructions, including the extension–restriction coreflection under suitable conditions.
- Relative monads: A relative monad on J:J→C assigns objects TX, units ηX:JX→TX, and Kleisli extensions k*:TX→TY satisfying right-unit, left-unit, and associativity laws.Its data and laws are those of an ordinary monad with the types adjusted to accommodate J.
- Relative monads: The relative monad laws induce a functor T:J→C, while η and Kleisli extension are natural; ordinary monads arise when J=C and J is the identity.A multiplication-based definition is not immediately available because T·T is generally ill-typed.
- Morphisms and relation to monads: Relative monads and their morphisms form a category RMon(J), and monads on C can restrict to relative monads on J with their morphisms.Under reasonable conditions, relative monads can conversely extend to monads via a right adjoint (−)♯, forming a coreflection with restriction (−)♭.
- Examples: Indexed containers form a relative monad because they are functors from the family category Fam A, equivalent to the slice category U/A, to U.The construction models closure under substitution, and interpretations preserve this structure as relative monad maps.
- Relative adjunctions: Any relative adjunction (L,R,φ) between J:J→C and D induces a relative monad with TX=R(LX), ηX=φ⁻¹(idLX), and k*=R(φ k).This connects relative adjunctions directly to the relative-monad structure.
- Kleisli and Eilenberg–Moore constructions: The splittings of a relative monad form a category, with the Kleisli construction initial and the Eilenberg–Moore construction terminal.For restricted ordinary monads, the ordinary Kleisli and Eilenberg–Moore categories, together with the corresponding functors, provide splittings of the relative monad.
3. Relative monads as skew-monoids in a skew-monoidal category
The section constructs a skew-monoidal structure on [J, C] using left Kan extension, allowing relative monads to be viewed as skew-monoids. When Lan_J exists, the resulting tensor, unit, and coherence maps satisfy the skew-monoidal axioms.
- Motivation: Relative monads on J ∈ J → C are represented as monoids in [J, C], but ordinary functor composition is unavailable there.The functor J provides a candidate unit, while composition of functors J → C is not directly defined.
- Construction: A left Kan extension along J converts functors J → C into functors C → C, enabling the composition-like tensor F ·_J G = Lan_J F · G.Lan_J is defined as the left adjoint of restriction when it exists, and it extends functors from J → D to C → D.
- Skew-monoidal structure: The induced unit and associativity maps are generally noninvertible, so [J, C] is skew-monoidal rather than properly monoidal.The maps λ, ρ, and α satisfy five coherence conditions, all of which are necessary in general.
- Theorem 3.1: If Lan_J ∈ [J, C] → [C, C] exists, then ([J, C], J, ·_J, λ, ρ, α) is a skew-monoidal category.Theorem 3.1 states that ·_J is functorial, λ, ρ, and α are natural, and the required coherence diagrams commute.
F ·J LanJJ
The section states the expression (e’) LanJ(F ·J (G ·J H)).
- It presents the expression (e’) LanJ(F ·J (G ·J H)).
J ·J LanJF · F ·J (LanJ(G ·J H))
The merged section records two compositional expressions involving relative left Kan extensions: (F ·J G) ·J LanJH and LanJ((F ·J G) ·J H).
- F ·J (LanJ(G ·J H)): The first displayed expression is (F ·J G) ·J LanJH.
- F ·J (LanJ(G ·J H)): The expression composes F ·J G with LanJH.
- F ·J (LanJ(G ·J H)): The first formula places LanJH after the composition F ·J G.
- F ·J (LanJ(G ·J H)): Together, the displayed formulas place LanJ in two different compositions involving F, G, and H.
- F ·J (LanJ(G ·J H)): The second displayed expression is LanJ((F ·J G) ·J H).
- F ·J (LanJ(G ·J H)): The second formula applies LanJ to the composite (F ·J G) ·J H.
F ·J (G ·J LanJH)
The section characterizes relative monads as skew-monoids in a skew-monoidal functor category and extends this equivalence to morphisms and alternative Eilenberg–Moore algebras. It also shows that the skew-monoidal structure need not be monoidal, with associativity sometimes failing to be invertible.
- Examples: The functor category [J, C] can be skew-monoidal without being monoidal: for J X = X × S, it is skew-monoidal but not monoidal.For J X = X + E, the associativity law α is not an isomorphism, and none of the canonical transformations ρ, λ, α has an inverse.
- Relative monads and skew-monoids: Relative monads on J are equivalent to skew-monoids in the skew-monoidal category ([J, C], J, ·J, λ, ρ, α).The correspondence converts Kleisli extension into multiplication and back, and is bijective.
- Relative monads and skew-monoids: This bijection extends to an isomorphism between the categories of relative monads on J and skew-monoids in ([J, C], J, ·J, λ, ρ, α).Morphisms preserve the corresponding units and multiplications or Kleisli extensions.
- Multiplication-based format: When LanJ exists, relative monads admit both Kleisli-extension and multiplication-based definitions.The multiplication format uses µ as a map from LanJ T (T X) to T X, while restriction from ordinary monads supplies the multiplication-based perspective.
- Eilenberg–Moore algebras: When LanJ exists, ordinary and alternative EM-algebras of a relative monad correspond bijectively, and their categories are isomorphic.An EM-algebra (X, χ) maps to (X, [χ]), while an alternative algebra (X, x) maps to (X, λg. x ◦ι g); the same correspondence applies to algebra maps.
4. Well-behaved relative monads
Well-behavedness makes the skew-monoidal structure on [J, C] properly monoidal, so relative monads become ordinary monoids and extend functorially to monads on C. These extensions form a coreflection, although the counit is generally an isomorphism only for finitary monads.
- Definition of well-behavedness: Well-behavedness requires Lan_J to exist and three canonical natural families to have isomorphic constituent maps, including full faithfulness and density of J.The third condition states that the nerve functor preserves left Kan extensions along J.
- Examples: For a type-theoretic universe closed under dependent products, the associated functor J_U is well-behaved, as are the finite-dimensional vector-space and lambda-calculus examples considered.The theorem establishes well-behavedness for J_U; the preceding passage states that J_f and J_U are well-behaved in the examples.
- Monoidal structure: For well-behaved J, ([J, C], J, ·_J, λ, ρ, α) is monoidal, and relative monads are exactly monoids in this monoidal category.The isomorphisms of the canonical maps ensure that the skew-monoidal unit and associativity laws become invertible.
- Extension to monads: Every relative monad on a well-behaved J extends to a monad on C, and relative monad morphisms extend functorially to monad morphisms.The extension is obtained at the level of monoids in [J, C] and [C, C].
- Coreflection: The extension and restriction constructions form a coreflection between RMon(J) and Mon(C), with the extension left adjoint to restriction and an isomorphic unit.This relationship arises because the adjunction Lan_J ⊣ −·J lifts from functors to relative monads.
- Limitation: The counit is generally not an isomorphism: for C = Set and J = Fin, its component is an isomorphism exactly when the monad is finitary.Consequently, monads on C and relative monads on J are generally not equivalent.
5. Arrows as a special case of relative monads
The section shows that arrows on J are precisely relative monads on the Yoneda embedding, reversing the usual view of arrows as generalizations of monads. This correspondence extends to an isomorphism of categories, identifies Freyd categories with Kleisli categories, and recovers arrows as monoids under suitable assumptions.
- Arrows and relative monads: Arrows on J are exactly relative monads on the Yoneda embedding Y, with explicit constructions in both directions forming a bijective correspondence.The correspondence maps an arrow by T Y X = R(X,Y) and reconstructs arrow composition from relative-monad extension.
- Morphisms: The bijection extends to an isomorphism between the categories of arrows on J and relative monads on Y.Arrow morphisms and relative-monad morphisms are obtained from one another by transposing components.
- Kleisli construction: The Freyd category of an arrow is the Kleisli category of its corresponding relative monad.This gives a relative-monad interpretation of the statement that Freyd is Kleisli for arrows.
- Monoidal structure: When J is small, the category [J, [Jop, Set]] is monoidal, and an arrow on J is a monoid in this category.This recovers the earlier characterization of arrows as monoids in the category of endoprofunctors on J.
6. Conclusions and further work
The paper presents relative monads as a natural generalization of monads beyond endofunctors, motivated by typed programming examples and encompassing arrows. It argues that ordinary monadic concepts can carry over to this setting while identifying implementation and further theoretical directions.
- Conclusions: Relative monads generalize monads to non-endofunctor settings and subsume arrows, reflecting the need for more precise type disciplines.The authors argue that their examples show monad-like entities that are not endofunctors are natural.
- Further work: Future work will compare relative monads with Spivey’s generalized monads, whose structures are monoids in [J, C] only when K has a left adjoint.The authors report that a fair amount of monad theory transfers to Spivey’s generalized monads and that, under this condition, they are equivalent to relative monads.
- Further work: The authors expect many concepts from ordinary monads to carry over and hope relative monads will support more reusable programming structures and programs.They note existing uses for syntax with reduction relations and for Haskell generalizations using constraint kinds and associated types.
- Implementation: A large part of the paper’s development has been formalized in the dependently typed programming language Agda.This formalization covers a large part, rather than the entirety, of the development.