在 Haskell 中实现 Profunctor Equipment

范畴论（Category theory）通常在落地到具体的实现之前显得非常抽象。在最近的一次探索中，Bartosz Milewski 展示了如何在 Haskell 中实现“Profunctor Equipment”——一种复杂的范畴结构。虽然理想情况下完整的实现需要一种依赖类型语言（dependently typed language），但 Haskell 的类型系统足够强大，可以提供一个玩具级实现，让程序员能够通过编译器验证这些数学直觉。

The Core Components of 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 作为全称量词，确保变换对所有类型 a 和 c 都成立。

Composition and Units

实现 equipment 的主要挑战之一是处理不同的复合方式：水平复合（horizontal）和垂直复合（both vertical and horizontal）。

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 中，它被表示为一个存在量化类型（existential type）：

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

在这个定义中，x 是一个存在量化类型——它不出现在参数列表中，这意味着它对外部世界是隐藏的，这正是 coend 在范畴论中表现出的行为。

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

该实现进一步扩展到了 companion 和 conjoint 的概念，它们本质上是 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 和 counit cell。例如，companion 的 unit 和 counit 定义如下：

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

Technical Reflections and Limitations

虽然这个 Haskell 实现为抽象数学与可执行代码之间搭建了一搭建了一座桥梁，但它也有局限性。作者指出，更完善的的实现需要一种依赖类型语言（例如 Lean），在那里这些类型之间的关系可以得到更严格的强制执行和证明。

这种观点在社区中也得到了共鸣，一些人建议依赖类型语言更适合这种级别的形式化验证。然而，这个“玩具”级实现仍然具有实用性：它允许程序员使用 Haskell 编译器作为范畴构造的合理性检查（sanity check）。

尽管具有理论深度，一些从业者指出，这些构造与实际应用之间存在差距。挑战仍然在于如何将这些高层级的范畴 equipment 转化为能够为开发者提供切实的利益的日常软件工程模式。

Sources