Tambara 设备公司推出新品

背景

本文源自 Hacker News 上关于 Tambara 模块的一篇深度技术文章。作者最初在尝试理解 Haskell 中的光学（optics，即透镜、棱镜、遍历等）时被范畴论所吸引。他对 van Laarhoven 的函子表示以及 Kmett 所使用的 Tambara 模块感到困惑。通过像玩俄罗斯方块一样反复运用 Yoneda 引理，作者逐渐取得了进展，并攻向越来越深奥的课题。在与牛津应用范畴论学校（Oxford Adjoint School in Applied Category Theory）的一群研究人员和学生合作后，他们解决了遍历光学（traversal optics）问题，并发表了一篇总结 profunctor 光学进展的论文。

光学处于半单子作用（monoidal actions） 与 Tambara 模块 的交汇处。光学与 Tambara 表示之间存在对偶性，这与数学家所谓的 Tannaka 重建（Tannakian reconstruction）有关——即从某个代数对象的所有表示中恢复该对象本身。

因此，Mateusz Stroiński 最近的文章《Module categories, internal bimodules and Tambara modules》引起了作者的极大兴趣。该文章指出 Tambara 模块可以被视为一种**双范畴（double category）**中的水平箭头，而这个双范畴同时也是一种 proarrow equipment。作者尝试在本文中勾勒该论文的内容，并用 Haskell 代码进行说明。

核心内容

核心口号

Tambara 模块之于单子函子（monoidal functors），如同 profunctor 之于函子。

这一口号揭示了 Tambara 模块与 profunctor 在结构上的类比关系。profunctors 是将函子范畴化（categorify）的关系，而 Tambara 模块则是将单子函子范畴化。

Tambara 模块的双范畴设置

传统上，我们可以在一个双范畴中研究 profunctors：0-单元格是范畴，水平1-单元格是 profunctors，垂直1-单元格是函子，2-单元格是自然变换。这个双范畴实际上是一种 proarrow equipment，它将函子与可表示 profunctor 以特定方式联系起来。

Stroiński 的工作表明，存在一个类似的构造：0-单元格是作用范畴（actegories），水平1-单元格是 Tambara 模块，垂直1-单元格是单子函子。为了形成2-单元格，我们首先需要能够沿着一对单子函子提升（或限制）一个 Tambara 模块。提升定义为：

Lift f g j (a, c) = j (f a, g c)

在 Haskell 中，这对应于 newtype Lift f g j a c = Lift (j (f a) (g c))。

一个2-单元格则是一个从 h 到 Lift f g j 的自然变换。即 type Cell f g h j = forall a c . h a c -> j (f a) (g c)。

单子函子的简化定义

作者使用了一个简化的严格单子函子定义，省略了单子范畴定义中的对象约束：

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

其中 alpha' 是 alpha 的逆。单子函子可以组合，组合结果仍是单子函子。

Tambara 模块的精确定义

Tambara 模块是一个与单子范畴的作用兼容的 profunctor。如果将一个 profunctor 解释为保留证明的关系（proof-relevant relation），那么 Tambara 模块具有以下性质：只要两个对象相关，它们乘以同一个对象后仍然相关。“乘法”在此指单子范畴的作用。形式上，一个 Tambara 模块是一个配备了变换 j a b -> j (m acta) (mact b) 的 profunctor，该变换在 a, b 处自然，在 m 处 dinatural，并且与单子结构良好交互。

在 Haskell 中，这对应一个类型类：

class (Actegory ten act, Profunctor j) => Tambara ten act j where
  leftAct :: j a b -> j (m `act` a) (m `act` b)

最简单的例子是 hom-functor（(->)），其 leftAct 就是 second（使用作用的双函子性质）。

Tambara 模块之间通过保持作用的自然变换作为态射构成一个范畴。通常的 profunctor 组合（使用 coend）在 Tambara 模块上同样成立。因此，Tambara 模块、coend 组合以及自然变换构成一个双范畴（bicategory），其中 actegories 是0-单元格，Tambara 模块是1-单元格。而作用在单一范畴内的**内 Tambara 模块（endo-Tambara modules）**则形成一个单子双范畴，以 profunctor 组合为张量积，以 hom-functor 为单位。

自由 Tambara 模块与光学

有一个明显的遗忘函子从 Tambara 模块双范畴到普通 profunctor 双范畴（它会遗忘作用）。该遗忘函子有一个左伴随，对于任意 profunctor j，它生成一个自由 Tambara 模块，由如下 coend 给出：

FreeTamb ten act j s t = ∫^{m} ∫^{x,y} hom(s, m `act` x) × j x y × hom(m `act` y, t)

在 Haskell 中，这建模为一个存在类型：

data FreeTamb ten act j s t = forall m x y. (MonoidalCategory ten, Actegory ten act) =>
  FreeTamb (s -> m `act` x) (j x y) (m `act` y -> t)

该类型确实是一个 Tambara 模块，其 leftAct 实现利用了作用的结合性。

光学可以定义为自由 Tambara 模块作用于一个可表示 profunctor 的结果。特别地，取 Rep a b x y = (x -> a, b -> y)，则：

type Optic ten s t a b = FreeTamb ten (Rep a b) s t

通过 Yoneda 归约，这等价于标准的光学形式：

data Optic ten act s t a b = forall m. Optic (s -> m `act` a) (m `act` b -> t)

这正是光学（如透镜、棱镜、遍历）的经典表示。

内化单子作用

一个单子作用被看作一个函子 act : ten → [C, C]，如果它有一个右伴随，则可以内化到范畴 C 中。该右伴随扮演了“内部 hom”的角色。在 Haskell 中，这对应一个类型类，其中定义了 uncurry 和 curry 操作，将作用与内部 hom 相互转换。

关键要点

• 核心类比：Tambara 模块之于单子函子，如同 profunctor 之于函子。这一视角统一了光学与范畴论中的表示理论。
• 双范畴框架：Tambara 模块可以自然地嵌入一个双范畴，其中水平箭头是 Tambara 模块，垂直箭头是单子函子。该双范畴是一种 proarrow equipment，使得单子函子与可表示 Tambara 模块之间建立联系。
• 自由构造：任何 profunctor 都可以通过自由 Tambara 模块构造获得一个 Tambara 模块，该构造由 coend 给出，在 Haskell 中表现为存在类型。
• 光学的范畴论定义：光学等价于自由 Tambara 模块作用于一个可表示 profunctor 的结果，经 Yoneda 归约后得到标准形式 Optic s t a b = ∃ m. (s → m ⊗ a, m ⊗ b → t)。
• 内化作用：若单子作用有右伴随，则可内化为内部