4
応用数学解説
文献あり

圏論から見るHaskellのApplicative

圏論,計算機科学,Haskell
707
0
$$\newcommand{CAb}[0]{\mathbf{Ab}} \newcommand{CArr}[0]{\mathbf{2}} \newcommand{CCat}[0]{\mathbf{Cat}} \newcommand{CCAT}[0]{\mathbf{CAT}} \newcommand{CEnr}[1]{{#1}\textrm{-}\mathbf{Cat}} \newcommand{CENR}[1]{{#1}\textrm{-}\mathbf{CAT}} \newcommand{CMod}[1]{{#1}\textrm{-}\mathbf{Mod}} \newcommand{CMonCat}[0]{\mathbf{MonCat}} \newcommand{cod}[0]{\mathop{\mathrm{cod}}} \newcommand{Colim}[0]{\mathop{\mathrm{Colim}}} \newcommand{Const}[0]{\mathop{\mathrm{Const}}} \newcommand{couni}[0]{\varepsilon} \newcommand{CQuiv}[0]{\mathbf{Quiv}} \newcommand{CSet}[0]{\mathbf{Set}} \newcommand{CUni}[0]{\mathbf{1}} \newcommand{defeq}[0]{\stackrel{\textrm{def}}{=}} \newcommand{defequiv}[0]{\stackrel{\textrm{def}}{\Leftrightarrow}} \newcommand{dom}[0]{\mathop{\mathrm{dom}}} \newcommand{fmap}[0]{\mathop{\texttt{fmap}}} \newcommand{Hom}[0]{\mathop{\mathrm{Hom}}} \newcommand{Id}[0]{\mathrm{Id}} \newcommand{id}[0]{\mathrm{id}} \newcommand{liftAA}[0]{\mathop{\texttt{liftA2}}} \newcommand{Lim}[0]{\mathop{\mathrm{Lim}}} \newcommand{Limind}[0]{\mathop{\underset{\longrightarrow}{\mathrm{Lim}}}\nolimits} \newcommand{Limproj}[0]{\mathop{\underset{\longleftarrow}{\mathrm{Lim}}}} \newcommand{lsimarrow}[0]{\xleftarrow{\sim}} \newcommand{Lsimarrow}[0]{\overset{\sim}{\Longleftarrow}} \newcommand{Mor}[0]{\mathop{\mathrm{Mor}}} \newcommand{Obj}[0]{\mathop{\mathrm{Obj}}} \newcommand{pure}[0]{\mathop{\texttt{pure}}} \newcommand{rsimarrow}[0]{\xrightarrow{\sim}} \newcommand{Rsimarrow}[0]{\overset{\sim}{\Longrightarrow}} \newcommand{SMC}[0]{\mathbf{SMC}} \newcommand{SMCC}[0]{\mathbf{SMCC}} \newcommand{To}[0]{\Rightarrow} \newcommand{uni}[0]{\eta} $$

はじめに

← 前回： 圏論から見るHaskellのFunctor

前回記事ではHaskellにおけるFunctorを圏論的な視点から考察してみました。今回はその流れでApplicativeについて見てみたいと思います。

Applicativeはモナドや(強自己)関手に比べてとても新しい概念であり、圏論の範囲でモナドや強自己関手について調べられたのが1960～70年代、モッジ (Eugenio Moggi) によってモナドがプログラミングに応用されたのが1990年前後であるのに比べて、Applicativeが論文に登場したのは2008年とつい最近のことでした (しかも圏論からではなくプログラミング論側、Functional Pearlとしての掲載でした)。

圏論から見た場合、applicative functorを端的に表現するとモノイダル強自己関手というように言い表せます。ApplicativeはFunctorが持っていなかったモノイダルな性質を獲得し、そのためにプログラミングにおいても有用な性質を獲得しています。

前回からの内容

定義の都合上、定義文中ではモノイダル圏上で定義していますが、本稿の内容の範囲ではカルテシアン閉圏に読み替えて構いません。カルテシアン閉圏については前回を参照してください。

対称モノイダル閉圏$(\mathcal{C},I,\otimes,\To)$の上の自己関手がテンソル強性 (tensorial strength) を持つとは、$A,B$について自然な$\mathcal{C}$の射の族$\tau_{A,B}:A\otimes TB\to T(A\otimes B)$が存在して、次の図式を可換にするものである：

\begin{xy} \xymatrix{ (A\otimes B)\otimes TC \ar[rr]^-{\tau_{A\otimes B,C}} \ar[d]_-{\wr} & & T((A\otimes B)\otimes C) \ar[d]^-{\wr} \\ A\otimes(B\otimes TC) \ar[r]^-{\id_A\otimes\tau_{B,C}} & A\otimes T(B\otimes C) \ar[r]^-{\tau_{A,B\otimes C}} & T(A\otimes(B\otimes C)) } \end{xy}
\begin{xy} \xymatrix@C=1em{ 1\otimes TA \ar[rr]^-{\tau_{1,A}} \ar[rd]_-{\sim} & & T(1\otimes A) \ar[ld]^-{\sim} \\ & TA } \end{xy}

$T$がテンソル強性を持つとき、$T$は$\mathcal{C}$上に$\fmap:(A\to B)\to TA\to TB$の実装を持ちます。逆に$T$が$\fmap$の実装を持つとき、$T$はテンソル強性を持ちます (前回参照)。

Applicativeの導入

関手と積の関係

関手とは圏と圏の間に定まる関係であり、圏の構造のみからその内容が決定されます。言い換えると、型の対応$A\mapsto TA$と射の対応$f\mapsto Tf$のみからその実装が定まります。つまり、関手と二項積の間には本質的には関連性がありません。モノイダル積の構造を保存する関手を(強)モノイダル関手と言います。

モノイダル圏$(\mathcal{C},I,\otimes),(\mathcal{C}',I',\otimes')$の間の強モノイダル関手とは、関手$F:\mathcal{C}\to\mathcal{C}'$であって、$A,B$について自然な同型

  • $\gamma_{A,B}:FA\otimes' FB\xrightarrow{\sim}F(A\otimes B)$
  • $e:I'\xrightarrow{\sim} FI$
    が存在し、次の図式を可換にするものである：
    \begin{xy} \xymatrix{ (FA\otimes' FB)\otimes' FC \ar[d]_-{\gamma_{A,B}\otimes'\id_{FC}} \ar[r]^-{\sim} & FA\otimes'(FB\otimes' FC) \ar[d]^-{\id_{FA}\otimes'\gamma_{B,C}} \\ F(A\otimes B)\otimes' FC \ar[d]_-{\gamma_{A\otimes B,C}} & FA\otimes' F(B\otimes C) \ar[d]^-{\gamma_{A,B\otimes C}} \\ F((A\otimes B)\otimes C) \ar[r]^-{\sim} & F(A\otimes(B\otimes C)) } \end{xy}
    \begin{xy} \xymatrix{ FA\otimes' I' \ar[r]^-{\id_{FA}\otimes' e} \ar[d]_-{\wr} & FA\otimes' FI \ar[d]^-{\gamma_{A,I}} & FI\otimes' FA \ar[d]_-{\gamma_{I,A}} & I'\otimes' FA \ar[l]_-{e\otimes'\id_{FA}} \ar[d]^-{\wr} \\ FA & F(A\otimes I) \ar[l]^-{\sim} & F(I\otimes A) \ar[r]^-{\sim} & FA } \end{xy}

同型$\gamma,e$がどちらも恒等射であるとき、$\mathcal{C}$はストリクトモノイダルという。

また、$\gamma,e$についての条件が同型ではなく射$\gamma_{A,B}:FA\otimes' FB\to F(A\otimes B)$, $e:I'\to FI$についてのみであった場合、$T$はlaxモノイダル、逆に$\gamma_{A,B}:F(A\otimes B)\to FA\otimes' FB$, $e:FI\to I'$についてのみであった場合、$T$はoplaxモノイダルという。

強モノイダルな関手はlaxかつoplaxなモノイダル関手ということができます。ストリクトモノイダルは強モノイダルのさらに特別な場合であるので、これもlaxでもoplaxでもあります。

カルテシアン積を持つ圏の間の関手は、積に関する普遍性から自然に$\gamma_{A,B}:F(A\times B)\to FA\times FB$を持ちます。またカルテシアン積の単位元は終対象$1$であるため、ここから$\gamma$と$e={!_1}$に関する可換図式が成り立ち、カルテシアン積を持つ圏の間の関手はすべてoplaxモノイダルになります。

モノイダル閉圏$(\mathcal{C},I,\otimes,\To)$上の自己関手$T:\mathcal{C}\to\mathcal{C}$がテンソル強性を持つlaxモノイダル関手であって、かつ次の図式を可換にするとき、$T$をapplicative functorという。

\begin{xy} \xymatrix{ (A\otimes TB)\otimes TC \ar[r]^-{\sim} \ar[d]_-{\tau_{A,B}\otimes\id} & A\otimes(TB\otimes TC) \ar[d]^-{\id\otimes\gamma_{B,C}} \\ T(A\otimes B)\otimes TC \ar[d]_-{\gamma_{A\otimes B,C}} & A\otimes T(B\otimes C) \ar[d]^-{\tau_{A,B\otimes C}} \\ T((A\otimes B)\otimes C) \ar[r]^-{\sim} & T(A\otimes(B\otimes C)) } \end{xy}

Applicativeクラス

HaskellにおけるApplicativeは、Functor $T$であって、$\circledast:T(A\to B)\to TA\to TB$または$\liftAA:(A\to B\to C)\to TA\to TB\to TC$、および$\pure:A\to TA$をメソッドに持つものです。
$\circledast$と$\liftAA$はどちらか片方が定義されているとき、もう片方を以下で定義します：
\begin{align} \_\circledast\_&=\liftAA(\id_{A\To B})\\ \liftAA&=\lambda fxy.\fmap(f)(x)\circledast y \end{align}

さらに、Applicative $T$は次の公理を満たすことが要請されます：

  • 単位元律 $\pure(\id_A)\circledast x=x$
  • 合成律 $((\pure(\circ)\circledast g)\circledast f)\circledast x=g\circledast(f\circledast x)$、ただし$\circ$は関数の合成を表す演算子$\_\circ\_:(B\to C)\to(A\to B)\to A\to C$のこと。
  • $\pure$の自然性 $\pure(f)\circledast\pure(x)=\pure(f(x))$
  • 交換律 $f\circledast\pure(x)=\pure(\lambda k.k(x))\circledast f$

$T$がApplicativeであるとき、$\tau_{A,B}:A\times TB\to T(A\times B)$が次で実装できます：
$$ \tau_{A,B}=\lambda(a,x).\pure(\lambda b.(a,b))\circledast x $$
この$\tau$の実装に対して、Applicativeの公理から
\begin{gather} \lambda t.\pure(\lambda((x,y),z).(x,(y,z)))\circledast(\tau_{A\times B,C}t) =\lambda((a,b),c').\tau_{A,B\times C}(a,\tau_{B,C}(b,c'))\\ \lambda(u,a).a=\lambda t.\pure(\lambda(u,a).a)\circledast(\tau_{1,A}t) \end{gather}
が成り立つため、$T$のテンソル強性が示されます。$\tau_{A,B}$を使うと$\fmap$の実装が
$$ \fmap(f)(x)=(\pure(\lambda(f',x').f'(x'))\circ\tau_{A\to B,A})(f,x) $$
とできるため、従ってApplicative $T$における$\fmap$の実装は
$$ \fmap=\lambda fx.\pure(f)\circledast x $$
となります。

また、$\gamma_{A,B}:TA\times TB\to T(A\times B)$の実装は
\begin{align} \gamma_{A,B} &= \lambda(x,y).\liftAA(\lambda ab.(a,b))xy\\ &= \lambda(x,y).\fmap(\lambda ab.(a,b))(x)\circledast y\\ &= \lambda(x,y).(\pure(\lambda ab.(a,b))\circledast x)\circledast y \end{align}
となり、ここから$(T,\gamma,\eta_1:1\to T1)$がlaxモノイダル関手をなすことが示されます。従ってApplicative $T$はapplicative functorをなすことがわかります。

様々な性質

定義に見られる通り、applicative functorはモノイダル関手的な性質と強自己関手的な性質を両方持ち合わせているため、それら単体の性質および相互的な性質の数々が絡み合っています。この節ではそれらをなるべく個別に考察してみたいと思います。

pure

$T:\mathcal{C}\to\mathcal{C}$はカルテシアン閉圏の上のapplicative functorとします。このとき、$\pure_A:A\to TA$は次で実装できます：
$$ A\xrightarrow{\id\times e}A\times T1 \xrightarrow{\tau_{A,1}}T(A\times 1) \xrightarrow{\sim}TA $$

このとき、$\pure$は自然変換、すなわち$f:A\to B$に対して$\pure_B\circ f=Tf\circ\pure_A$が成り立ちます。
\begin{xy} \xymatrix{ A \ar[r]^-{\pure_A} \ar[d]_-{f} & TA \ar[d]^-{Tf} \\ B \ar[r]^-{\pure_B} & TB } \end{xy}
加えて、以下の図式も併せて可換になります：
\begin{xy} \xymatrix@C=1.5em{ A\times B \ar@{=}[rr] \ar[d]_-{\pure_A\times\pure_B} & & A\times B \ar[d]^-{\pure_{A\times B}} & & 1 \ar@{=}[ld] \ar[rd]^(.6){\pure_1} \\ TA\times TB \ar[rr]^-{\gamma_{A,B}} & & T(A\times B) & 1 \ar[rr]^-{e} & & T1 } \end{xy}
モノイダル関手の間の自然変換が上図のようなコヒーレンス条件を満たすとき、$\pure:\Id\xrightarrow{\cdot}T$はモノイダル自然変換であると言います。

$\pure_1$が$e$と同一になることから、$\pure$を$e$の代用とすることができます (命題1)。

カルテシアン閉圏$\mathcal{C}$とその上の関手$T:\mathcal{C}\to\mathcal{C}$に対して、射の族$\gamma_{A,B}:TA\times TB\to T(A\times B)$と$\pure_A:A\to TA$が存在して各添字について自然であり、さらに次の図式が可換になるとする。
\begin{xy} \xymatrix{ (TA\times TB)\times TC \ar[d]_-{\wr} \ar[r]^-{\gamma_{A,B}\times\id} & T(A\times B)\times TC \ar[r]^-{\gamma_{A\times B,C}} & T((A\times B)\times C) \ar[d]^-{\wr} \\ TA\times(TB\times TC) \ar[r]^-{\id\times\gamma_{B,C}} & TA\times T(B\times C) \ar[r]^-{\gamma_{A,B\times C}} & T(A\times(B\times C)) } \end{xy}
\begin{xy} \xymatrix{ TA\times 1 \ar[r]^-{\id\times\pure_1} \ar[d]_-{\wr} & TA\times T1 \ar[d]^-{\gamma_{A,1}} & & A\times B \ar@{=}[r] \ar[d]_-{\pure_A\times\pure_B} & A\times B \ar[d]^-{\pure_{A\times B}} \\ TA & T(A\times 1) \ar[l]_-{\sim} & & TA\times TB \ar[r]^-{\gamma_{A,B}} & T(A\times B) } \end{xy}
このとき、$T$はapplicative functorである。

モノイダルな適用

カルテシアン閉圏の上のapplicative functor $T:\mathcal{C}\to\mathcal{C}$に対して、$\circledast_{A,B}:T(A\To B)\times TA\to TB$は次で実装できます：
$$ T(A\To B)\times TA\xrightarrow{\gamma_{A\To B,A}}T((A\To B)\times A)\xrightarrow{T\mathrm{ev}_{A,B}}TB $$
定義から、この射は$B$に対して自然となります。$\mathrm{ev}_{A,B}$同様、$A$に対しては自然ではないことに注意してください。

$\mathcal{C}$上での関数適用を表す射$\mathrm{comp}_{A,B,C}:(B\To C)\times(A\To B)\to(A\To C)$に対して、これをカリー化した射を$\fmap$で持ち上げた射を
$$ \fmap(\lambda g.g\circ\_):T(B\To C)\to T((A\To B)\To(A\To C)) $$
とおきます。このとき、次の2つの図式が可換になります：

  1. $((\pure(\circ)\circledast g)\circledast f)\circledast x= g\circledast(f\circledast x)$
    \begin{xy} \xymatrix@C=-1.0em{ (T(B\To C)\times T(A\To B))\times TA \ar[r]^-{\sim} \ar[d]_-{(\fmap(\lambda g.g\circ\_)\times\id)\times\id} & T(B\To C)\times(T(A\To B)\times TA) \ar[d]^-{\id\times\circledast_{A,B}} \\ (T((A\To B)\To(A\To C))\times T(A\To B))\times TA \ar[d]_-{\circledast_{A\To B,A\To C}\times\id} & T(B\To C)\times TB \ar[d]^-{\circledast_{B,C}} \\ T(A\To C)\times TA \ar[r]^-{\circledast_{A,C}} & TC } \end{xy}

  2. $\pure(f)\circledast\pure(x)=\pure(f(x))$
    \begin{xy} \xymatrix{ (A\To B)\times A \ar[r]^-{\mathrm{ev}_{A,B}} \ar[d]_-{\pure_{A\To B}\times\pure_A} & B \ar[d]^-{\pure_B} \\ T(A\To B)\times TA \ar[r]^-{\circledast_{A,B}} & TB } \end{xy}

既に前節で見た通り$\gamma$は$\pure$と$\circledast$から構成できるため、関手$T$と$\pure,\circledast$からapplicative functorを構成することができます。

交換律の導出

関数適用に対応する$\mathrm{ev}_{A,B}:(A\To B)\times A\to B$という射は、次のような普遍性を持っています。

カルテシアン閉圏$\mathcal{C}$の射$f:C\times A\to B$に対して、射$g:C\to(A\To B)$がただ1つ存在して、次の図式が可換となる：
\begin{xy} \xymatrix@C=3.5em{ C\times A \ar[rd]^(.5){f} \ar[d]_-{g\times\id} \\ (A\To B)\times A \ar[r]_-{\mathrm{ev}_{A,B}} & B } \end{xy}

一方で、$\circledast$にはこのような普遍性はありません。なので、例えば次のような図式の可換は明らかではなく、実際$\circledast$と$\pure$からapplicative functorを構成する際には公理として要請される必要があります。

  • $\pure(\id)\circledast x = x$
    \begin{xy} \xymatrix{ TA \ar[r]^-{j_A\times\id} \ar@{=}[d] & (A\To A)\times TA \ar[d]^-{\pure_{A\To A}\times\id} \\ TA & T(A\To A)\times TA \ar[l]_-{\circledast_{A,A}} } \end{xy}

  • $f\circledast\pure(x)=\pure(\lambda k.k(x))\circledast f$
    \begin{xy} \xymatrix@C=4em{ A\times T(A\To B) \ar[d]_-{(a\mapsto\lambda f.f(a))\times\id} \ar[r]^-{\sim} & T(A\To B)\times A \ar[d]^-{\id\times\pure_A} \\ ((A\To B)\To B)\times T(A\To B) \ar[d]_-{\pure_{(A\To B)\To B}\times\id} & T(A\To B)\times TA \ar[d]^-{\circledast_{A,B}} \\ T((A\To B)\To B)\times T(A\To B) \ar[r]^-{\circledast_{A\To B,B}} & TB } \end{xy}

Applicativeな型の例：ZipList

実際にApplicativeの例としてZipListを見てみましょう。ZipListはデータとしてはリストと同一ですが、Applicativeの実装にzippingを採用したものです。

Applicativeの実装は次のようになっています：

      pure x = ZipList (repeat x)
liftA2 f (ZipList xs) (ZipList ys) = ZipList (zipWith f xs ys)

この実装の本質であるzipWithの挙動ですが、リスト$[x_1,x_2,\dots]$と$[y_1,y_2,\dots]$に対して$[f(x_1,y_1),f(x_2,y_2),\dots]$を返します。リストの長さは2つのリストのうち短い方の長さになり、また評価順の関係で次のような評価が成り立ちます：

      >>> let f = undefined
>>> zipWith f [] undefined
[]

ZipListはおそらくMonadにできますが、およそ有用でないらしく2021年12月現在baseなどには実装されていません。

Applicativeの利用例：traverse

Applicativeの利用について、最たる例がおそらくtraverseでしょう。この関数はTraversableクラスのメソッドであり、Traversable tに対して次のような型を持ちます：
traverse :: Applicative f => (a -> f b) -> t a -> f (t b)

具体的な例としては、IOモナドとListに対して次のような関数が与えられます：
traverse :: (a -> IO b) -> [a] -> IO [b]

TraversableはMonadよりよほど特殊なことを要求しているためここでは扱いませんが、事実としてTraversableがApplicativeのサブクラスであることにより次のような関手がTraversableとして実装できます。以下で圏$\mathcal{C}$はカルテシアン閉かつすべての余積を持つものとします。

  • $X\mapsto 1+X$ (Maybe X型)
  • $X\mapsto A+X$ (Either A X型)
  • $X\mapsto A\times X$ ((A,X)型)
  • $X\mapsto \coprod_{i=1}^\infty X^i=1+X+X^2+X^3+\cdots$ (有限リスト)

これらがtraverseの実装を持つことは、applicative functorの性質 (特にlaxモノイダル関手としての性質)と余積の持つ普遍性によって示され、モナドであることは必要としていません。

Haskellのリストは無限リストも許容していますがTraversableの実装を持ちます。実装を読む限りはTraversableがFoldableを要求していることと関連していそうですが、これに関しては調べ切れていません。

おわりに

圏論側に立ってapplicative functorがどのようなものかを観察してきました。Applicativeはどうしてもちょっと弱いMonadというような立ち位置にいるため、いまひとつ立ち位置のつかめないクラスに今後もしばらくなりつづけることと思われます。しかし、圏論的視点に立てばそもそもApplicativeの本質はモナドっぽい部分には無く、モノイダル関手、あるいはモノイダル変換としての構造および機能にあることが分かります。
そもそもAppicativeという言葉自体が、内実がapplication＝適用にあることを主張していますから、その意味でもこれをモナドの腐ったのみたいに見る方がおかしいということですね (そんな見方してる人はいない)。

参考文献

[1]
Unknown, 取得中..., Mathlog, アクセス日: Thu Nov 23 2023
[2]
Conor McBride and Ross Paterson, Applicative Programing with Effects, Journal of Functional Programming, 2008, pp. 1–13
投稿日：2021年12月17日
更新日：2023年11月23日

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。

投稿者

merliborn
merliborn
31
4727
圏論や普遍代数に興味があります。現在の専門は型理論および圏論的意味論です。

コメント

他の人のコメント

コメントはありません。
読み込み中
merliborn
merliborn
圏論から見るHaskellのApplicative