複合光學元件：一個用於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}$）本身就是一個豐富、可組合的實體。這與應用範疇論的趨勢一致，在該領域中，雙範疇和profunctor正成為開放系統和資源感知計算的通用語言，正如在範疇量子力學或Coq光學元件函式庫的工作中所見。

邏輯流程： 論證以手術般的精確度進行。首先，它確立了舊體制的限制：建立在么半作用上的簡單光學元件，在多項式函子和不同的光學元件組合上遇到了瓶頸。診斷結果是，么半範疇 $\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` 函式庫文件與原始碼。 https://hackage.haskell.org/package/lens
10. nLab 社群維基。關於雙範疇、Profunctor、光學元件的條目。 https://ncatlab.org/nlab/show/HomePage