行动类别

行动类别
Actegories

原始链接: https://bartoszmilewski.com/2026/06/30/actegories/

$\mathbf M$

本摘要探讨了**作用范畴（actegories）**在函数式编程中的基础作用，特别是关于透镜（lenses）和棱镜（prisms）等光学结构的应用。作用范畴被定义为一种由**幺半范畴（monoidal category）**作用其上的范畴。幺半范畴是配备了结合律和单位元张量积的范畴。本文展示了如何利用 Haskell 中的类型类、约束和双函子（bifunctors）来建模这些结构。通过使用 `UndecidableSuperClasses` 等语言编译指示，可以编码维持必要相干性条件所需的结合子（associators）和单位元转换（unitors）。这种作用本身——可以被视为用幺半范畴的对象对范畴的对象进行“缩放”——被建模为双函子。除了定义单个作用范畴外，本文指出，共享同一幺半范畴的作用范畴本身也构成一个范畴，其中态射定义为幺半函子。最终，作用范畴为理解不同范畴如何相互作用提供了一个强有力的框架，形成了一种可以组织成双范畴（bicategory）的结构。文中通过笛卡尔积的自作用和各种 Haskell 实现等实例，说明了这些抽象的范畴论概念是如何转化为具体的函数式编程模式的。

Sorry.

原文

Previously: Kan Extensions in Double Categories.

In programming, actegories play a central role in optics: lenses, prisms, traversals, etc. To understand actegories, let’s start with the definition of a monoidal category.

Monoidal Category

A monoidal category $\mathbf M$ is a category equipped with a tensor product. A tensor product is a functor $\otimes \colon \mathbf M \times \mathbf M \to \mathbf M$ . We assume that this product is associative and unital– up to isomorphism. It means that there is an invertible associator:

$\alpha_{a, b, c} \colon (a \otimes b) \otimes c \to a \otimes (b \otimes c)$

natural in all three arguments. We also have a unit object $1$ and two (invertible, natural) unitors:

$\lambda_a \colon 1 \otimes a \to a$

$\rho_a \colon a \otimes 1 \to a$

To get a better feel for it, we can try to model a monoidal category in Haskell. We parameterize it by the type of the tensor product, ten, which we want to be a Bifunctor:

The standard way to define a subcategory of Hask is to restrict the types of objects by imposing a constraint. Such a restriction has a special kind, Constraint:

A common example of such a constraint is a typeclass. For instance Monoid will restrict the objects of the category to be monoids. (In principle, we should also restrict the type of arrows, here to monoid morphisms.)

We can specify the unit of a monoidal category as an associated type (parameterized by ten):

    type Unit ten :: Type

The unit should be an object of the category, so it should satisfy the constraint. We can encode this in our definition as a precondition: obj (Unit ten). This leads to a circularity, which we can overcome using the language pragma UndecidableSuperClasses:

Finally, we can add the associator and the unitors (and their inverses):

Notice the obj constraints in the type of these functions and the infix notation for the tensor.

Let’s work out a few examples. The simplest is the category of all types with a cartesian product as tensor.

We define Hask using an empty class, and we make all objects its instances:

Similarly, we can define a monoidal category with Either as the tensor product, or with Monoid as the object constraint.

Actegory

An actegory is a category that supports the action of a monoidal category. You may think of it as “multiplying” or “scaling” the objects of this category by objects of the monoidal category. The (left) action can be defined as a functor from the product category to $C$ :

$\triangleright \colon \mathbf M \times C \to C$

or, after currying, as a functor from $\mathbf M$ to the endofunctor category:

$\triangleright \colon \mathbf M \to [C, C]$

The coherency conditions are the invertible natural transformations that relate the action $\triangleright$ to the tensor product $\otimes$ and its unit $1$ :

$\alpha_{m n a} \colon (m \otimes n) \triangleright a \to m \triangleright (n \triangleright a)$

$\lambda_{a} \colon 1 \triangleright a \to a$

The action is functorial in both arguments, so our Haskell translation pegs it, for simplicity, as a Bifunctor. (A Profunctor action is also possible. Categorically, it would correspond to using $\mathbf M^{op}$ as the monoidal category.)

Another simplifying assumption is that the action uniquely identifies the tensor product, encoded here as the functional dependency act -> ten.

The simplest example of an actegory is the self action of the cartesian product. Here, the monoidal category acts on itself:

Monoidal Functors

Actegories that use the same monoidal category for their actions form a category. The morphisms in this category are (strict) monoidal functors. These are functors that map one action to another:

$f (m \triangleright_1 a) \cong m \triangleright _2 f a$

In Haskell, we can model them as:

In fact, actegories form a bicategory, with action-preserving natural transformations acting between monoidal functors.

Here’s an interesting example of a monoidal functor between non-trivial actegories:

Haskell code is available here.

行动类别 Actegories

Monoidal Category

Actegory

Monoidal Functors

Related

行动类别
Actegories