Actegories 技术解析

背景

本文源自一篇关于范畴论在编程中应用的讨论，特别关注了“Actegories”这一概念。Actegories 在光学（Optics）领域——如 lenses、prisms、traversals 等——中扮演着核心角色。理解 Actegories 需要先从 monoidal category（幺半范畴）的定义出发。

核心内容

Monoidal Category（幺半范畴）

一个 monoidal category 是一个配备了张量积（tensor product）的范畴。张量积是一个函子：(\otimes: \mathcal{C} \times \mathcal{C} \to \mathcal{C})。我们假设这个乘积是结合的和有单位的——在 isomorphism 的意义上。这意味着存在一个可逆的结合子（associator）：

[ \alpha_{A,B,C}: (A \otimes B) \otimes C \to A \otimes (B \otimes C) ]

对所有三个参数自然。此外，我们还有一个单位对象 (I) 和两个（可逆、自然的）左/右单位子（unitors）：

[ \lambda_A: I \otimes A \to A,\quad \rho_A: A \otimes I \to A ]

为了更直观地理解，我们可以用 Haskell 建模一个 monoidal category。我们用张量积的类型 ten 来参数化，它应该是一个 Bifunctor：

class (Bifunctor ten) => MonoidalCategory ten where ...

标准做法是通过施加约束来限制 Hask 的子范畴 —— 这类约束具有特殊种类 Constraint：

class Bifunctor ten => MonoidalCategory (obj :: Type -> Constraint) ten where ...

一个常见的约束例子是 typeclass，例如 Monoid 将限制范畴的对象为 monoids（原则上还应限制箭头的类型为 monoid morphisms）。

我们可以将 monoidal category 的单位指定为关联类型（参数化为 ten）：

type Unit ten :: Type

单位应该是范畴的对象，因此它应满足约束 obj。这可以通过语言扩展 UndecidableSuperClasses 来编码为前置条件：

class (Bifunctor ten, obj (Unit ten)) => MonoidalCategory (obj :: Type -> Constraint) ten where
  type Unit ten :: Type
  alpha :: (obj a, obj b, obj c) => (a `ten` b) `ten` c -> a `ten` (b `ten` c)
  lambda :: (obj a) => (Unit ten) `ten` a -> a
  -- 以及其他逆等

注意这些函数类型中的 obj 约束以及张量积的中缀表示法。

我们来列举几个例子。最简单的例子是全体类型的范畴，以笛卡尔积作为张量积：

instance MonoidalCategory Hask (,) where
  type Unit (,) = ()
  alpha ((a, b), c) = (a, (b, c))
  lambda ((), a) = a
  rho (a, ()) = a

这里我们用空类定义 Hask，并让所有对象成为其实例：

class Hask a
instance Hask a

类似地，我们可以定义以 Either 为张量积的 monoidal category，或以 Monoid 为对象约束的 monoidal category。

Actegory（作用范畴）

Actegory 是一个支持某 monoidal category 作用的范畴。你可以把它想象成用 monoidal category 的对象来“乘以”或“缩放”这个范畴的对象。左作用可以定义为一个从乘积范畴 (\mathcal{M} \times \mathcal{C}) 到 (\mathcal{C}) 的函子：

[ \bullet: \mathcal{M} \otimes \mathcal{C} \to \mathcal{C} ]

或者经过 currying 后，成为从 (\mathcal{M}) 到自函子范畴 ([\mathcal{C}, \mathcal{C}]) 的函子。

一致性条件是涉及作用的可逆自然变换，将作用与张量积及其单位联系起来：

[ \alpha_{M,N,A}: (M \otimes N) \bullet A \to M \bullet (N \bullet A) ] [ \lambda_A: I \bullet A \to A ]

作用在两个参数上都是函子性的，因此为简单起见，我们的 Haskell 翻译将其定位为 Bifunctor（Profunctor 作用也是可能的，它对应将 (\mathcal{M}^{\text{op}}) 作为 monoidal category 使用）。

class (MonoidalCategory obj ten, Bifunctor act) => Actegory obj ten act | act -> ten where
  assoc :: (obj m, obj n) => (m `ten` n) `act` a -> m `act` (n `act` a)
  assoc' :: (obj m, obj n) => m `act` (n `act` a) -> (m `ten` n) `act` a
  unit :: Unit ten `act` a -> a
  unit' :: a -> Unit ten `act` a

另一个简化假设是作用唯一确定张量积，这里用函数依赖 act -> ten 编码。

最简单的 actegory 例子是笛卡尔积的自作用（self action），即 monoidal category 作用于自身：

instance Actegory Hask (,) (,) where
  assoc ((m, n), a) = (m, (n, a))
  assoc' (m, (n, a)) = ((m, n), a)
  unit ((), a) = a
  unit' a = ((), a)

Monoidal Functors（幺半函子）

使用相同 monoidal category 进行作用的 actegories 构成一个范畴。这个范畴中的态射是（严格的）monoidal functors，它们将一个作用映射到另一个作用：

[ F: (\mathcal{C}, \bullet) \to (\mathcal{D}, \bullet') ]

在 Haskell 中可以建模为：

class (Actegory obj ten act1, Actegory obj ten act2, Functor f) => MonFunctor obj ten act1 act2 f where
  as :: obj m => m `act2` f a -> f (m `act1` a)
  as' :: obj m => f (m `act1` a) -> m `act2` f a

实际上，actegories 构成一个 bicategory，而保持作用的自然变换充当 monoidal functors 之间的 2-态射。

下面是一个非平凡 actegories 之间的 monoidal functor 的有趣例子：

instance (Traversable f) => MonFunctor Monoid (,) (,) (,) f where
  as (m, fa) = fmap (m, ) fa
  as' = sequenceA

完整的 Haskell 代码可在此 GitHub 仓库 获取。

关键要点

• Monoidal category 是带有张量积（满足结合律和单位律，up to isomorphism）的范畴，它是构建 actegory 的基础。
• Actegory 是一个范畴，它被某个 monoidal category 以某种方式“作用” —— 作用是一个双函子，并满足与张量积和单位的一致性条件。
• 在编程中，actegory 的概念直接对应于 optics（如 lenses、prisms 等）的范畴论基础。
• Haskell 中通过 typeclass 和函数依赖可以很好地建模 monoidal category 和 actegory，利用 UndecidableSuperClasses 解决循环依赖。
• Monoidal functors 是保持作用的函子，作用范畴之间的态射，它们构成一个 bicategory。
• Traversable functor 给出了一个非平凡的 monoidal functor 实例，展示了 actegories 与数据结构遍历之间的联系。

意义与影响

Actegories 为 optics 提供了范畴论的形式化基础，使得 lenses、prisms、traversals 等概念的组合和推导有了严格的数学框架。在函数式编程（尤其是 Haskell）中，optics 已成为处理嵌套数据结构的核心工具，而 actegories 的理论将有助于设计更通用、更模块化的光学组合