タンバラ装備

home about bartosz milewski's programming cafe category theory, haskell, concurrency, c++ july 11, 2026 tambara equipment posted by bartosz milewski under category theory, double category | tags: category theory, double categories, optics, proarrow equipment, profunctors, tambara modules | [2] comments 私は当初、ハスケルのオプティクスを理解しようとして圏論に惹かれました。van laarhovenのファンクター表現とkmettのタンバラモジュールの使用に困惑していました。ヨネダの補題でテトリスをプレイすることで、より難解なトピックに次々と取り組むことができ、進歩することができました。応用圏論のオックスフォード・アジョイント・スクールでの研究者や学生のグループと共に、トラバーサルオプティクスの問題を解決し、プロファンクターオプティクスの進歩をまとめた論文を発表しました。オプティクスは、モノイダル作用とタンバラモジュールの交差点に位置します。オプティクスとタンバラ表現の間には双対性があります。これは、数学者がタンナキアン再構成と呼ぶものに関連しており、代数的なオブジェクトがその表現の全体から回復されるときです。 最近の記事「モジュールカテゴリ、内部二重モジュール、およびタンバラモジュール」が私の興味を引いたのも不思議ではありません。タンバラモジュールは、ダブルカテゴリの水平方向の矢印と見なすことができ、それはプロアロー装備でもあります。この記事の概要をスケッチし、ハスケルコードを使用してそれを説明しようと思います。 スローガンは、タンバラモジュールはモノイダルファンクターにとって、プロファンクターがファンクターにとってそうであるようなものであるということです。タンバラモジュールにとってダブルカテゴリ設定の主な利点は、それがリッチカテゴリに対してすぐに機能することです。 モノイダルファンクターの復習 簡単にするために、モノイダルカテゴリの定義からオブジェクト制約を省略した、厳密なモノイダルファンクターの簡略化されたバージョンを使用します。 class (actegory ten act1, actegory ten act2, functor f) => monfunctor ten act1 act2 f where alpha :: m `act2` f a -> f (m `act1` a) alpha' :: f (m `act1` a) -> m `act2` f a ここで、alpha' は alpha の逆です。 モノイダルファンクターは合成できます。 newtype monfuncompose f g a = monfuncompose { getmonfuncompose :: f (g a) } そして、その合成もまたモノイダルファンクターです。 instance ( actegory ten act1 , actegory ten act2 , actegory ten act3 , monfunctor ten act2 act3 f , monfunctor ten act1 act2 g ) => monfunctor ten act1 act3 (monfuncompose f g) where alpha mfga = let m3fga' = second getmonfuncompose mfga fmga = alpha @ten @act2 @act3 m3fga' fgma = fmap (alpha @ten @act1 @act2) fmga in monfuncompose fgma alpha' (monfuncompose fgma) = let fmga = fmap (alpha' @ten @act1 @act2) fgma mfga = alpha' @ten @act2 @act3 fmga in second monfuncompose mfga ハスケルの型チェッカーを助けるために、型アプリケーションを使用していることに注意してください。 タンバラモジュール タンバラモジュールは、モノイダルカテゴリのアクションと互換性のあるプロファンクターです。プロファンクターを証拠関連関係（proof-relevant relation）と解釈すると、タンバラモジュールは、2つのオブジェクトが関連付けられている場合、それらを同じオブジェクトで「乗算」しても関連性が保たれるという性質を持ちます。この場合、乗算とはモノイダルカテゴリのアクションを意味します。言い換えれば、タンバラモジュールは、以下の変換を備えたプロファンクターです。 that is natural in and , and dinatural in . アクションはモノイダル構造と良好に相互作用します。 (modulo some associators and unitors). これをハスケルで型クラスとして例示できます。 class (actegory ten act, profunctor j) => tambara ten act j where leftact :: j a b -> j (m `act` a) (m `act` b) actegoryの左アクションに集中することを選択しましたが、右アクション、または両方を定義するのは簡単です。簡単にするために、両方の引数に同じアクションを使用しています。完全な一般性では、2つの別々のアクテゴリを持つことになります。 タンバラモジュールの最も単純な例はホムファンクターです。 instance (actegory ten act) => tambara ten act (->) where leftact :: actegory ten act => (a -> b) -> m `act` a -> m `act` b leftact = second ここでは、アクションの bifunctoriality を使用しました。 タンバラモジュールはカテゴリを形成し、その中でアクションを保存する自然変換が射として機能します。coend を使用した通常のプロファンクター合成もタンバラモジュールで機能します。 data tamcompose p q d c where tamcompose :: p x c -> q d x -> tamcompose p q d c 合成の結果は再びタンバラモジュールになります。 instance (tambara ten act p, tambara ten act q) => tambara ten act (tamcompose p q) where leftact :: (tambara ten act p, tambara ten act q) => tamcompose p q a b -> tamcompose p q (m `act` a) (m `act` b) leftact (tamcompose pxc qdx) = tamcompose (leftact pxc) (leftact qdx) これらをまとめると、 bicategory があり、アクテゴリは 0-セル、coend 合成を持つタンバラモジュールは 1-セル、それらの間の自然変換は 2-セルとなります。さらに、エンドタンバラモジュール、つまり単一のカテゴリ内で動作するタンバラモジュールは、プロファンクター合成をテンソル積とし、ホムファンクターを単位とするモノイダル bicategory を形成します。 タンバラ装備 以前、カテゴリを 0-セル、プロファンクターを水平方向の矢印、ファンクターを垂直方向の矢印、自然変換を 2-セルとするダブルカテゴリを研究しました。このダブルカテゴリはプロアロー装備であり、ファンクターと表現可能なプロファンクターを特定の形で関連付けます。アクテゴリを 0-セル、タンバラモジュールを水平方向の 1-セル、モノイダルファンクターを垂直方向の 1-セルとする同様の構成が存在することが判明しました。 2-セルを形成するために、まずタンバラモジュールを2つのモノイダルファンクターのペアにリフト（または制限）できる必要があります。リフトを次のようなプロファンクターとして定義します。 or, using placeholders, . ハスケルでは、これを新しい型として定義します。 newtype lift f g j a c = lift (j (f a) (g c)) タンバラモジュールのリフトは、構造マップを合成として定義された構造を持つ、再びタンバラモジュールになります。 second arrow lifts the (invertible) monoidal functor structure map to : これはハスケルでも同様です。 instance ( actegory ten act1 , actegory ten act2 , monfunctor ten act1 act2 f , monfunctor ten act1 act2 g , tambara ten act2 j ) => tambara ten act1 (lift f g j) where leftact (lift j) = lift $ dimap alpha' alpha $ leftact @ten @act2 j act2 に対応する正しい左アクションを選択するために、型アプリケーションを使用しました。 2-セルは、からへの自然変換として定義されます。 type cell f g h j = forall a c . h a c -> j (f a) (g c) コンパニオンと共役は表現可能なプロファンクターであり、f がモノイダルファンクターである限り（恒等ファンクターは自明にモノイダルです）、自動的にタンバラモジュールになります。 type companion f d c = lift f identity (->) type conjoint f d c = lift identity f (->) コンパニオンと共役の単位セルと余単位セルは、定義が比較的容易です（リンクされたコードを参照）。 自由タンバラとオプティクス からへの明らかな忘却ファンクターがあります（アクションを忘れます）。このファンクターは左随伴を持ちます。任意のプロファンクターに対して、次の coend によって自由タンバラモジュールを生成します。 ハスケルでは、これを存在型データ型としてモデル化します。 data freetamb ten act j s t = forall m x y. (monoidalcategory ten, actegory ten act) => freetamb (s -> m `act` x) (j x y) (m `act` y -> t) 結果は実際にタンバラモジュールになります。 instance (actegory ten act, monoidalcategory ten, profunctor j) => tambara ten act (freetamb ten act j) where -- na -> (nm)c, jcd, (nm)d -> nb leftact (freetamb a_mc jcd md_b) = freetamb f jcd g where --f :: n `act` a -> (n `ten` m) `act` c f na = assoc' $ second a_mc na --g :: (n `ten` m) `act` d -> n `act` b g nm_d = second md_b $ assoc nm_d 偶然にも、オプティクスは表現可能なプロファンクターに作用する自由タンバラモジュールとして定義できます。実際、ヨネダ還元を適用すると、次のようになります。 ハスケルでは data rep a b x y = rep (x -> a) (b -> y) これにより、次のようになります。 type optic ten s t a b = freetamb ten (rep a b) s t これは、ヨネダ還元により、次のものと同型になります。 data optic ten act s t a b = forall m. optic (s -> m `act` a) (m `act` b -> t) モノイダルアクションの内部化 a m