解説: Directed Containers as Categoires

  • Posted on 2024-11-26
  • Last modified on 2025-01-18

\gdef\id{\mathop{\mathrm{id}}} \gdef\comp{\circ} \gdef\placeholder{{-}} \gdef\setsum{\operatorname{\raisebox{-0.2em}{$\Large\Sigma$}}} \gdef\setprod{\operatorname{\raisebox{-0.2em}{$\Large\Pi$}}} \gdef\Set{\mathrm{\mathbf{Set}}} \gdef\Cat{\mathrm{\mathbf{Cat}}} \gdef\Functors#1{\mathrm{\mathbf{Fun}}\left({#1}\right)} \gdef\Monads#1{\mathrm{\mathbf{Monads}}\left({#1}\right)} \gdef\Comonads#1{\mathrm{\mathbf{Comonads}}\left({#1}\right)} \gdef\CatC{\Cat^\sharp} \gdef\Ob{\mathop{\mathrm{Ob}}} \gdef\Mor{\mathop{\mathrm{Mor}}} \gdef\dom{\mathop{\mathrm{dom}}} \gdef\cod{\mathop{\mathrm{cod}}} \gdef\map{\mathop{\mathrm{map}}} \gdef\binprod{\mathbin{\Pi}} \gdef\bincoprod{\mathbin{\amalg}} \gdef\Id{\mathrm{Id}} \gdef\homset#1#2#3{{#1}\! \left\lbrack {#2}, {#3} \right\rbrack} \gdef\homsetl#1#2{{#1}\! \left\lbrack {#2} \right\rbrack} \gdef\asfunctor#1{\left. \llbracket {#1} \rrbracket^{c} \right.} \gdef\Cont{\mathrm{\mathbf{Cont}}} \gdef\Poly{\mathrm{\mathbf{Poly}}} \gdef\PolyFunctor#1{\mathrm{\mathbf{PFun}}\left({#1}\right)} \gdef\contcomp{\lhd} \gdef\inl{\operatorname{\mathtt{inl}}} \gdef\inr{\operatorname{\mathtt{inr}}} \gdef\divleft#1#2{\frac{{#1}, \_}{{#1}, {#2}}} \gdef\divright#1#2{\frac{\_, {#2}}{{#1}, {#2}}} \gdef\rootpos{o} \gdef\nextshape{\darr} \gdef\posplus{\oplus} \gdef\retroarr{\nrightarrow}

論文“Directed Containers as Categories”の解説をします。 本記事の内容は基本的にこの論文によります。

多項式関手 = コンテナ = 多項式

多項式関手

このブログでは既に何度か多項式関手というものを取り扱っています。 しかし、一貫した定義を使っていたわけではなく、また今回解説する論文とも微妙に定義が異なるため、 まずは定義から始めます。

この論文では「集合の圏\Set上の多項式関手」というものを扱っています。 まず、表現可能関手というものを定義します。

\Set上の表現可能関手
集合の圏\Setからそれ自身への関手R : \Set \to \Setが表現可能関手である \Leftrightarrow ある集合Aが存在して、Rは\Set(A,\placeholder)と表される関手と同型である

Haskell的に言うならば、関数の型(a -> b)へ引数の型を部分適用した(->) aというFunctorや、 適当な型Xを選べば(->) Xと同型になるようなFunctorが表現可能関手です。

instance Functor ((->) a) where
  fmap f g = f . g

例えば、以下のIntFunは(->) Intと同型なので表現可能関手です。

newtype IntFun b = MkIntFun (Int -> b)
instance Functor IntFun where
  fmap f (MkIntFun g) = MkIntFun (f . g)

また、「パラメータの型bをn個だけ集めた型」も表現可能関手です。 なぜなら、「『値の種類がちょうどn個の型』を引数にとる関数」と同型だからです。

data Vec2 b = V2 b b

instance Functor Vec2 where
  fmap f (V2 x1 x2) = V2 (f x1) (f x2)

-- Vec2は表現可能関手

vec2Rep :: (Bool -> b) -> Vec2 b
vec2Rep f = V2 (f False) (f True)

vec2Rep' :: Vec2 b -> (Bool -> b)
vec2Rep' (V2 x0 x1) =
  \x -> case x of
    False -> x0
    True -> x1

-- (ここでBoolはちょうど2種類の値をとる型の代表例として使っており、
-- 値が2種類ならばBool以外のどんな型でもよい)

-- Vec3 なども同様に表現可能関手
data Vec3 b = V3 b b b

特別なケースとして、Identityと Proxyはそれぞれ 「値が1つだけの型()」「値がない型Void」からの関数に同型なため、 表現可能関手です。

newtype Identity b = Identity b
identityRep :: (() -> b) -> Identity b
identityRep f = Identity (f ())

identityRep' :: Identity b -> (() -> b)
identityRep' (Identity x) = const x

data Proxy b = Proxy

proxyRep :: (Void -> b) -> Proxy b
proxyRep _ = Proxy

proxyRep' :: Proxy b -> (Void -> b)
proxyRep' Proxy = absurd

多項式関手は、表現可能関手を使って次のように定義されます。

\Set上の多項式関手
集合の圏\Setからそれ自身への関手F : \Set \to \Setが多項式関手である \Leftrightarrow Fは、いくつかの表現可能関手F_sの直和として表すことができる

これを表現可能関手の定義を使って言い換えると、\Set上の多項式関手Fとは、 ある集合Sと、Sで添字付けられた集合族P:S \to \Setを使って、 以下のように表現できる関手です。

\begin{align} F(\placeholder) &\cong \setsum (s \in S). \left( Ps \to \placeholder \right) \end{align}

特に、ある集合XにFを適用した集合FXは以下のように書くことができます。

\begin{equation} \begin{aligned} FX &\cong \setsum (s \in S). \left( Ps \to X \right) \\ &\cong \set{ (s,v) | s \in S, v \in Ps \to X } \end{aligned} \end{equation}

Haskellで例えるならば、多項式関手Fとは以下のようなFunctor（あるいは以下のようなものと同型なFunctor） のことです。

data F a =
  S0 (P0 -> a) | S1 (P1 -> a) | S2 (P2 -> a) | ...

数学的な定義におけるSの各要素s_0, s_1, \ldots \in Sが コンストラクタS0, S1, ...に、 各要素におけるPの値P(s_0), P(s_1), \ldotsが 各コンストラクタにおけるP0, P1, ...に対応します。

例えば、以下のようなデータ型Fooは多項式関手です。

data Foo a = Foo0 a | Foo1 a a | Foo2 a a

実際に、Fooと同型な関手Foo'を上記の形式で書くことができます。

type P0 = ()
type P1 = Bool
type P2 = Bool

data Foo' a =
    Foo0' (P0 -> a)
  | Foo1' (P1 -> a)
  | Foo2' (P2 -> a)

コンテナ

コンテナ（container）とは、（\Set上の）多項式関手から、 それを定義するために使われたデータだけを取り出したものです。

コンテナ
コンテナとは、集合Sと集合族P:S \to \Setの組(S,P)のことである。

任意のコンテナ(S,P)に対して、対応する\Set上の関手を(S,P)の解釈 (interpretation)と 呼んで、\asfunctor{S,P}と書くことにします。 逆に言えば、多項式関手とは、あるコンテナの解釈\asfunctor{S,P}と同型になっているような関手のことです。

\begin{align} {} & \asfunctor{S,P} : \Set \to \Set\\ {} & \asfunctor{S,P}X = \set{ (s,v) | s : S, v : Ps \to X }\\ {} & (\asfunctor{S,P}f)(s,v) = (s, f \comp v) \end{align}

多項式関手それぞれにコンテナが対応するだけでなく、 多項式関手の間の射である自然変換についても、 それに対応するコンテナの射（container morphism）を考えることができます。

コンテナの射
以下のような型の関数の組(t,q)を、コンテナ(S,P)から(S',P')へのコンテナの射とよぶ。 \begin{align} t &: S \to S' \\ q &: \setprod (s : S). P'(t s) \to P s \end{align}

コンテナの射(t,q)は、多項式関手の間の自然変換\asfunctor{t,q}として解釈できます。

\begin{align} \asfunctor{t,q}_{X} &: \asfunctor{S,P}X \to \asfunctor{S',P'}X \\ \asfunctor{t,q}_{X}(s,v) &= (t s, \lambda p'. v (q s p')) \end{align}

2つのコンテナ(S,P),(S',P')の間のコンテナの射をすべて集めた集合を\homset{\Cont}{(S,P)}{(S',P')}とすると、 その自然変換としての解釈を与える関数\asfunctor{-} : \homset{\Cont}{(S,P)}{(S',P')} \to \left( \asfunctor{S,P} \to \asfunctor{S',P'} \right) は全単射になっています。というより、そうなるようにコンテナの射とその解釈は定義されています。 これにより、各コンテナを対象、 射をコンテナの射としたコンテナの圏（category of containers）\Contを定めることができます。 コンテナの圏における恒等射と射の合成は、 解釈\asfunctor{\placeholder}がコンテナの圏から\Set上の自己関手の圏\Functors{\Set}への関手

\begin{CD} \Cont @>{\asfunctor{-}}>> \Functors{\Set} \end{CD}

として成り立つように、自然変換の恒等射と合成から逆算して定めることができます。

具体的には… 具体的には、コンテナの恒等射は \begin{equation} (\id_S, \lambda s. \id_{Ps}) : (S,P) \to (S,P) \end{equation} コンテナの射の合成は \begin{equation} \begin{aligned} (t,q) &: (S,P) \to (S',P') \\ (u,r) &: (S',P') \to (S'',P'') \\ (u,r)\comp (t,q) &= (u \comp t, \lambda s. q s \comp r (t s)) \end{aligned} \end{equation} という定義になります。

実質的に、コンテナは\Set上の多項式関手を集合で表現したもので、 更にコンテナの圏は関手圏\Functors{\Set}の部分圏の”多項式関手の圏”の表現になっています。

コンテナと多項式

\gdef\src{\operatorname{src}} \gdef\tgt{\operatorname{tgt}}

コンテナと同じく\Set上の多項式関手を記述する別の方法として、多項式（polynomial）を考えることができます。 （紛らわしい名前ですが、「関手」が付かない「多項式」とだけ言ったとき、それは多項式関手そのものではなく、 それを表現するデータをそう呼ぶ、という意味です。）

多項式
多項式とは、集合S、集合\bar{P}、そして関数\src : \bar{P} \to Sの三つ組(S,\bar{P},\src)のことである。

あるいは、多項式とは、図式

\begin{CD} S @<<{\src}< \bar{P} \end{CD}

のことだということもできます。

任意のコンテナ(S,P)は、 \bar{P}を全てのsに対するPsの直和をとったものとし、 \srcを「元々はどの集合Psに属していたか」を返す関数として、 多項式(S,\bar{P},\src)に変換することができます。

\begin{align} \bar{P} &= \setsum (s \in S). Ps \\ &= \set{ (s,p) | s \in S, p \in Ps } \\ \src (s,p) &= s \end{align}

逆に、任意の多項式((S,\bar{P},\src))は、 Psを「\src p == sとなるようなpを集めた\bar{P}の部分集合」 と定義することで、コンテナ(S,P)に変換することができます。

\begin{align} Ps = \set{ p | p \in \bar{P}, \src p = s } \end{align}

これらの変換は（同型なコンテナを同じとみなせば）互いに逆変換になっており、 コンテナと多項式は同じデータの異なる表現であることがわかります。

コンテナの射と同様に、多項式の射も考えることができます。 これは上記の変換と整合するようにコンテナの射の定義から計算することで得られますが、 やや煩雑なのでここでは省略します。

多項式コモナド = Directedコンテナ = 小さい圏

コンテナの合成

多項式関手は合成で閉じています。すなわち、2つのコンテナ(S,P)(T,Q) に対して、その解釈\asfunctor{S,P}と\asfunctor{T,Q}の合成関手は、 また何らかのコンテナの解釈（と同型）になっています。 そこで、合成関手に対応するコンテナを、(S,P)と(T,Q)の合成と呼ぶことにし、 (S,P)\contcomp (T,Q)と表記します。

コンテナの合成演算子\contcompは、具体的な計算方法を次のように与えることができます。

\begin{align} U &= \setsum (s : S). Ps \to T \\ &= \set{ (s,v) | s : S, v : Ps \to T } \\ R(s,v) &= \setsum (p : Ps). Q(vp) \end{align}

実際、これを関手として解釈すると、 Xに関して自然な同型\asfunctor{U,R}X \simeq \asfunctor{S,P}(\asfunctor{T,Q}X)が成り立つことが以下の計算によってわかります。

\begin{align} \asfunctor{U,R}X &= \setsum (u : U). (Ru \to X) \\ &= \setsum (s : S). \setsum (v : Ps \to T). \left( R(s,v) \to X \right) \\ &= \setsum (s : S). \setsum (v : Ps \to T). \left( \left( \setsum (p : Ps). Q(vp) \right) \to X \right) \\ &\simeq \setsum (s : S). \setsum (v : Ps \to T) \left( \setprod (p : Ps). \left( Q(vp) \to X \right) \right) \\ &\simeq \setsum (s : S). \setprod (p : Ps). \left( \setsum (t : T). Qt \to X \right) \\ &\simeq \setsum (s : S). Ps \to \left( \setsum (t : T). Qt \to X \right) \\ &= \asfunctor{S,P}( \asfunctor{T,Q}X ) \end{align}

コンテナの合成は、それが関手の合成という（同型を除いて）モノイドになっている演算と 一致するように定義されているため、それ自身コンテナの圏\Contにおけるモノイド積となることができます。 すなわち、\contcompは（同型を除いて）結合的で、モノイド単位(1, \mathrm{const} 1)をもちます。 ここで1は適当な一元集合1=\set{\star}です。

多項式コモナドから小さい圏まで

前項で見たように多項式関手は関手の合成で閉じているので、コモナドすなわち関手の合成に関するコモノイドも、 多項式関手だけからなる\Functors{\Set}の部分圏において考えられる概念です。 コモナド構造を追加で持つ多項式関手を多項式コモナド (polynomial comonad)と呼ぶことにしましょう。 コモナドとは、以下のような自然変換\mathrm{extract}, \mathrm{duplicate} を持つ関手Wであって、それらがコモナド則とよばれるいくつかの等式を満たすものでした。

\begin{CD} W @>{\mathrm{extract}}>> \mathrm{Id} \end{CD} \begin{CD} W @>{\mathrm{duplicate}}>> W\comp W \end{CD}

コンテナは多項式関手と対応し、コンテナの合成は多項式関手の合成と対応することから、 多項式関手が持つコモナド構造に対応する構造をコンテナに対しても考えることができます。 そのようなコモナドに対応する構造を持つコンテナは、 コンテナの射\mathrm{extract}'=(e_0, e_1),\mathrm{duplicate}'=(d_0, d_1)であって、 コモナド則と対応する等式を満たすようなものです。

\begin{CD} (S,P) @>{(e_0,e_1)}>> (1, \lambda p. 1) \end{CD} \begin{CD} (S,P) @>{(d_0,d_1)}>> (S,P) \contcomp (S,P) \end{CD}

コモナド則から課される条件を適用していくと、これらの射 (e_0, e_1), (d_0, d_1)は3つの関数(\rootpos_{(-)}, (- \nextshape -), (- \posplus_{(-)} -)) を使って以下のように書かれるものでなければならないことを示すことができます。

\begin{align} e_0 &= \lambda (\_ : S). \star \\ e_1 &= \lambda (s : S) (\_ : 1). \rootpos_s \\ d_0 &= \lambda (s : S). (s, \lambda (p : Ps). s \nextshape p) \\ d_1 &= \lambda (s : S) \left((p, p') : \setsum (p : Ps). P(s \nextshape p)\right). \\ &{\phantom{=}} \qquad p \posplus_{s} p' \end{align}

ただし、これらの関数の型は以下のようになっており、

\begin{equation} \begin{aligned} \rootpos_{(-)} &: \setprod (s : S). Ps \\ (- \nextshape -) &: \setprod (s : S). Ps \to S \\ (- \posplus_{(-)} -) &: \setprod (s : S). \setprod (p : Ps). P(s \nextshape p) \to Ps \end{aligned} \end{equation}

以下の等式を満たすものである必要があります。

\begin{equation} \begin{aligned} s \nextshape \rootpos &= s \\ s \nextshape (p \posplus_s p') &= \left(s \nextshape p\right) \nextshape p' \\ p \posplus_s o &= p \\ o \posplus_s p &= p \\ \left(p \posplus_s p' \right) \posplus_s p'' &= p \posplus_s \left(p' \posplus_{(s \nextshape p)} p'' \right) \end{aligned} \end{equation}

Directedコンテナを、この5つの等式を満たすような(\rootpos, \nextshape, \posplus)を備えたコンテナ(S,P) と定義します。すなわち、Directedコンテナは多項式コモナドをコンテナの言葉で記述したものです。

Directedコンテナ
Directedコンテナとは、以下の型を持つ5つ組(S,P,\rootpos, \nextshape, \posplus)であって、 (30)の等式すべてを満足するもののことである。 \begin{align*} S &: \Set\\ P &: S \to \Set\\ \rootpos_{(-)} &: \setprod (s : S). Ps \\ (- \nextshape -) &: \setprod (s : S). Ps \to S \\ (- \posplus_{(-)} -) &: \setprod (s : S). \setprod (p : Ps). P(s \nextshape p) \to Ps \end{align*}

ここで更に、Directedコンテナを記述するデータ(S,P,\rootpos, \nextshape, \posplus)を、 コンテナ(S,P)の代わりに多項式(S,\bar{P},\src)を用いるように書き換えます。 まず、機械的にPsを\bar{P}で置き換えます。

\begin{align} \rootpos_{(-)} &: S \to \bar{P} \\ (- \nextshape -) &: S \to \bar{P} \to S \\ (- \posplus_{(-)} -) &: S \to \bar{P} \to \bar{P} \to \bar{P} \end{align}

ただし、

  • これらの関数の戻り値をPsから置き換えた箇所については、 その戻り値に\srcを適用するとsであるという新しい等式を追加する
  • これらの関数の引数をPsから置き換えた箇所については、 “\srcがsでない引数に対しては定義されない”とする

ようにします。細かくみていくと、以下のようになります。

  • \rootpos_sは、\src (\rootpos_s) = sという等式が追加されます。

  • s \nextshape pについては、引数の条件から「s = \src pであるような引数についてのみ定義される」 という条件が付きますが、これは\tgt p = \src p \nextshape pである関数\tgt : \bar{P} \to Sを 代わりに用いれば、定義域を全域に保ったままにできます。

  • p \posplus_{s} p'については、引数の条件から

    • s = \src p
    • \tgt p = \src p'

    についてのみ定義された関数であり、更に

    • \src (p \posplus_{s} p') = s

    という等式が追加されます。(- \nextshape -)のときと同様に、 引数sを自動で補う新たな関数 p ; p' = p \posplus_{\src p} p' を用いれば、引数の条件ひとつは取り除くことができます。

これらをまとめると、多項式(S,\bar{P},\src)に変換したDirectedコンテナとして、Directed多項式が次のように定義できます。

  • Directed多項式は、2つの集合(S, \bar{P})および以下の4つの関数

    \begin{align} \src &: \bar{P} \to S\\ \tgt &: \bar{P} \to S\\ \rootpos_{(-)} &: S \to \bar{P}\\ (- ; -) &: \bar{P} \to \bar{P} \to \bar{P} \end{align}

    であって、以下の等式

    \begin{aligned} \src (\rootpos_s) &= s \\ \tgt (\rootpos_s) &= s \\ \src (p ; p') &= \src p \\ \tgt (p ; p') &= \tgt p' \\ p ; o &= p \\ o ; p &= p \\ \left(p ; p' \right) ; p'' &= p ; \left(p' ; p'' \right) \end{aligned}

    を満たすものである。ただし、p ; p'は部分関数であり、 \tgt p = \src p'を満たすとき、そのときに限り定義される。

これは、名前が違っているだけで、対象の集合をS、射の集合を\bar{P}とする小さい圏を定義するデータと全く同じになっています。

小さい圏
2つの集合\Ob(C),\Mor(C)と、 以下の型を持つ4つの関数の組(\src,\tgt,\id,(-;-))を併せたものであって、 更に(41)のすべての等式を満たすものを小さい圏とよぶ。 \begin{align} \src, \tgt &: \Mor(C) \to \Ob(C) \\ \id &: \Ob(C) \to \Mor(C) \\ (- ; -) &: \Mor(C) \to \Mor(C) \to \Mor(C) \end{align} ただし、(- ; -)は部分関数であり、(p ; p')は\tgt p = \src p'であるとき、 そのときに限り定義される。 \begin{align} \begin{aligned} \src (\id_s) &= s \\ \tgt (\id_s) &= s \\ \src (p ; p') &= \src p \\ \tgt (p ; p') &= \tgt p' \\ p ; \id &= p \\ \id ; p &= p \\ (p ; p') ; p'' &= p ; (p' ; p'') \end{aligned} \end{align}

これらのデータは、元々は多項式コモナドを記述するデータを、 1対1対応を守りながら変形させていったものでした。したがって、

多項式コモナド \cong Directedコンテナ \cong Directed多項式 = 小さい圏

という1対1の対応が得られたことになります。

コモナドと小さい圏は射についても対応しているか？

「コンテナとコンテナの射からなる圏」は、「多項式関手と自然変換の圏」と 多項式関手やコンテナの同型を無視すれば完全に一致するように作ることができました。1

さて、2つの\Set上のコモナドW, W'があったとき、 その間の自然変換\alpha : W \to W'であってコモナド演算\mathrm{extract}, \mathrm{duplicate}と両立するものを コモナド準同型 (comonad morphism)とよびます。 コモナドを対象、コモナド準同型を射とする圏を考えることもでき、コモナドの圏\Comonads{\Set}と呼ばれます。

一方で、2つの小さい圏C,C'の間の射として、最もふつうに考えられるのは関手F : C \to C'です。 小さい圏の圏\Catは、対象を小さい圏、射を関手とする圏として、圏論の教科書にも必ず登場するような一般的な圏です。

ここまで、多項式コモナドと小さい圏は1対1に対応することを見てきましたが、それは 「コモナドの圏を多項式コモナドに制限したもの」と「小さい圏の圏」との圏同値になっているのでしょうか？ 言い換えれば、「多項式コモナドの間のコモナド準同型」と「小さい圏の間の関手」の間に自然な1対1対応はあるのでしょうか？

これは「ない」というのが解答になります。「多項式コモナドの間のコモナド準同型」に対応するような小さい圏のあいだの射は、 関手とは異なるものになります。 その小さい圏の間の射は関手でなければ何であるのか、というのは後続の論文などで明らかにされており、“cofunctor”とよばれているもの (をわずかに一般化して、射の向きを合わせたもの)、あるいは”retrofunctor”とよばれているものであったことが言われています。

対応の具体例

多項式コモナドと小さい圏の対応を、具体的なコモナドや圏に対して考えた例を挙げてみます。 論文中では、これらの例のほかに、 「小さい圏の余積が多項式コモナドの余積(instance (Comonad f, Comonad g) => Comonad (Sum f g))に対応すること」や、 「小さい圏の積が多項式コモナドのテンソル積(instance (Comonad f, Comonad g) => Comonad (Day f g))に対応すること」 が挙げられています。

具体例1: Tracedコモナド

多項式コモナドであるTracedコモナドを考えます。2

newtype Traced m a = Traced { runTraced :: m -> a }
  deriving Functor

instance Monoid m => Comonad (Traced m) where
  extract (Traced t) = t mempty
  duplicate (Traced t) = Traced $ \m1 -> Traced $ \m2 -> t (m1 <> m2)

これは表現可能関手(->) mと同じものなので多項式です。 （多項式とはいくつかの表現可能関手の和なのでした。どんな表現可能関手も”1個の和”なので多項式です。） 型mを適当な集合Mとみなして、コンテナ(S,P)として表すならば、 Sとしては1つの元のみを持つ集合1 = \set{\star}とし、PはS=1の唯一の元を 集合Mに写す関数P(\star) = Mになります。

M上のモノイド構造(\mathrm{mempty}, \cdot)を使うと、Traced mに対応するdirectedコンテナ(S,P,\rootpos,\nextshape,\posplus) は次のようになります。

\begin{align} \rootpos_{\star} &= \mathrm{mempty} \\ \star \nextshape m &= \star \\ m_1 \posplus_{\star} m_2 &= m_1 \cdot m_2 \end{align}

これを更に小さい圏としてみなすと、これは

  • 対象の集合がS = 1 = \set{\star}、すなわち対象を1つだけ持つ
  • 射の集合が\bar{P} \cong Mで、対象が1つだけなのですべての射は対象\starから出てそこに戻る射である
  • 恒等射は\id_{\star} = \mathrm{mempty}、射の合成はm_1 ; m_2 = m_1 \cdot m_2である

となっています。これは、 モノイドを対象が1つだけの圏とみなす標準的な方法そのものです。

具体例2: NonEmptyリスト

また、NonEmptyリスト が持つComonadインスタンスも、対応するdirectedコンテナや小さい圏が何であるかを見てみましょう。

（NonEmptyのComondインスタンスを知らなかったという方は、過去記事でも軽く触れましたのでご参照ください。）

NonEmpty aは長さ1以上のリストのデータ型ですが、これを（きちんとしたHaskellではありませんが） 以下のように長さごとに異なるコンストラクタLnからなるデータ型とみなせば、多項式関手になっています。

data NonEmpty' a =
    L0 a
  | L1 a a
  | L2 a a a
  ...
  ...
  | Ln a a a ...... a -- (n+1)個
  ...
  ...

data NonEmpty'' a =
    L0 ({0} -> a)
  | L1 ({0,1} -> a)
  | L2 ({0,1,2} -> a)
  ...
  ...
  | Ln ({0,1,2,...,n} -> a)
  ...
  ...

これをコンテナ(S,P)として表現するならば、Sが自然数の集合S = \mathbb{N} = \set{0,1,\ldots}、 Pnを0からnまでのn+1個の自然数の集合\set{0,1,\ldots,n}とすることに相当します。

更に、NonEmptyのコモナドのインスタンスに対応するdirectedコンテナのデータ(\rootpos, \nextshape, \posplus)は 以下のようになります。

\begin{align} \rootpos_{n} &= 0 \\ n \nextshape p &= n - p \\ p \posplus_{n} p' &= p + p' \end{align}

これを小さい圏に変形すると、以下のような圏が得られます。

  • 対象の集合Sは自然数の集合\mathbb{N}

  • 射の集合\bar{P}は、自然数の組(n,p)∈\mathbb{N}^2であって、 n \ge pを満たすようなものの集合

    • \src (n,p) = n, \tgt (n,p) = n - pすなわち(n,p)はnから出てn-pに向かう射
    • 恒等射は\id_{n} = (n,0)
    • (n,p)と(n',p)の射の合成はn - p = n'であるときのみ定義され、(n,p) ; (n - p,p') = (n,p + p')

これは、\mathbb{N}に以下のような順序を与えて順序集合とみなし、それをさらに圏とみなしたものになっています。

\cdots \prec n+1 \prec n \prec \cdots \prec 2 \prec 1 \prec 0

  1. 圏同値といいます↩︎

  2. 論文中では、これをさらに自然数\mathbb{N}=\set{0,1,2,\ldots}が足し算に関してなすモノイドに特殊化したものが例として挙げられています。↩︎