HaskellにおけるProfunctor Equipmentの実装

圏論は、具体的な実装に落とし込まれるまで、しばしば抽象的に感じられます。最近の探求において、Bartosz Milewskiは、洗練された圏論的構造である「Profunctor Equipment」をHaskell内でどのように実装するかを示しています。完全な実装には理想的には依存型言語が必要ですが、Haskellの型システムは、プログラマがコンパイラを通じてこれらの数学的な直感を検証できるような、トイ実装を提供するのに十分強力です。

Profunctor Equipmentの核となる構成要素

Profunctor EquipmentをHaskellで実装するには、圏論的概念を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: これらは自然変換として実装されます。Haskellでは、これは多相関数として表現されます：
type Cell f g h j = forall a c . h a c -> j (f a) (g c)

ここで、forall は全称量化子として機能し、変換がすべての型 a および c に対して成立することを保証します。

構成と単位

Equipmentを実装する際の主な課題の一つは、水平方向と垂直方向という異なる構成モードを扱うことです。

Horizontal Composition

水平方向の構成は、2つのセルを組み合わせて、合成された関手に作用する新しいセルを作成します。関手の合成に 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

垂直方向の構成はより複雑であり、プロファンクタの合成を必要とします。これは 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の法則を満たすためには、単位セルを両方の次元に対して定義する必要があります：

  • 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）のセルが備わっています。例えば、companionの単位と余単位は以下のように定義されます：

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など）が必要であると述べています。

この意見はコミュニティでも共鳴しており、一部では、このレベルの形式検証には依存型言語の方が適していると示唆されています。しかし、この「トイ」実装の有用性は変わりません。プログラマがHaskellのコンパイラを、圏論的構成の健全性をチェックするための手段として利用できるからです。

理論的な深さにもかかわらず、一部の実践者は、これらの構成と実用的なアプリケーションの間のギャップに注意をしています。これらの高レベルな圏論的equipmentを、開発者に具体的な利益をもたらす日常的なソフトウェアエンジニアリングのパターンへと翻訳することが、依然として課題として残っています。

Sources