复合光学：基于双范畴的Profunctor作用框架

目录

1. 引言

在范畴论与函数式编程的语境下，光学为访问和更新复杂数据结构的部分提供了一种原则性的方法。虽然简单光学在单一范畴框架内使用幺半作用进行操作，但涉及多项式函子的最新发展需要一个更一般的理论。本文引入了复合光学，它通过使用双范畴（特别是Profunctor双范畴Prof）对共预层范畴的作用来推广该框架。这种统一优雅地捕捉了由多项式函子间的自然变换所产生的光学。

2. 简单光学

光学的基础建立在作用范畴的概念之上。

2.1 作用范畴与幺半作用

一个作用范畴由一个幺半范畴 $\mathcal{M}$ 对一个范畴 $\mathcal{C}$ 的作用定义，记作 $\bullet : \mathcal{M} \times \mathcal{C} \to \mathcal{C}$。这可以看作一个幺半函子 $\bullet: \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$。

2.2 混合变差作用与余端

给定两个作用 $\bullet_1: \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$ 和 $\bullet_2: \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$，它们可以组合成积范畴 $\mathcal{C}^{\text{op}} \times \mathcal{D}$ 上的混合变差作用。然后，同态集沿着这些作用进行扩展，并在使用余端对 $\mathcal{M}$ 进行平均后，我们得到简单（混合）光学的标准形式：

$$O\langle a,b \rangle\langle s,t \rangle = \int^{m:\mathcal{M}} \mathcal{C}(s, m \bullet_1 a) \times \mathcal{D}(m \bullet_2 b, t)$$

这里，$\langle a, b \rangle$ 代表“焦点”，而 $\langle s, t \rangle$ 代表“整体对象”。

2.3 光学范畴

这些光学构成了一个范畴 $\mathbf{Opt}$ 的同态集，其中对象是序对 $\langle a, b \rangle$。

3. 双范畴

双范畴通过引入2-胞（1-胞之间的态射）来推广范畴论，将严格的等式放宽为相干同构。

3.1 定义与示例

一个双范畴 $\mathcal{B}$ 由0-胞（对象）、1-胞（对象间的箭头）和2-胞（1-胞间的箭头）组成。对于任意一对0-胞 $i, j$，1-胞构成一个同态范畴 $\mathcal{B}(i, j)$。典型的例子是 $\mathbf{Cat}$，其中范畴作为0-胞，函子作为1-胞，自然变换作为2-胞。

3.2 作为双范畴的幺半范畴

单对象双范畴等价于一个幺半范畴。其1-自同态胞是幺半范畴的对象，复合是张量积，2-胞是态射。

3.3 伪函子

双范畴之间的伪函子 $F: \mathcal{C} \to \mathcal{D}$ 是一种映射，它保持双范畴结构直到相干同构，而非严格保持。

4. 基于双范畴作用的复合光学

关键的洞见在于，复合光学中焦点与复合对象之间的关系，并非由单一的幺半作用（一个作用范畴）来描述最为恰当，而是由一个双范畴的作用来描述。本文提出使用双范畴 $\mathbf{Prof}$（由范畴、Profunctor和自然变换构成）对共预层范畴的作用来定义复合光学。这些光学的复合通过Kan扩张来解释，为其链式行为提供了坚实的范畴论基础。

5. 多项式光学作为特例

复合光学理论包含了多项式光学。作为多项式函子间自然变换出现的光学（在先前工作中表示为“小眼”）被证明是通用双范畴框架的一个特定实例。当作用双范畴是 $\mathbf{Prof}$ 且被作用的范畴是共预层范畴时，产生的复合光学恰好对应于这些基于多项式的光学。

6. 技术细节与数学框架

核心的技术贡献是使用双范畴作用和Kan扩张来表述光学。给定一个作用于范畴 $\mathcal{X}$ 的双范畴 $\mathcal{B}$，以及分组到范畴 $\mathcal{A}$ 和 $\mathcal{B}$ 中的焦点，一个复合光学可以定义为某个Kan扩张积分：

$$\text{Optic}((A,B), (S,T)) \cong \int^{M \in \mathcal{B}} \mathcal{X}(\alpha(M, A), S) \times \mathcal{X}(T, \beta(M, B))$$

其中 $\alpha$ 和 $\beta$ 表示双范畴的双侧作用。这通过将幺半范畴 $\mathcal{M}$ 替换为双范畴 $\mathcal{B}$，并将作用 $\bullet_1, \bullet_2$ 替换为更一般的、尊重双范畴结构的双函子 $\alpha, \beta$，从而推广了简单光学公式。

7. 分析框架：核心洞见与逻辑脉络

核心洞见： Milewski的论文不仅仅是对透镜理论的又一次渐进式调整；它是对整个可组合数据访问器的范畴操作系统的战略性升级。从幺半作用范畴到双范畴作用的转变，类似于从单线程进程推广到并发、网络化的系统。其核心观点是，现代数据结构的真正复杂性——例如嵌套容器、依赖类型或图模式——本质上是多维的，需要一个框架，其中“上下文”（$\mathcal{M}$ 或 $\mathcal{B}$）本身就是一个丰富的、可组合的实体。这与应用范畴论的趋势一致，在范畴量子力学或Coq光学库的工作中可以看到，双范畴和Profunctor正成为开放系统和资源感知计算的通用语言。

逻辑脉络： 论证过程如外科手术般精确。首先，它确立了旧范式的局限性：基于幺半作用构建的简单光学，在遇到多项式函子和不同的光学组合时遇到了瓶颈。诊断结果是幺半范畴 $\mathcal{M}$ 过于“扁平”，无法对复合焦点的独立、交互的上下文进行建模。解决方案是双范畴，它提供了必要的二维结构来追踪这些交互。概念验证是优雅的：证明Profunctor双范畴 $\mathbf{Prof}$ 对共预层的作用，自然地产生了先前临时定义的、多项式光学的“小眼”。逻辑高潮在于统一：曾经被视为不同物种（透镜、棱镜、多项式光学）的东西，现在被揭示为同一双范畴属在不同参数下的表现形式。

8. 优势、缺陷与可操作的见解

优势：

1. 统一能力： 该框架成功地包含了多项式光学和不同的组合，减少了概念上的碎片化。
2. 数学稳健性： 利用双范畴、Profunctor和Kan扩张等成熟概念，确保了理论上的可靠性，并与大量知识体系建立了联系。
3. 面向未来： 双范畴表述本质上更具表达力，已准备好为新兴数据结构范式（例如涉及定向类型依赖或带效应上下文的结构）的光学建模。

1. 计算可处理性： 论文侧重于存在性证明和泛性质，但对算法见解涉及较少。我们如何高效地计算这些复合光学？余端/Kan扩张的表述对于实现者来说可能过于抽象。这与Van Laarhoven透镜的具体表示形成对比，后者可以直接映射到函数式代码。
2. 缺乏实证验证： 没有案例研究或基准测试表明，这个通用框架解决了简单光学无法解决的实际软件工程问题。如果没有这一点，对于实践者来说，它可能只是一个寻找问题的解决方案。
3. 陡峭的学习曲线： 双范畴理论和余端演算的先验知识要求很高，可能限制了在专门研究范畴语义学的学术圈之外的采用。

1. 对于库设计者： 将本文作为设计下一代光学库（例如Haskell的`lens`或Scala的`monocle`）的北极星。开始原型设计一个“双范畴后端”，对于常见情况可以优雅地回退到简单光学，但在通用框架内可以原生处理多项式和复合光学。
2. 对于研究者： 最紧迫的下一步是具体化。遵循原始“透镜”论文的路径，该论文催生了实用的库。为复合光学开发一个规范的、具体的表示（或许是一种广义的van Laarhoven形式），并提供从双范畴规范到该表示的编译器。
3. 对于实践者： 关注这一研究方向。虽然不能立即付诸实践，但它指明了高级函数式编程抽象的方向。现在就理解它，可以为设计健壮、面向未来的系统提供竞争优势。

9. 未来应用与研究方向

光学的双范畴框架开辟了几个有前景的途径：

1. 依赖类型的光学： 在依赖类型语言（如Agda或Idris）中为透镜和棱镜建模具有挑战性。基于Profunctor的双范畴方法可以为这些设置中的光学提供更清晰的语义基础，其中类型可以依赖于值。
2. 与效应系统集成： 作用双范畴可以用带效应的计算范畴（例如，单子双范畴）来实例化。这可能导致一个统一的“带效应光学”理论，用于处理存在I/O、状态或非确定性时的访问和更新。
3. 数据库视图更新： 数据库中的视图更新问题是透镜的经典应用。复合光学可以建模涉及跨多个表的连接（类似多项式的结构）的更复杂视图定义，并为更新传播提供范畴论的正确性证明。
4. 机器学习与可微编程： 正如在PyTorch或JAX等框架中所见，访问和操作复杂张量或计算图的部分至关重要。一个通用的光学框架可以为此类操作提供一个原则性的、可组合的API，其中双范畴捕获计算图本身的结构。
5. 双向变换： BX领域研究不同数据表示之间的同步器，与透镜有深刻联系。这个复合光学框架可以为复杂模式上的多路同步提供新的、更具可组合性的构造。

10. 参考文献

1. Boisseau, G., & Gibbons, J. (2018). What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma. Proceedings of the ACM on Programming Languages.
2. Riley, M. (2018). Categories of optics. arXiv preprint arXiv:1809.00738.
3. Loregian, F. (2021). Coend Calculus. Cambridge University Press.
4. Mac Lane, S. (1998). Categories for the Working Mathematician. Springer Science & Business Media.
5. Pickering, M., Gibbons, J., & Wu, N. (2017). Profunctor optics: Modular data accessors. Art Science and Engineering of Programming.
6. Spivak, D. I. (2020). Polynomial functors and ommatidia. arXiv preprint arXiv:2006.16941.
7. Nester, C. (2022). Bicategories in Functional Programming: A Survey. Journal of Functional Programming.
8. Abramsky, S., & Coecke, B. (2004). A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science.
9. Haskell `lens` library documentation and source code. https://hackage.haskell.org/package/lens
10. nLab community wiki. Entries on Bicategory, Profunctor, Optic. https://ncatlab.org/nlab/show/HomePage