圏論から見るHaskellのFunctor
はじめに
きっかけは、先月Qiitaに投稿された次の記事を読んだことです。
HaskellにおけるFunctor => Applicative => Monadの継承関係についての考察記事ですが、これを圏論的な視点からアプローチしなおしてみようと思ったのが当初の目的でした。しかし、そのために調べ物をしていると、あまりにも自分がapplicative functorについて知らないということが発覚してしまい、記事の内容を大幅に変更したものが本記事です。
本記事ではHaskellにおけるFunctorが果たす役割を圏論的なアプローチで考察します。 Haskell Advent Calendar に参加しようとも思っていたのですが、土壇場で熱を出して数日寝込んだために全ての予定が四散してしまいました。南無。
前提知識について
本記事では圏論の以下の知識を前提として書いていきます。これら基礎知識については Leinster や Mac Lane の対応する章、あるいは alg-dさんの圏論のページ などをご参照ください。
- 圏・関手・自然変換の定義 (Chap.1, [Leinster]、または ～I.§4, [MacLane])
また、例示部分に限ってはさらに追加の知識が必要になるかもしれません。ご了承ください。もしいい例をご存じの方がいましたらご教示いただけると幸いです。
圏論的に見たプログラミング
プログラムと型と圏論の関係
型 (の組)、あるいはその型の値の集合を対象として、変数の組$x_1:A_1,\dots,x_n:A_n$から型$B$の値を返すプログラム$\mathtt{f}$を$(A_1,\dots,A_n)$から$B$への射とみなすことで、これらの型とプログラムは圏をなします。これはものすごく端折って書いているので厳密にはいろいろ設定をちゃんとしないといけないのですが、今回は置いておきます。
型とプログラムで圏を構成できるということは、型付きのプログラムを行う体系は圏論によって抽象的な議論が可能ということになります。あるいは、圏論を通して意味論を様々考えることができるようにもなります。
カルテシアン積
一般的なラムダ計算の体系において、その圏論的意味論にはカルテシアン閉圏が採用されます。カルテシアン閉圏とは、終対象$1$とカルテシアン積$\times$が存在して、さらに任意の内部hom対象$A^B$を持つ圏のことです。
- 圏$\mathcal{C}$の終対象$1$とは、任意の対象$x\in\mathcal{C}$に対して$!_x:x\to 1$がただ1つ存在するような$\mathcal{C}$の対象$1$である。
- 圏$\mathcal{C}$がカルテシアン積を持つとは、任意の対象$x_1,x_2\in\mathcal{C}$に対して対象$x_1\times x_2$と各成分への射$x_1\xleftarrow{p_1}x_1\times x_2\xrightarrow{p_2}x_2$が存在して、任意の$x_1\xleftarrow{f_1}a\xrightarrow{f_2}x_2$に対して$f_i=p_i\circ u$を満たす$u:a\to x_1\times x_2$がただ1つ存在することである。
- 圏$\mathcal{C}$のカルテシアン積に対して、内部hom対象$A^B$とは、$\mathrm{ev}_{A,B}:A^B\times A\to B$を備えた対象$A^B$であって、任意の$f:C\times A\to B$に対して$f=\mathrm{ev}_{A,B}\circ(f'\times\id_A)$を満たす$f:C\to A^B$がただ1つ存在するものである。
- 終対象・カルテシアン積・内部hom対象を備えた圏をカルテシアン閉圏という。
Haskellで言うと、終対象とは$():()$、カルテシアン積とは$(a,b):(A,B)$のことです。また、内部hom対象とは関数型$A\To B$のことです。終対象とカルテシアン積を持つ圏は全ての有限積を持ちます。これはHaskellでは$()$, Solo , タプル$(a_1,\dots,a_n)$に相当します。
圏論的に見たFunctor
関手とFunctor
HaskellにおけるFunctorとは、型演算$A\mapsto TA$であって、メソッドとして$\texttt{fmap}:(\alpha\to\beta)\to T\alpha\to T\beta$を持つものをいいます。加えて、Functor $T$には次の2つの公理を満たすことが期待され、これは言語仕様などでは定められていませんが、実装によって公理は満たされているものとして扱われます。
- 単位元律 $\fmap(\id_A)=\id_{TA}$
- 合成律 $\fmap(g\circ f)=\fmap(g)\circ\fmap(f)$
$T$が関手であればこの2つの公理は当然に満たされますが、逆に$T$が関手であっても$\fmap$の実装が自然になされるわけではありません。これは、$f\mapsto Tf$という対応は一般に圏の内側で定義されているものではないからです。
可換モノイドとその間のモノイド準同型からなる圏$\mathbf{CMon}$について考える。このとき、ただ1つの元からなる自明なモノイドが終対象、通常の直積がカルテシアン積となり、$(f\odot g)(x)=f(x)\odot g(x)$によってモノイド準同型による可換モノイドが構成できるため、$\mathbf{CMon}$はカルテシアン閉圏である。
任意の可換モノイド$(M,e,\odot)$に対して、$TM=M\sqcup\{0\}$ ($0\notin M$) として、二項演算$\bar{\odot}:TM\times TM\to TM$を
\begin{align}
m\mathbin{\bar{\odot}}m'&=m\odot m'& &(m,m'\in M)\\
m\mathbin{\bar{\odot}}0&=m& &(m\in M)\\
0\mathbin{\bar{\odot}}0&= 0
\end{align}
で定める。
このとき、モノイド準同型$f:M\to N$に対して$Tf:TM\to TN$が
\begin{align}
(Tf)(m)&=f(m)& &(m\in M)\\
(Tf)(0)&=0
\end{align}
で定まり、$T(\id_M)=\id_{TM}$と$T(g\circ f)=Tg\circ Tf$を満たすため、$T$は関手である。
一方で、$f\mapsto Tf$は$(M\To N)\to (TM\To TN)$のモノイド準同型ではなく、従って$\mathbf{CMon}$は$\fmap$に相当する射を持たない。
強自己関手
$\fmap$を備えた自己関手は、強自己関手と呼ばれる特別な関手のクラスに一致します。歴史的には、これは豊穣圏におけるモナドの研究から生まれた概念であり、おそらく初出はA.コック (Andres Kock) の1970年の論文です。
対称モノイダル閉圏$(\mathcal{C},I,\otimes,\To)$上の強自己関手 (strong endofunctor) とは、$\mathcal{C}$から$\mathcal{C}$への関手で、かつ$\mathcal{C}$-豊穣関手でもあるものを言う。
すなわち、強自己関手$T=(T,\mathrm{st}^T):\mathcal{C}\to\mathcal{C}$とは関手$T:\mathcal{C}\to\mathcal{C}$と$\mathcal{C}$の射の族
$$
\mathrm{st}^T_{A,B}:(A\To B)\to(TA\To TB)
$$
の組であり、次の2つの図式を可換にするものである：
\begin{xy}
\xymatrix@C=5em{
(B\To C)\otimes(A\To B)
\ar[r]^-{\mathrm{st}^F_{B,C}\otimes\mathrm{st}^F_{A,B}}
\ar[d]_-{\circ_{A,B,C}}
& (TB\To TC)\otimes(TA\To TB)
\ar[d]^-{\circ_{TA,TB,TC}}
\\
(A\To C)
\ar[r]^-{\mathrm{st}^F_{A,C}}
& (TA\To TC)
}
\end{xy}
\begin{xy}
\xymatrix{
& I
\ar[ld]_-{j_A}
\ar[rd]^-{j_{TA}}
\\
(A\To A)
\ar[rr]^-{\mathrm{st}^F_{A,A}}
&
& (TA\To TA)
}
\end{xy}
ここで$\circ_{A,B,C}:(B\To C)\otimes(A\To B)\to(A\To C)$とは2つの関数の合成、$j_A:I\to (A\To A)$とは$(A\To A)$の要素としての$\id_A$を示す射である。
本稿ではモノイダル圏や豊穣圏については立ち入らず、強自己関手の定義も後半の言い換えたものを使います。カルテシアン閉圏は対称モノイダル閉圏の特別な場合なので、以降カルテシアン閉圏と直積で書きます。モノイダル圏や豊穣圏についてどうしても気になる場合は、以下の文献を参考にしてください。
- 対称モノイダル閉圏：[MacLane]のⅦ.1,Ⅶ.7、または §E.2, [ Riehl ]
- 豊穣圏：[MacLane]のⅠ.8、あるいは概観だけなら、 このセミナー動画 の最初5分を見るのが一番早いと思います。
圏$\mathcal{C}$上の強自己関手$T$、すなわち$\fmap$を備えた関手$T$について、次のような射が定義できます：
$$
\tau_{A,B}=\lambda(a,r).\fmap(\lambda b.(a,b))(r):A\times TB\to T(A\times B)
$$
$\tau_{A,B}$は$A,B$について自然で、さらに次のような図式を可換にします：
\begin{xy}
\xymatrix{
(A\times B)\times TC
\ar[rr]^-{\tau_{A\times B,C}}
\ar[d]_-{\wr}
&
& T((A\times B)\times C)
\ar[d]^-{\wr}
\\
A\times(B\times TC)
\ar[r]^-{\id_A\times\tau_{B,C}}
& A\times T(B\times C)
\ar[r]^-{\tau_{A,B\times C}}
& T(A\times(B\times C))
}
\end{xy}
\begin{xy}
\xymatrix@C=1em{
1\times TA
\ar[rr]^-{\tau_{1,A}}
\ar[rd]_-{\sim}
&
& T(1\times A)
\ar[ld]^-{\sim}
\\
& TA
}
\end{xy}
逆に、上記の2つの図式を可換にする$A,B$について自然な射の族$\tau_{A,B}:A\times TB\to T(A\times B)$を持つ性質のことを、テンソル強性 (tensorial strength) と言います。モノイダル圏$\mathcal{C}$がテンソル強性を持つとき、$\mathrm{st}^T_{A,B}:(A\To B)\to(TA\To TB)$を次の射のカリー化として定義できます：
$$
(A\To B)\times TA\xrightarrow{\tau_{A\To B,A}}T((A\To B)\times A)\xrightarrow{T\mathrm{ev}_{A,B}}TB
$$
ここで$\mathrm{ev}_{A,B}:(A\To B)\times A\to B$とは関数適用を表す射です。
実は、定義2の図式を可換にする$\mathrm{st}^T_{A,B}:(A\To B)\to(TA\To TB)$が定まっているとき、$T$は対象上の写像$A\mapsto TA$でありさえすれば$T$の関手性が示せます ($Tf=\fmap(f)$とすればよい)。このことから、$A\mapsto TA$の対応と$\fmap$の実装のみによってFunctorクラスを定められることがわかります。
Const
型はConst a b = Const { getConst :: a }で定義されるデータ型です。この型についての説明には
The 'Const' functor.
とあり、本質的には型aの値を保持したままFunctorのように振る舞う存在であると思われます。実際、Functorのインスタンスが次のように実装されます：
instance Functor (Const a) where
fmap _ (Const v) = Const v
Const aはaがMonoidのインスタンスである場合のみApplicativeのインスタンスが実装されています。これは、型Const a (x -> y)の値と型Const a xの値から型Const a yの値を作るに際して、それぞれの値が持つ型aのデータの処理を、Applicativeの公理を満たしながら行うことができないためと思われます。
Applicativeへの動機
強関手は関手よりは強い概念ですが、プログラミングの上では基礎的な構造以上の有用性を持っていません。具体的には$A\to TA$や$T(A\To B)\to TA\to TB$といった計算が、Functor上では保証されないためとても不便です。
そのような計算を保証した構造が、HaskellのApplicative、圏論ではapplicative functorと呼ばれるものです。