目錄
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 混合變差作用與Coend
給定兩個作用 $\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}$ 上嘅混合變差作用。然後,hom-集會沿住呢啲作用擴展,並喺使用coend對 $\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}$ 嘅hom-集,其中對象係對 $\langle a, b \rangle$。
3. 雙範疇
雙範疇透過引入2-胞(1-胞之間嘅態射)來推廣範疇論,將嚴格相等放鬆為協調同構。
3.1 定義與例子
一個雙範疇 $\mathcal{B}$ 由0-胞(對象)、1-胞(對象之間嘅箭頭)同2-胞(1-胞之間嘅箭頭)組成。對於任何一對0-胞 $i, j$,1-胞形成一個hom-範疇 $\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. 多項式光學作為特例
複合光學理論包含咗多項式光學。作為多項式函子之間自然變換而產生嘅光學(喺先前工作中表示為「ommatidia」)被證明係一般雙範疇框架嘅一個特定實例。當作用嘅雙範疇係 $\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}$ 對共預層嘅作用,自然產生先前特設嘅多項式光學「ommatidia」。邏輯高潮係統一:曾被視為唔同物種(透鏡、棱鏡、多項式光學)嘅嘢,而家喺唔同參數下被揭示為同一個雙範疇屬嘅表現形式。
8. 優點、缺點與可行見解
優點:
- 統一能力: 該框架成功包含咗多項式光學同唔同嘅複合,減少咗概念碎片化。
- 數學穩健性: 利用已確立嘅概念,如雙範疇、profunctor同Kan擴展,確保理論嘅嚴謹性並連接到龐大嘅知識體系。
- 未來兼容性: 雙範疇表述本質上更具表達力,準備好為新興數據結構範式(例如涉及定向類型依賴或帶有效果上下文嘅範式)建模光學。
- 計算可處理性: 論文側重於存在性證明同萬有性質,但缺乏算法洞察。我哋點樣高效地計算呢啲複合光學?Coend/Kan擴展表述對於實現者來說可能過於抽象。對比Van Laarhoven透鏡嘅具體表示,佢哋直接映射到函數式代碼。
- 缺乏實證驗證: 冇案例研究或基準測試表明呢個通用框架解決咗簡單光學無法解決嘅實際軟件工程問題。冇咗呢點,對於實踐者來說,佢有成為「為解決問題而尋找問題嘅解決方案」嘅風險。
- 陡峭學習曲線: 雙範疇理論同coend演算嘅先備知識要求高,可能限制咗喺專門研究範疇語義學嘅學術圈以外嘅採用。
- 對於庫設計者: 將呢篇論文作為設計下一代光學庫(例如Haskell嘅`lens`或Scala嘅`monocle`)嘅北極星。開始原型設計一個「雙範疇後端」,佢可以優雅地回退到簡單光學處理常見情況,但能夠喺通用框架中原生處理多項式同複合光學。
- 對於研究者: 最緊迫嘅下一步係具體化。跟隨原始「透鏡」論文嘅路徑,佢催生咗實用庫。為複合光學開發一個規範嘅、具體嘅表示(可能係一個通用嘅van Laarhoven形式),並提供從雙範疇規範到呢個表示嘅編譯器。
- 對於實踐者: 關注呢條研究路線。雖然唔係立即可行,但佢指示咗高級函數式編程抽象嘅方向。而家理解佢,可以為設計穩健、未來兼容嘅系統提供競爭優勢。
9. 未來應用與研究方向
光學嘅雙範疇框架開闢咗幾個有前景嘅途徑:
- 依賴類型嘅光學: 喺依賴類型語言(如Agda或Idris)中為透鏡同棱鏡建模係有挑戰性嘅。基於profunctor嘅雙範疇方法可以為呢啲設定中嘅光學提供更清晰嘅語義基礎,喺度類型可以依賴於值。
- 與效應系統集成: 作用嘅雙範疇可以用帶有效果計算嘅範疇(例如單子雙範疇)來實例化。呢個可能導致一個統一嘅「帶效應光學」理論,用於處理存在I/O、狀態或非確定性時嘅存取同更新。
- 數據庫視圖更新: 數據庫中嘅視圖-更新問題係透鏡嘅經典應用。複合光學可以為涉及跨多個表連接(類似多項式結構)嘅更複雜視圖定義建模,並為更新傳播提供範疇論嘅正確性證明。
- 機器學習與可微分編程: 正如喺PyTorch或JAX等框架中所見,存取同操作複雜張量或計算圖嘅部分至關重要。一個通用光學框架可以為呢類操作提供一個原則性、可組合嘅API,而雙範疇則捕捉計算圖本身嘅結構。
- 雙向轉換: BX領域研究唔同數據表示之間嘅同步器,與透鏡有深厚聯繫。呢個複合光學框架可以為複雜模式上嘅多路同步提供新嘅、更可組合嘅構造。
10. 參考文獻
- Boisseau, G., & Gibbons, J. (2018). What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma. Proceedings of the ACM on Programming Languages.
- Riley, M. (2018). Categories of optics. arXiv preprint arXiv:1809.00738.
- Loregian, F. (2021). Coend Calculus. Cambridge University Press.
- Mac Lane, S. (1998). Categories for the Working Mathematician. Springer Science & Business Media.
- Pickering, M., Gibbons, J., & Wu, N. (2017). Profunctor optics: Modular data accessors. Art Science and Engineering of Programming.
- Spivak, D. I. (2020). Polynomial functors and ommatidia. arXiv preprint arXiv:2006.16941.
- Nester, C. (2022). Bicategories in Functional Programming: A Survey. Journal of Functional Programming.
- Abramsky, S., & Coecke, B. (2004). A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science.
- Haskell `lens` library documentation and source code. https://hackage.haskell.org/package/lens
- nLab community wiki. Entries on Bicategory, Profunctor, Optic. https://ncatlab.org/nlab/show/HomePage