在 Haskell 中實現 Profunctor Equipment

範疇論（Category theory）通常在落實到具體實作之前顯得非常抽象。在最近的一次探索中，Bartosz Milewski 展示了如何在 Haskell 中實作「Profunctor Equipment」——一種複雜的範疇結構。雖然理想情況下，完整的實作需要依賴型語言（dependently typed language），但 Haskell 的型別系統已足夠強大，足以提供一個玩具級（toy）實作，讓程式設計師能透過編譯器驗證這些數學直覺。

Profunctor Equipment 的核心組件

要在 Haskell 中實作 Profunctor Equipment，我們必須將範疇概念映射到 Haskell 的型別系統中。此實作專注於單一範疇（即 Haskell 的型別與函式範疇），並將範圍限制在內函子（endo-functors）與內型變函子（endo-profunctors）上。

0-Cells, 1-Cells, and 2-Cells

在此框架中，組件定義如下：

  • 0-Cells: Haskell 的型別與函式範疇。
  • Vertical 1-Cells: 使用標準函式庫中的 Functor 來實作。
  • Horizontal 1-Cells: 使用 Profunctor 來實作。
  • 2-Cells: 這些被實作為自然轉換（natural transformations）。在 Haskell 中，這表示為一個多型函式：
type Cell f g h j = forall a c . h a c -> j (f a) (g c)

這裡的 forall 作為全稱量詞（universal quantifier），確保該轉換對所有型別 a 與 c 皆成立。

組合與單位 (Composition and Units)

實作 equipment 的主要挑戰之一在於處理不同的組合模式：水平組合（horizontal）與垂直組合（vertical）。

水平組合 (Horizontal Composition)

水平組合將兩個 cell 結合，以建立一個作用於組合後函子的新 cell。使用 Compose newtype 進行函子組合，實作如下：

hcomp :: (Functor f, Functor f', Functor g, Functor g'
         , Profunctor h, Profunctor j, Profunctor k) =>
    Cell f g h j -> Cell f' g' j k 
                 -> Cell (Compose f' f) (Compose g' g) h k

hcomp fg_hj fg_jk hac = dimap getCompose Compose $ fg_jk (fg_hj hac)

垂直組合與共端 (Vertical Composition and Coends)

垂直組合更為複雜，需要型變函子（profunctor）的組合。這使用 coend 來實作，在 Haskell 中，coend 被表示為一個存在型（existential type）：

data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

在此定義中，x 是一個存在型——它不出現在參數列表中，這意味著它對外部世界是隱藏的，而這正是 coends 在範疇論中的行為方式。

單位 Cell (Unit Cells)

為了滿足 equipment 的定律，必須為兩個維度定義單位 cell：

  • Horizontal Unit: type Hunit p = Cell Identity Identity p p
  • Vertical Unit: type Vunit f a b = Cell f f (->) (->)

同伴與共伴 (Companions and Conjoints)

此實作進一步擴展到同伴（companions）與共伴（conjoints）的概念，這在本質上是 Haskell 生態系統中 Costar 與 Star 型別的同義詞。

  • Companion: 表示為 Costar f d c，定義為 newtype Costar f d c = Costar { runCostar :: f d -> c }。
  • Conjoint: 表示為 Star f d c，定義為 newtype Star f d c = Star { runStar :: d -> f c }。

這些組件配備了單位與反單位（unit and counit）cell。例如，同伴的單位與反單位定義如下：

type CompUnit f   = Cell Identity f (->) (Costar f)
compUnit :: Functor f => CompUnit f
compUnit h = Costar (fmap (h . runIdentity))

type CompCoUnit f = Cell f Identity (Costar f) (->)
compCoUnit (Costar h) = Identity . h

技術反思與限制

雖然這個 Haskell 實作在抽象數學與可執行程式碼之間提供了一個有價值的橋樑，但它也有其限制。作者指出，更完善的實作需要依賴型語言（例如 Lean），在那裡這些型別之間的關係可以被更嚴格地強制執行與證明。

這種觀點在社群中也得到了共鳴，有些人建議依賴型語言更適合進行這種程度的形式化驗證（formal verification）。然而，這個「玩具級」實作仍具備實用性：它允許程式設計師將 Haskell 編譯器作為範疇建構的健全性檢查工具。

儘管具有理論深度，一些實踐者指出，這些建構與實際應用之間仍存在差距。挑戰在於如何將這些高層次的範疇 equipment 轉換為日常軟體工程模式，從而為開發者提供切實的利益。

Sources