この記事は Category Theory Advent Calendar 2018 7日目 かつ Haskell (その2) Advent Calendar 2018 7日目の記事です。

Category Theory Advent Calendar 2018の6日目はcorollary2525さんの「随伴は　あらゆるところに　現れる」、8日目は空席、9日目はt_uemura669101さんの「トポスと高階論理」です。

Haskell (その2) Advent Calendar 2018の6日目は空席、8日目はtakoeight0821さんの「Type defaultingについての初級的な解説」です。

この記事はどういう記事か

圏論の方から来た人向け：

デカルト積やテンソル積の一般化である「モノイド積」の話と、「内部ホム」の話をします。文献によっては内部ホムはモノイド積の右随伴として導入されますが、ここではモノイド構造を仮定せずに内部ホムの定式化（閉圏）をします。

Haskellの方から来た人向け：

この記事ではHaskellにおけるアプリカティブ関手の使い方は解説しません。Haskellの方から来た読者はすでにアプリカティブ関手をある程度知っており、圏論的な話にﾁｮｯﾄ興味がある、と仮定します。

これを読めば、「モナドは自己関手の圏におけるモノイド対象だよ、何か問題でも？」と同じノリで「アプリカティブ関手はモノイド圏における強laxモノイド関手だよ、何か問題でも？」と言って他人を煙に巻くことができます。

はじめに

Haskellにはアプリカティブ関手という概念があります。Haskellではこれは「モナドと関手の中間の概念」とされていますが、圏論的にはどういう概念に相当するのでしょうか。

-- Functorとは、 fmap が定義された型のことである
class Functor f where
  fmap :: (a -> b) -> (f a -> f b)
 -- 満たすべき公理がいくつか

-- Applicativeとは、 pure と (<*>) が定義されたFunctorのことである
class (Functor f) => Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b
  -- 満たすべき公理がいくつか

-- Monadとは、 (>>=) が定義されたApplicativeのことである
class (Applicative m) => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  -- 満たすべき公理がいくつか

アプリカティブ関手の元ネタである論文では、アプリカティブ関手とはstrong lax monoidal functorである、とされています。では、strong lax monoidal functorとは一体なんなのでしょうか？

それを知るためにはモノイド圏 (monoidal category) 周辺を勉強していけば良さそうです。

この記事ではHaskellの語彙と例を中心に解説していきますが、もっと圏論的な説明が読みたい人はPDFを読んでください。（風呂敷を広げ過ぎたので未完成です。すみません）

モノイド圏とアプリカティブ周りのPDF：applicative.pdf

圏のモノイド構造

集合圏の直積（デカルト積）や、線型空間の圏におけるテンソル積を一般化した概念をモノイド積と呼びます。ベースとなる圏が同じでも、複数のモノイド積が定まることがあります（同じ集合圏にも、直積と直和という異なる2つのモノイド積が定まる）。

Hask圏（Haskellの型を対象、関数を射とみなした圏。厳密には圏にはならないという話があるので、ボトムのことは都合よく忘れる）においては、タプル (,) や Either がモノイド積を与えます。

圏とその上のモノイド積の組をモノイド圏と呼びます。より詳しく言えば、モノイド圏とは、以下の組です：

• 圏 \(\mathcal{C}\)
• モノイド積と呼ばれる双関手 \(\boxtimes\colon\mathcal{C}\times\mathcal{C}\rightarrow\mathcal{C}\) （モノイド圏の文献ではモノイド積を\(\otimes\)で書くことも多いのですが、\(\otimes\)は線型空間のテンソル積を想起させるので、あえて違う記号を選びました。四角にバッテンだからと言って文字化けしているわけではありません）
• 単位対象 \(e\in\mathcal{C}\)
• associatorと呼ばれる自然同型 \(\alpha=\alpha_{a,b,c}\colon (a\boxtimes b)\boxtimes c\stackrel{\sim}{\longrightarrow} a\boxtimes(b\boxtimes c)\)
• left unitorと呼ばれる自然同型 \(\lambda=\lambda_a\colon e\boxtimes a\stackrel{\sim}{\longrightarrow} a\)
• right unitorと呼ばれる自然同型 \(\varrho=\varrho_a\colon a\boxtimes e\stackrel{\sim}{\longrightarrow} a\)

associator, left unitor, right unitorは「一貫性（コヒーレンス）条件」と呼ばれる条件を満たします（詳しくはPDFを見てください）。

モノイド圏の構成要素と比較するために、普通のモノイドの定義も思い出しておきましょう：

• 集合 \(M\)
• 二項演算 \(\,\cdot\,\colon M\times M\rightarrow M\)
• 単位元 \(e\in M\)
• 結合法則 \((a\cdot b)\cdot c=a\cdot(b\cdot c)\)
• 左単位則 \(e\cdot a=a\)
• 右単位則 \(a\cdot e=a\)

モノイド圏ではベースとなる集合が圏で、二項演算は双関手、単位元は単位対象となります。結合法則や左右の単位則は、等式ではなく自然同型に置き換えられました。というのも、圏論では「対象として同じである」ことは重要ではなく（対象はただのラベルに過ぎないので）、「対象が同型である」とした方が都合がいいからです。

例として、Haskellのタプル (,) について、モノイド圏の構成要素を書き出してみましょう。

• 双関手：(,)
• 単位対象：単位（ユニット）型 ()
• associator:
  • assoc :: ((a,b),c) -> (a,(b,c))
  • assocInv :: (a,(b,c)) -> ((a,b),c)
• left unitor:
  • leftUnitor :: ((), a) -> a
  • leftUnitorInv :: a -> ((), a)
• right unitor:
  • rightUnitor :: (a, ()) -> a
  • rightUnitorInv :: a -> ((), a)

さて、圏は関手と自然変換を語るための言葉なので、モノイド圏を定義したら、それに対応する「関手」「自然変換」も定義されるべきです。ただ、モノイド圏の関手の定義の方法はいくつか考えられます。

モノイドの準同型 \(f\) が満たす法則は\[f(e)=e, \quad f(a\cdot b)=f(a)\cdot f(b)\]ですが、さっきも書いたように圏論において対象の間に等式が成り立つことを要請するのは不自然です。つまり、モノイド関手 \(F\) について\[F(e)=e, \quad F(a\boxtimes b)=F(a)\boxtimes F(b)\]ではなく、もっと弱い形の\[F(e)\rightarrow e, \quad F(a\boxtimes b)\rightarrow F(a)\boxtimes F(b)\]や\[F(e)\leftarrow e, \quad F(a\boxtimes b)\leftarrow F(a)\boxtimes F(b)\]という関係を要請するべきです。

「モノイド関手」には、この辺の違いによって、laxモノイド関手 (lax monoidal functor), strongモノイド関手 (strong monoidal functor)、strictモノイド関手、oplaxモノイド関手などの変種があります。

「laxとかstrongとか、『strong lax monoidal functor』に近づいてきたぞ？」と思われるかもしれませんね。実際「strong lax monoidal functor」のlax monoidal functorは今説明したそれです。ですが、strongに関してはstrong monoidal functorのstrongとstrong lax monoidal functorのstrongでは全く異なる意味なので注意してください。

laxモノイド関手は

• 関手 \(F\colon \mathcal{C}\rightarrow \mathcal{D}\)
• 射 \(\varepsilon\colon e\rightarrow F(e)\)
• 自然変換 \(m\colon F(a)\boxtimes F(b)\rightarrow F(a\boxtimes b)\)

の組で、適切な条件を満たすものです。Haskell風に書けば

class (Functor f) => LaxMonoidal f where
  epsilon :: () -> f ()
  m :: (f a, f b) -> f (a, b)

となるでしょうか。

モノイド自然変換はlaxモノイド関手の間の自然変換で、通常の自然性に加えて\(\varepsilon\), \(m\)と可換になるもののことです。

内部ホムと閉圏

プログラミング言語によって、多変数関数の扱いは色々あります。C言語やJavaScriptのように「0個もしくは複数個の引数を取れる関数」を基本とするもの、MLやHaskellのように「1引数の関数」を基本とし、複数の引数をとる関数はタプルやカリー化を使うものです。

圏の射は、MLやHaskellのような「関数が1引数」の言語に似ていると言えます。複数の引数をとる射は \(a\times b\rightarrow c\) という風に、始域の側を直積やテンソル積として表現できます。あるいは、集合圏や線型空間の圏ではカリー化によって「関数を返す」射として同等の射を表現することもできます。

この「関数」に相当する対象は「内部ホム」と呼ばれ、\(c^b\) とか \(\operatorname{hom}(b, c)\) とか色々な書き方がされますが、ここでは \([b, c]\) と書くことにします。（圏の定義に使うホムセット \(\operatorname{Hom}(b, c)\) は圏によらず「集合」（またはクラス）ですが、 \(c^b\) や\(\operatorname{hom}(b, c)\) など内部ホムは「圏の対象」であることに注意してください）

集合圏や線型空間の圏のような「内部ホムを持つ圏」を一般的に取り扱うために、閉圏を定義します。

文献によってはモノイド積の右随伴として内部ホムを定義していますが、ここではモノイド積を仮定せずに内部ホムを定義します。

閉圏とは、以下の組です：

• 圏 \(\mathcal{C}\)
• 関手 \([-,-]\colon\mathcal{C}^{\mathsf{op}}\times\mathcal{C}\rightarrow\mathcal{C}\)
• 単位対象 \(e\in\mathcal{C}\)
• 自然同型 \(i=i_a\colon a\rightarrow[e,a]\)
• 対角自然変換 \(j=j_a\colon e\rightarrow[a,a]\) 「内部ホムの恒等射」
• 対角自然変換 \(L=L^a\colon [b,c]\rightarrow[[a,b],[a,c]]\)「内部ホムの関数合成」

例によって \(i\), \(j\), \(L\) は適切な公理を満たします（詳しくはPDFを参照）。

Haskellの関数型 a -> b はHask圏の内部ホムです。単位対象は先ほどと同じ単位型 () です。\(i\), \(j\), \(L\)に相当する関数は次のようになります：

i :: a -> (() -> a)
j :: () -> (a -> a)
L :: (b -> c) -> ((a -> b) -> (a -> c))

\(L\) に関しては見覚えがあるかと思いますが、関数合成演算子 (.) そのものですね！

閉圏を定義したからには、当然閉関手と閉自然変換も定義しなければなりません。

閉関手は

• 関手 \(F\colon \mathcal{C}\rightarrow \mathcal{D}\)
• 射 \(\varepsilon\colon e\rightarrow F(e)\)
• 自然変換 \(\mathsf{ap}\colon F([a,b])\rightarrow [F(a),F(b)]\)

の組で、適切な条件を満たすものです。Haskell風に書けば

class (Functor f) => Closed f where
  epsilon :: () -> f ()
  ap :: f (a -> b) -> (f a -> f b)

どこかで見たような型が登場しました。これはApplicative関手の<*>そのものですね。

（閉自然変換の定義はここでは省略します。詳しくはPDFを見てください。）

モノイド閉圏

モノイド積と内部ホムの両方を持つ圏をモノイド閉圏と呼びます。（もうちょっと詳しく言うと、モノイド積と内部ホムが随伴を介して結びついていなければなりません）

モノイド閉圏は「モノイド積が右随伴を持つ圏」として定式化することもできますし、実際そうしている文献もあります。

モノイド閉関手とモノイド閉自然変換も、雰囲気で定義できます。特に、モノイド閉圏においてはlaxモノイド関手と閉関手が実質同じ概念になります。

対称モノイド圏、対称閉圏、対称モノイド閉圏

対称モノイド圏とは、モノイド圏の左右の入れ替えができる圏です。例えば、Haskellでは

swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

という関数でタプルの左右を入れ替えられますね。

内部ホムに関して（対称閉圏）は

flip :: (a -> b -> c) -> (b -> a -> c)

という関数によって引数の左右を入れ替えられます。

強さを求めて

「strong lax monoidal functor」のlax monoidal functorの部分はわかりましたが、strongの部分はまだです。そのために関手の「強度」の概念を見ていきます。

強関手とfmap

圏の関手はホム集合の間の写像\[\operatorname{Hom}(a,b)\rightarrow\operatorname{Hom}(F(a),F(b))\]を与えますが、この対応は「集合としての写像」であり、圏の中の射ではありません。

一般の圏ならそれでも仕方ないのですが、閉圏には内部ホムがあります。内部ホムがある状況では、内部ホムの間の射があっても良いのではないでしょうか。

実際、Haskellでよくでてくる関手（Functorのインスタンスであるような関手）は「Haskell内部の」関数として

fmap :: (a -> b) -> (f a -> f b)

が定義されます。このように「圏の内部で」射の対応を作れるような関手を強関手と呼び、fmapのような \([a,b] \rightarrow [F(a), F(b)]\) を強度と呼びます。

そう、HaskellでFunctorのインスタンスとなるような関手はただの関手ではなく、強関手だったのです！ツヨイ！

強関手には満たすべき2つの公理がありますが、それはHaskellの言葉で言えば

fmap (f . g) = fmap f . fmap g
fmap id = id

に相当します。

強関手の間の自然変換も当然定義できます（略）。

モノイド圏における強関手

モノイド圏と閉圏は「多変数関数を扱える」と言う点で良く似ていました。閉圏で強関手を定義できたということは、当然（？）モノイド圏でも強関手を定義できます。

関手が強関手になるためには、通常の関手に加えて「強度」があれば良いのですが、一般のモノイド圏には内部ホムはないので\[[a,b]\rightarrow[F(a),F(b)]\]という定義は使えません。代わりにテンソル強度と呼ばれる\[t\colon a\boxtimes F(b)\rightarrow F(a\boxtimes b)\]を使います。

Haskellではテンソル強度を

tensorialStrength :: (a, f b) -> f (a, b)
tensorialStrength (x, m) = fmap (\y -> (x, y)) m

と定義できます。

モノイド閉圏には内部ホムもモノイド積もありますが、そのような状況では2種類の強関手の定義は同等と思えます。

強閉関手 (strong closed functor)

いよいよ核心に近づいてきました。

「関手を内部化できる」強関手と「内部ホムを保つ」閉関手の概念を組み合わせたものが強閉関手です。ただ組み合わせるだけではなく、強関手と閉関手の構造が適切な意味でコンパチブルになるようにします。

このとき、強閉関手 \(F\) には \(\eta=\eta_a\colon a\rightarrow F(a)\) という閉自然変換が定義できます。

この自然変換、どこかで見ましたね？そう、Applicativeクラスの pure :: a -> f a とそっくりです。

強laxモノイド関手 (strong lax monoidal functor)

強関手とlaxモノイド関手を組み合わせると強laxモノイド関手が定義できます。

このとき、強laxモノイド関手 \(F\) には \(\eta=\eta_a\colon a\rightarrow F(a)\) というモノイド自然変換が定義できます。

中間まとめ

アプリカティブ関手は強閉関手である。Haskellの圏はモノイド閉圏なので、「アプリカティブ関手は強laxモノイド関手である」と言っても同じことである。

ではここからは、モナドとアプリカティブ関手の関係を見ていきます。

強モナド

モナドの定義は有名だと思います（略。脳内で思い描いてください。またはPDFを見てください）。

しかし、モナドの定義ではどこにも「モノイド積」や「内部ホム」には言及していません。こんな状況で「モナドがlaxモノイド関手または閉関手である」なんて言えるわけはないですね？

つまり「モナドはアプリカティブ関手である」という主張は圏論的にはウソです。

しかし、先に見たようにHaskellでは関手を内部化できました。HaskellのFunctorクラスはただの関手ではなく、「強関手」と呼ばれるものに対応するのでした。ということは、HaskellのMonadクラスはただのモナドではなく、もっと「強い」モナドに対応すると考えられます。

強モナドとは、モナドの定義における自己関手が強関手であって、さらに自然変換を強自然変換に置き換えたものです。

この「強関手」や「強自然変換」は「モノイド積」や「内部ホム」と関連する概念なので、ここ（強モナド）から「laxモノイド関手または閉関手である」が言えてもおかしくありません。

強モナドから強laxモノイド関手（アプリカティブ関手）へ；処理の順番

強モナドにlaxモノイド関手の構造を与えるには、\[F(a)\boxtimes F(b)\rightarrow F(a\boxtimes b)\]という射を与えれば良いです。Haskellでいうところの (f a, f b) -> f (a, b) に相当します。

このような射（関数）は、Haskell的に考えれば引数を順番に処理して値を取り出し、タプルに入れて返す関数となります。しかし、処理の順番を考えると

-- 左を先に処理
f :: (Monad m) => (m a, m b) -> m (a, b)
f (u, v) = do x <- u
              y <- v
              return (x, y)

-- 右を先に処理
g :: (Monad m) => (m a, m b) -> m (a, b)
g (u, v) = do y <- v
              x <- u
              return (x, y)

の2通りの（一般には異なる）関数が考えられます。これらはどちらも真っ当なlaxモノイド関手の構造を与えますが、Haskellでは規約として最初の方（左を先に評価する）を採用しています。

その他

関手の「強度」周りの話は豊穣圏の言葉を使って話すこともできます。

多変数関数を圏論で扱う際にモノイド圏と内部ホムの2通りのやり方があると書きましたが、圏の概念を拡張して「複数の入力を取る射」を考える、というやり方もあります。これはmulticategoryと呼ばれているようです。

まとめ

• カリー化を多用するHaskellのような言語では、モノイド圏の言葉（タプル）よりも閉圏の言葉（関数型）で語った方が色々スッキリする！
• アプリカティブ関手はstrong closed functorまたはstrong lax monoidal functorである。
• 「モナドはアプリカティブ関手である」の意味するところは「強モナドは2通りの方法でアプリカティブ関手とみなせる」であって、Haskellではそのうちの一方を規約として採用している。
• 圏論的な話を知らなくてもアプリカティブ関手は使える。アプリカティブ関手に「アプリカティブ」という圏論っぽくない名前が付けられたのは幸いである。

細かいところの証明がまだ終わってないので、もしかしたらどこかで嘘を言ってるかもしれません。その場合は気付き次第コメント欄でご指摘願います。