「圏論とプログラミング」発表スライドメモ

この記事は、先日の 2020年01月25日に慶応大学で開催された[シンポジウム「圏論的世界像からはじまる複合知の展望」](http://www.inter.ipc.i.u-tokyo.ac.jp/symposium.html)の登壇資料を文字起こししたものです。

- Slide: [圏論とプログラミング / Category Theory and Programming \- Speaker Deck](https://speakerdeck.com/inamiy/category-theory-and-programming)
- Video: [圏論とプログラミング / 稲見泰宏 \- YouTube](https://www.youtube.com/watch?v=Ua6NE48_-1s)

---

![Category and Programming.001.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/9f300cdf-13f7-a096-a09d-2407eb5d2c52.png)

皆さん、こんにちは。稲見 泰宏と申します。
本日は、この圏論シンポジウムという貴重な場でお話しさせていただくことをとても光栄に思います。
私の方からは、**圏論とプログラミングに絡めた話**について発表します。
それでは、どうぞよろしくお願いします。

---

![Category and Programming.002.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/bf824173-4f61-4caf-7b10-5bf656c3efaf.png)

まず簡単に自己紹介します。稲見泰宏といいます。
現在は、フリーランスのiOSアプリ開発者として活動しております。
ここに書いてあるのは、私の過去10年間のプログラミング経歴ですが、
PHPとJavaScriptを使ったWeb開発に始まり、iOSエンジニアに転向してObjective-C、
途中寄り道もしながらJavaを学び、そして現在はよりモダンなSwift言語と、趣味でHaskellを少しだけ書いています。
 特にここ2年ほどは、より深くプログラミングを理解するために「圏論」を学んでいます。
元々は大学で物理学を専攻していて、最近はコンピュータ・サイエンス全般に興味があります。

---

![Category and Programming.003.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/75f551cf-6d57-56b6-db8e-afa5f6bdcd4c.png)

- [圏論とSwiftへの応用 / iOSDC Japan 2018 \- Speaker Deck](https://speakerdeck.com/inamiy/iosdc-japan-1)
- [プログラマのためのモナド\(圏論\) / \#cat4pg \- Speaker Deck](https://speakerdeck.com/inamiy/number-cat4pg)
- [Swiftプログラミングと論理 〜そして帰ってきた圏論〜 / Swift and Logic, and Category Theory \- Speaker Deck](https://speakerdeck.com/inamiy/swift-and-logic-and-category-theory)

ちなみに宣伝になりますが、ここにあるリンク集は、私がここ1〜2年で、 プログラミングと圏論をテーマに発表した資料です。
今日の発表はこれらの発展形になりますので、もしご興味があれば、これらの資料もぜひチェックしてみてください。

---

![Category and Programming.004.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/026f3a53-de15-a9b1-de36-3ea033f680fa.png)

さて、今日のテーマは **「圏論とプログラミング」** なわけですが、
よく聞かれるのが、 **「一般のプログラマーは圏論を学んだ方が良いのか？」** という質問です。
これに対して、私はこのように考えています。

---

![Category and Programming.005.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/cebee76f-a609-10c9-45ca-eebcffc6d0ff.png)

このスライドにあるのは、1990年代から2010年代にかけてのプログラミング言語の変遷です。
ご存知の通り、1990年代といえばまさに **インターネットが大普及する時代** で、
この頃に登場した **Webプログラミング (Python, Ruby, Java, JS, PHP)** は
比較的小規模のアプリケーション開発が中心で、軽量なインタープリタ言語が人気でした。

しかし2010年代にも入ると、**スマートフォンが大躍進**し、
サーバーだけでなく手元のクライアントアプリも**複雑な機能性が求められる**ようになりました。
それに伴い、プログラミング言語も、**型付き**で堅牢な言語が好まれるようになりました。
**Rust, Kotlin, TypeScript, Swift** などがそれらの代表的なモダン言語です。

---

![Category and Programming.006.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/5530dd2b-2702-becf-47de-8c428326454d.png)

これらの新しい言語に共通している点としては、
**静的型付け**であり、**型推論**が備わっていること、**ジェネリクス**があること、
**パターンマッチング**ができること、**モナド**の技術が使われている、などなどです。
つまり、この20年という時代の流れを一言でまとめるなら、
**「型付きプログラミング」の台頭**、ひいては**「関数型プログラミング」の台頭**といえます。

---

![Category and Programming.007.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/2ba60497-9edd-9aa3-6e72-2af51abe7405.png)

ここで、モナドといえば思い出すのは Haskell です。
そう、2010年代になって、**ようやく時代がHaskellに追いついてきた**と言っても過言ではありません。

---

![Category and Programming.008.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/36eb1d3f-7371-168c-da29-a4385f1bd616.png)

しかし、そんなHaskellもまた大きく影響を受けているのが、この**圏論**です。
いわゆる**矢印の理論**ですが、プログラミングの世界だけでなく、
**ありとあらゆる学問分野で用いられている**のが特徴です。

---

![Category and Programming.009.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/6c3e69ca-cbdf-35c4-3b56-c43783b209c6.png)

プログラマーが圏論を学ぶと嬉しいことは、ざっとこのようになります。
特に**実務の上で、型計算、設計、抽象化のスキルが上がる**というのは、
これからますます型の重要性が問われる時代において、大きなポイントだと言えます。

さて、そんな圏論とプログラミングの深い関係ですが、
ここからは実際に、**圏論がプログラミングにどのように影響を与え、
応用へとつながっていくのか**を見ていきたいと思います。

---

![Category and Programming.010.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/d5c853de-373b-cf66-e206-1fbeb079d995.png)

本日のアジェンダはご覧の通りです。
若干詰め込みすぎて、駆け足にはなると思いますが、全体像を俯瞰してもらえればと思います。
プログラミング言語は、Haskellを使います。

---

![Category and Programming.011.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/6b891225-3a83-365e-3a78-f19f67299210.png)

それでは、まずは**圏の定義**から見ていきましょう。

---

![Category and Programming.012.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/7fac16ef-9e9a-73c0-0dd0-dac1d31120ec.png)

圏の定義は大まかに、**恒等射`id`**と **射の合成演算`(.)` (ドット)** からなります。
これら2つをHaskellで書くとこのようなコードになります。
満たすべき性質としては、**単位法則**と**結合法則**が成り立つ必要があります。

---

![Category and Programming.013.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/d823e844-c330-eea1-30ce-3e759d4ae014.png)

ここで、Haskellには**型クラス**という便利な抽象化の機能があります。
他の言語でいうところの、**「インターフェース」「トレイト」「プロトコル」**と呼ばれるものです。
型クラスを使うと、まず `class Category` というものをこのように定義できます。
そして、この `cat` と書かれているところに「関数の矢印 `->`」を代入すると、
先ほどの実装が、いわゆる**型と関数の圏（Hask圏）** のインスタンスとして再定義することができます。

このように型クラスを使う利点として、他にもさまざまな便利な圏を定義することができます。
例えば。。。

---

![Category and Programming.014.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/93ef9ff3-984e-3895-8620-950487f26ec7.png)

このスライドにある**クライスリ圏**、いわゆる**「モナドに包まれた計算の射の世界」**というものを考えたり。。。
（参考：[プログラマのためのモナド\(圏論\) / \#cat4pg \- Speaker Deck](https://speakerdeck.com/inamiy/number-cat4pg)）

---

![Category and Programming.015.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/2799c002-5183-f301-75e3-9ebc051fa749.png)

あるいは**レンズ**という**「データ構造や内容にアクセスする機能の圏」**を作ることができます。
レンズについては、また後ほどご説明します。

---

![Category and Programming.016.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/8827c597-fd1e-9328-f0a7-dbd3e137edf9.png)

以上が、圏の定義になります。
次に、**関手**を見ていきます。

---

![Category and Programming.017.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/1d8140b1-5ed0-9b79-d4d0-8ce844343489.png)

**関手**については、一言で言うなら、**圏から圏へ、構造（形）を保つマッピング**です。

---

![Category and Programming.018.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/1ac97045-8308-fd8e-9f11-2d7db60a9107.png)

これをHaskellで考えると、このようなコードになります。
読み方としては、まず圏CとDがある上で、関手Fについて考え、
圏CにおけるAからBへの射 `c a b` は、圏Dにおける f a から f b への射 `d (f a) (f b)` に写る、
それが `fmap` となります。
関手の例としては、**2つの圏を同じHask圏として、Maybe型**をこのように実装することができます。
ただ、通常のHaskellのコードでは、このFunctorはやや冗長で、実際のところは。。。

---

![Category and Programming.019.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/d8395f57-ea3b-c9c1-4f28-f53b55e41936.png)

このように、Hask圏の自己関手の部分をまとめて `Functor` と呼ぶことがHaskellでは通例になっています。
つまり、**Haskellにおける`Functor`は、圏論における自己関手**のことです。

---

![Category and Programming.020.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/186684a8-082b-8dfb-65b1-29319369c48a.png)

それでは続いて、**関手圏と自然変換**について見ていきます。

---

![Category and Programming.021.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/9e4926dd-9105-8239-e31f-1dfcccb73527.png)

自然変換を一言で言うなら、**2つの圏の間を流れる関手が2つあり、
さらにその間を流れる自然な射α**、になります。
もしこの射が存在するならば、圏Dではいわゆる**可換図式**が成り立ちます。

---

![Category and Programming.022.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/4b68fd04-42e2-4a30-ef26-fb2805201483.png)

自然変換は、プログラミングでいうところの**ジェネリクス**に相当します。
**すべての x についての、 f x から g x への射の族**のことです。
このように自然変換を定義すると、自然変換もまた圏のインスタンスを構成することになります。
`id` は**恒等自然変換**、合成は**自然変換の垂直合成**になります。

---

![Category and Programming.023.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/070e2d5a-2382-becb-bd4e-ce90fdd6eaa2.png)

ここでは自然変換の例として、ジェネリック関数 `head` と `length` を考えてみましょう。
これらの関数は、「配列の最初の要素を取り出す」、ないし「全体の長さを計算する」ものです。

まず、`head` は `List a` から `Maybe a` への関数なので、`a` を無視して考えると、
**`List` から `Maybe` への自然変換**になります。

一方で、`length` は `List a` から `Int` の関数になりますが、これは一見すると、
返り値の型に関手が使われていないので、自然変換に見えないかもしれません。
しかし、ここで、`Const` という**定数関手**を使うアイディアがあります。
すると、実はこの関数もまた **`List` から `Const Int` への自然変換**で表せることが分かります。

---

![Category and Programming.024.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/99ca147c-5a60-d2dd-3e0c-0a887a3c1a61.png)

この定数関手を使った考えをさらに推し進めると、例えば、`Maybe a` は
`nothing` と `just` の2つのコンストラクタから構成されますが、
引数の型の関手はそれぞれ `Const ()` と `Identity` で書け、
これらを関手の直和でつなげることで、`Maybe` と**自然同型**になります。
注目してもらいたいのは、**この関手圏の世界ではもはや、プリミティブな型はほとんど登場せず、
関手とその射である自然変換が主役になっている**のが分かります。
これはまさに圏論で最も重要な**「関手と自然変換」**が成し得る世界観ですね。
Haskellではこれが美しく書けます。

ちなみに、関手の直和を取る話は、**モナドの計算効果を重ね合わせる**ための、
関手をベースとした足し算の話にもつながってきて、考え方としてとても重要になります。

---

![Category and Programming.025.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/24b8f67e-64d9-62dc-6d6f-a21940477379.png)

それでは次に**米田の補題**を見ていきます。

---

![Category and Programming.026.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/a10df042-710b-c791-a198-3bce5befcb49.png)

米田の補題は、先ほどの自然変換の図式で、右側の圏に**Set圏**を考え、
関手として**Hom関手**を使うと、**自然変換αの集合とF(A)が1:1に対応する**というものです。

---

![Category and Programming.027.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/a436fb86-9f88-2085-4c05-3005f89898da.png)

それを圏論で表現するなら上の式のようになります。
米田の補題の有名な例としては、**Fに恒等関手をおいたCPSと呼ばれる継続**であったり、
さらには**米田埋め込みがCPS変換に対応して、末尾再帰最適化などに使われています**。

このスライドでは、`newtype Yoneda`というものがHaskellに存在するので、
その中身を覗いてみると、実はそれが左辺と同じ形になるのが分かります。

---

![Category and Programming.028.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/f5f9d24c-a5a1-a69a-922c-a47055134fb2.png)

ここで、**米田埋め込み**と**米田の原理**をおさらいすると、このようになります。
特に**米田の原理**は、型プログラミングの世界において、**型計算の証明**で役に立ちます。

---

![Category and Programming.029.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/fe1167e7-1641-b652-7300-5e04fba234c4.png)

例えば、$(A^B)^C$ (`c -> b -> a`) を型計算したときに 
$A^{B×C}$ (`(b, c) -> a`) と同型であることが米田の原理から簡単に証明できます。
これは、単純な指数法則の1つではありますが、
型の世界でも全く同じように成り立つのはとても驚嘆に値します。

---

![Category and Programming.030.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/3b210959-5153-a122-772c-325df057218e.png)

ちなみに、米田の補題から得られる別の形として、**`Coyoneda`**と呼ばれる双対の形が挙げられます。
Haskell で表すとこのような形になりますが、この積分記号は圏論でいうCoendというもので、論理学でいう**存在量化子(∃)**だと思って下さい。
先ほどの`Yoneda`との違いとしては、**`lift`時（右辺から左辺への変換時）に、`f`が関手である必要がない**、という点です。
`lift` 後の`Coyoneda`は関手なので、言い換えるなら、**何もないところから関手ができる**ということになります。
これに加えて、いわゆる**フリーモナド**というものを組み合わせると、
**何もないところからモナドができる**、という面白いテクニック (Freer Monad) が使えます。

---

![Category and Programming.031.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/de42999b-60f0-ea6b-ed55-de8ad00eef90.png)

というわけで、この`Yoneda` / `Coyoneda` をまとめると、共変・反変バージョンを含めて
合計4つの同型の式が得られますが、実はこれらもおいおい型計算で大いに役立ってくれます。
ぜひとも覚えていってもらいたい式です。

---

![Category and Programming.032.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/94352176-2c5c-611b-4752-b560bbe3cb8f.png)

さて、どんどん先に進めます。次は**随伴**です。

---

![Category and Programming.033.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/8bb671f3-fc7c-fb88-1d0d-ba563f043dea.png)

**随伴**は、2つの圏について双方向に伸びる2つの関手があって、
このスライドのピンクの部分の**射集合が同型**であることを定義とします。
この場合、左の射集合から右への `leftAdjunct` 関数、
ないし逆変換の `rightAdjunct` 関数を定義することが、随伴になります。

---

![Category and Programming.034.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/0e7f2bc4-a11c-dcc5-5ce7-72aa107c7e0c.png)

ちなみに、`leftAdjunct` / `rightAdjunct` の代わりに、
この図式のように**`unit` と `counit`**を定義しても随伴になります。

---

![Category and Programming.035.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/3d4c9846-06e1-8f55-ee28-1e5c72e3bcf7.png)

以上のことをHaskellで記述すると、このように書けます。
実はこのコード、なかなか驚くべきことで、**並大抵のプログラミング言語ではこの実装がまずできません**。
なので、この点においても**Haskellは強力で読みやすく、圏論と極めて親和性が高い**といえます。

---

![Category and Programming.036.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/7d931bf1-5209-0075-dcd7-4ec615ed535f.png)

随伴の代表例としては、いわゆる**直積と冪の随伴関係**があります。
これをHaskellで書くと、このようになりますが、実装の中身は、いわゆる `curry` 化と `uncurry` 化に相当します。
curry 化は**2引数関数を1変数の高階関数に変換する**という点で、関数型プログラミングでは定番の機能です。

---

![Category and Programming.037.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/fce03708-d568-5f35-6fd4-7c270fa1a27b.png)

もうひとつ例としては、**クライスリ圏への埋め込み関手と拡張関手**というものがあります。
これは、少し複雑なバージョンのAdjunction型クラスを使うと、このように書くことができます。

他にも様々な随伴の例がありますので、こちらの記事を参考にしてみて下さい。

参考： [Haskellと随伴 \- Qiita](https://qiita.com/myuon_myon/items/d598480e4edd7a780ea7)

---

![Category and Programming.038.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/8ddae914-a7a4-fd72-1ebe-d36fb1260766.png)

はい、そしていよいよ、全ての概念である **Kan拡張** についてみていきます。

---

![Category and Programming.039.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/4b066f4e-89a7-5bf0-3bdc-a44a66cb8e75.png)

Kan拡張は、3つの圏A、B、Cと、2方向に伸びる関手G、Hがあるとき、
AからCに伸びるオレンジの射を考えるときに使います。
もしそのような普遍的な関手があると仮定したとき、他のどんなFを考えても、σの一意な自然変換が存在する。
この場合、オレンジの射のことを **右Kan拡張** といいます。

---

![Category and Programming.040.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/828d2f56-d1a8-7a45-c1cd-12b6fc255224.png)

このとき、黄色で塗られた2つの射の集合を考えると、これらは同型になります。
ここに、ある種の随伴関係が見て取れます。

---

![Category and Programming.041.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/0f7500dd-b5ab-c209-b166-85d8ea0aabe7.png)

以上をまとめて、圏Cの中身を展開してみると、このような図が書けます。
そして、やはりCの内部の黄色い射集合も同型になります。

ここで、Haskellには、`toRan` / `fromRan` という関数があるのですが、
この圏Cの中にある双方向な射がまさに、それら2つの関数に対応しているのが分かります。

---

![Category and Programming.042.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/fdbf509f-26e7-ceb5-a226-6111822ed786.png)

今の話を随伴部分だけ抜き出すと、このようにもう少し簡単に書けます。
スッキリ分かりやすくなったとも言えますし、逆に抽象度が上がりすぎて、初見殺しと言えるかもしれません。

---

![Category and Programming.043.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/39e7aede-caee-971a-a8da-0468e602a9f3.png)

これらの結果を Haskell ([kan\-extensionsパッケージ](https://hackage.haskell.org/package/kan-extensions)) で書くとこのようになります。
実は、**右Kan拡張**というのは、**極限、右随伴、さらにはYonedaを内包した型**になっており、
確かに変換する関数群が備わっているのが分かります。
それに対して、**左Kan拡張**というのは、右Kan拡張の双対、すなわち **余極限、左随伴、Coyoneda を内包**しています。

ちなみに私はHaskellを学び始めたとき、この**ワンライナーのコードの意味がさっぱり分からず苦い思い**をしましたが、
圏論を学ぶことでようやく読めるようになりました。

---

![Category and Programming.044.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/4d8e4e04-b27f-adb5-1a0b-6b62d2d59ce9.png)

さて、ここまでが一応基本編ということで、
この先は**実際のプログラミングへの応用編**に移りたいと思います。

---

![Category and Programming.045.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/6901e97f-6323-a680-bcd7-b16a910dc0d9.png)

まずは、**モナド**と**コモナド**から。

---

![Category and Programming.046.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/d9774154-0894-7e00-aaaf-bad5681b2fc0.png)

**モナド**については、Haskellで書くとこのような型クラスで記述できます。
こちらに関しては、一昨年に、私が詳しく解説した別の登壇資料があるので、今回は説明を割愛したいと思います。

参考： [プログラマのためのモナド\(圏論\) / \#cat4pg \- Speaker Deck](https://speakerdeck.com/inamiy/number-cat4pg)

---

![Category and Programming.047.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/c8dd541f-a393-0e34-1067-9c1271eeb31d.png)

ただ1点だけ、**随伴を使ったモナドの表現**をお見せします。
このコードは、先ほどの**「直積と冪の随伴」からモナドを作った場合**を示しています。
実はこの構成は、いわゆる**`State`モナド**というものに相当します。

---

![Category and Programming.048.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/d888c217-b9fd-1328-d954-0160ee1bac65.png)

やっていることとしては、**左随伴→右随伴の往復を2セット行う**と、
あっという間にモナドが出来上がるという仕組みです。

---

![Category and Programming.049.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/20071d83-1e3e-5a34-28b5-846bf85ed5d5.png)

そして同様に、**コモナド**についても随伴から考えることが可能です。
ちなみに、このスライドのコードは、Haskellでよく見かける`Comonad`型クラスです。
利用例としては、画像処理やライフゲーム、あとWebフロントエンド開発で有名な `React` のComponentなどもコモナドになります。

---

![Category and Programming.050.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/cb5be3ca-5048-0997-eb9b-8bdcdb828469.png)

そして先ほどの「直積と冪の随伴」からコモナドを作ると、
いわゆる **`Store`コモナド** が出来上がります。

---

![Category and Programming.051.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/ea95eae7-95f0-8b6c-6c91-8d5721ed11ff.png)

コモナドの作り方はやはり先ほどと似ていて、今度はモナドの時とは向きが逆で、
**右随伴→左随伴の往復を2セット**すると出来上がります。

---

![Category and Programming.052.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/1f4cd6f1-e58e-6fd6-2b22-b94073fe893e.png)

ちなみにコモナドを使った例としては、例えば**ライフゲーム**があります。
ライフゲームというのは、簡単な生存ルールを用いたシミュレーションゲームで、
2次元平面上で、隣のセルの生死に応じて、自分のセルの生死が決まるものです。
これをHaskellでサクッと実装すると、コモナドの力を使って。。。

---

![Category and Programming.053.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/acaa281a-6b9b-0836-1503-0bd5f9ce2e72.png)

たったこれだけのコード量で実装できます。
一応、赤線で引いた箇所がComonadのキモとなる部分です。

---

![Category and Programming.054.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/ab22558d-1714-35f7-24cd-49bb98f3dd5f.png)

そうすると、例えば簡単なgliderと呼ばれるライフゲームの例がこのように斜めに進んで動きます。
（NOTE: メモ化のない関数を使ったStoreコモナドはパフォーマンスが悪いので注意。実際は、高速な `Vector` などを使います）

---

![Category and Programming.055.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/4cc685f4-097a-a9a8-cc8a-7990cf6adf41.png)

続きまして、**アプリカティブ関手**の話に移ります。
アプリカティブというのは、Haskellにおいて`Functor`と`Monad`の中間に位置する重要な型クラスで、
例えば並列計算やより高速なパーサー処理などに使われますが、
これは圏論でいう**Lax Monoidal関手**というものを使って説明することができます。

---

![Category and Programming.056.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/c196d110-1ff9-59ae-115c-4c002a04c893.png)

**Lax Monoidal関手**というのは、2つのモノイダル圏の間をマップするFがあり、
さらに、単位対象とモノイド積について、右の圏にある**ηという射**と**μという自然変換**が備わっていることを指します。
この2つの矢印は、必ずしも同型射ではないというのがポイントで、**Lax Monoidal（緩いモノイダル関手）**と呼ばれる所以です。

---

![Category and Programming.057.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/03fe6683-45a1-83c0-6cca-96dcddcff81b.png)

そして、これらのLax Monoidalの性質に、**strength** というもう一つの自然変換が加わると、
Haskellにおける有名な`Applicative`になります。

ここでは、ηとμに着目すると、Haskellでは `unit`と`zip`という関数を使って定義することができます。

---

![Category and Programming.058.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/ea4b91e7-4a5b-d3fc-9ad2-f03a08bbcf92.png)

ちなみに、実際のHaskellの`Applicative`は、`unit` と `zip`ではなく、
下にある `pure`と`liftA2`という関数を代わりに実装することを条件としています。
ちなみに `unit` から `pure` への変換は、米田の補題を使うと簡単に同じものであることが示せます。

---

![Category and Programming.059.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/54833a43-4d49-e8d1-5ef5-06b70f1a5257.png)

ここで余談として、**Day Convolution** と呼ばれる「関手の積」があります。
これにもし F == G とおくと、まさに`Applicative`と同じ構造が得られることになります。
実は、アプリカティブというのは、モナドと同じく
「自己関手の圏におけるモノイド対象（ただしモノイド積は、Day Convolution）」
であり、これが先ほどの Lax Monoidal関手と等しくなります。

---

![Category and Programming.060.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/34217eaf-58f9-7c21-22cf-416b70679389.png)

続いて **Profunctor/Arrow** についてお話しします。

---

![Category and Programming.061.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/c5dff463-f0df-3eea-9d8a-40eacbfec3ae.png)

**Profunctor** というのは、2つの圏CとDに対して、**左側のC^opとDの積の圏からSet圏への関手**を意味します。
すると、左側で双方向に伸びる射 f と g が、Profunctorによって、`dimap f g` に写ります。

---

![Category and Programming.062.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/cec4075e-25b5-f1b2-1bc0-1dcf70402722.png)

これをHaskellで書くとこのようなコードになります。

---

![Category and Programming.063.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/aa858406-37d4-fdbf-b52e-e8e88f594373.png)

次に、このProfunctorにさらに**strength**という自然変換を追加します。
（NOTE: 先ほどのアプリカティブ関手に備わるstrength の profunctor版）

モノイド積に「直積」ないし「直和」を用いることで、
`StrongProfunctor` と `ChoiceProfunctor` をこのように定義できます。

---

![Category and Programming.064.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/1c467b20-d6e7-ebe7-e2c5-4ccca751d286.png)

そして、これらにさらにモノイド対象を加えると、`Arrow` や `ArrowChoice` と呼ばれる構造になります。

---

![Category and Programming.065.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/08a82eb0-e15e-d79a-2b77-0d0a4afdd3ce.png)

この図は、**`Arrow`の基本的な性質**をまとめた図になります。
アプリカティブやモナドと同じく、並列や直列の計算効果を表せる一方で、
`Arrow`の場合は、入力を受け取って選択できるなど、より抽象度の高いクラスになります。

---

![Category and Programming.066.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/8b66fa2f-d76f-a447-27f1-21f78112f8ad.png)

この`Arrow`を使った例としては、`Profunctor`と合わせて考えると、
実は圏論でいうところの**直積・直和の普遍性**について説明することが可能です。
まず、`Arrow`の (`&&&`) と `Profunctor` の `unzip` から**直積の普遍性**が得られます。
また、`ArrowChoice` の (`|||`) と `Profunctor` の `unzipEither` から、**直和の普遍性**が導かれます。

---

![Category and Programming.067.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/46e6c0e9-04bf-de31-5c1b-50be658745a4.png)

**直積と直和の普遍性**を図に表すと、ご覧の通りです。
圏論では当たり前に見るこの図式ですが、プログラミングの世界でいえば
**複数の関数を束ねたり、パターンマッチングで分岐したり**、プログラミングの重要な側面について説明しています。
そしてそれらを抽象化する考え方が`Arrow`といえます。

---

![Category and Programming.068.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/25e43a06-4c87-7ce1-0aff-69127331cdb0.png)

それではいよいよ **Optics**と呼ばれる**Lensの一般化**について見ていきます。

---

![Category and Programming.069.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/b279cfc6-6a7c-c20a-ea0b-36cd811cfe22.png)

**Lens**というのは、**複雑なデータ構造のアクセスを提供する型**になります。
例えば、この図のようなツリー構造があったとして、その奥底にあるノードの情報を変更したいとします。

---

![Category and Programming.070.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/090db4ba-73dc-cd24-ebd2-c46ff2897343.png)

その際、必要なステップとしては、まずゲッターを使って下位のノードにアクセスして。。。

---

![Category and Programming.071.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/7e6b20d6-20ba-3855-b374-32551a5466a2.png)

それを更新したら、親ノードを含めて次々にアップデートしていきます。

---

![Category and Programming.072.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/226c3485-4590-e079-1a6b-d9a368322a89.png)

つまり、**各階層でゲッターとセッターの両方**が使用されて、このペアのことを**Lens**といいます。

---

![Category and Programming.073.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/37c0d966-b409-8a42-6981-a0d9e382357d.png)

そうすると、最初の例にもあった通り、**Lensは圏を構成するので、2つのLensを合成することが可能**です。
この図のように、**合成して deep な getter と setter のレンズを作る**ことができます。
ちなみに、この図の矢印は少し簡略化した書き方をしていて、実際のところは次のスライドのようになります。

---

![Category and Programming.074.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/cfd09b3d-166b-21cf-cb24-b9e09cab0442.png)

つまり左側の`Lens`のように、**実際の矢印は単純な双方向ではなく、グニャっとカーブした矢印も含まれている**のが分かります。
他にも、`Prism`や`Traversal`、`Iso`など、**様々な形の双方向的な射のペアがある**ことが分かります。
これらをまとめて**`Optics`**といいます。

---

![Category and Programming.075.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/82f0485e-4fe5-cdff-685b-35a12b96c1e3.png)

この一連のOpticsパターンを上手く抽象化する方法として、圏論のCoend (存在量化子)を使って上の式のように書くことができます。
そして、テンソル積 `⊗` に直積(タプル)や直和(`Either`)を代入すると、先ほどの`Lens`や`Prism`が作れます。

---

![Category and Programming.076.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/70a1ca24-9415-78e6-fae3-294c17b7277d.png)

さて、このOpticsパターンですが、もっと上手い書き方はないでしょうか？
このスライドは、双方向だけからなる`Iso`の射がProfunctorを経てSet圏に写っている図式ですが、
これは見方を変えると、このようにも言えます。

---

![Category and Programming.077.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/77046d0c-0d4c-73e9-ecac-0ba8103522ad.png)

それは、**先ほど中央にあったProfunctorの圏を左側に移行して考える**ことです。
そうすると、**左側にあったIsoの射は、中央の赤矢印の自然変換に対応する**ことが分かります。
これを **Profunctor Iso**といいます。
この仕組みは簡単で、**米田埋め込みを2回行う**と、両者が同じものであることが証明できます。

---

![Category and Programming.078.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/b42d9f8e-0912-09cf-a886-c92c6be3aa2e.png)

ひとたび、Profunctor Isoが分かると、今度はより複雑なレンズの射を考えたときにも
同じテクニックが利用できて。。。

---

![Category and Programming.079.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/330ce8b5-8fe8-6deb-780f-a243a7506db4.png)

やはり`Lens`も同様に、自然変換を使った**Profunctor Lensの射**に置き換えることが可能です。
ちなみに違いとしては、先ほどの`Iso`では`Profunctor`を使っていましたが、
`Lens`の場合はさらに強力な`StrongProfunctor`を使います。

---

![Category and Programming.080.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/7a9feb7f-b172-5b60-c15c-1ea59e536fbc.png)

こうすると、Opticsの実装はさらに美しく書くことができて、
突き詰めると **`Profunctor` から `Profunctor` への自然変換**、になります。
ちなみに、Opticsの種類としては、ここにあるのは、あくまで一例で、、、

---

![Category and Programming.081.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/193c93b3-0945-4805-b996-5f78ea9e4918.png)

実際はこの図のように、**たくさんのOpticsのパターンとその親子関係**で構成されています。
状況に応じて、これらを組み合わせたりしながら、様々なデータ構造にアクセスすることが可能になります。

---

![Category and Programming.082.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/a310c48d-e0eb-dcbe-b138-32b2324983f6.png)

そして最後に駆け足で、**Recursion Scheme**についてお話します。
簡単にいうと、**再帰的なデータ構造に関する計算全般**のことを指します。

---

![Category and Programming.083.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/5b092234-ca44-f2ed-b773-2bde96e4d804.png)

再帰的なデータとは、例えば`List`のような構造で、**定義の中で再帰が発生している**、つまり**右辺の中に左辺が存在する**ものです。
これは、**`ListF`というベース関手を用意して、その不動点を計算すると求まる**ことが知られています。
`Fix`の定義から、`Fix(F)`と`F(Fix(F))`が同型になり、これを圏論的視点からいろいろ活用できます。

---

![Category and Programming.084.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/af6e83e3-f82b-eed4-4797-919f18e1af81.png)

代表的なRecursion Schemeの例としては、
Fixの定義を **F-始代数 (initial algebra)** として見たときの、そこからの畳込みである **Catamorphism** であったり、
**F-終余代数 (final coalgebra)** へのデータ生成となる **Anamorphism** が挙げられます。
他にも、機能を追加した **Paramorphism** やその双対の **Apomorphism** があります。

---

![Category and Programming.085.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/8ec994c1-e249-7cac-e55f-7ded3ed87a24.png)

これらをHaskellで書くとこのように書くことができ、様々な再帰処理の場面で活用することができます。

---

![Category and Programming.086.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/7430f0dc-a9cd-9fe6-1dfc-8640fc3ca440.png)

こちらは先ほどの説明の通りです。
Para-はいわゆる「原始再帰」とも言われます。


---

![Category and Programming.087.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/77bca7a1-90e4-9287-3d5e-d222ff322abf.png)

何とかモルフィズムというのは、他にも実にたくさんの種類があり、こちらの図が参考になります。

---

![Category and Programming.088.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/adeadc2d-7173-2f9b-bd2f-b20aea7d566b.png)

Recursion Schemeは再帰処理のあらゆる場面で活用できます。
例えば**ソートアルゴリズム**や**動的計画法**などを圏論的視点から眺めると、より面白い結果が見えてきます。

参考：[挿入ソートと選択ソートは双対 \- Qiita](https://qiita.com/lotz/items/a69587882be6e987de4e)

---

![Category and Programming.089.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/f1d0ab4e-a68d-a198-991b-1ca9b005c226.png)

というわけで、以上、駆け足になりましたが、まとめに入ります。

---

![Category and Programming.090.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/38516403-c9c9-b9d0-d255-c7511a95359c.png)

今回、実に様々な圏論の概念について、**Haskellでどのように記述できるか**、
また、それらが**どのように応用されるのか**を見てきました。
これらをまとめると、圏論には、**プログラミング理論を学ぶためのエッセンスが随所に散りばめられている**ことが分かります。
個人的な意見としては、圏論は全てのプログラマーには必要ないかもしれませんが、
さらに深くプログラミングそのものを知るためには、Haskellの理解を含め、土台を支える圏論を学ぶことが欠かせないと思っています。
大変駆け足な発表になりましたが、今日の内容から何か皆様の中で得るものがありましたら幸いです。

---

![Category and Programming.091.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/ce3b56b0-234b-23db-558c-9afd1695d75b.png)

参考文献：

- [Category Theory for Programmers](https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/)
- [圏論 | 壱大整域](http://alg-d.com/math/kan_extension/)
- [Monads Made Difficult](https://www.stephendiehl.com/posts/monads.html)
- [Haskellと随伴 - Qiita](https://qiita.com/myuon_myon/items/d598480e4edd7a780ea7)
- [kan-extensions](https://hackage.haskell.org/package/kan-extensions-5.2)
- [Generalising Monads to Arrows](https://www.cse.chalmers.se/~rjmh/Papers/arrows.pdf)
- [Arrows: A General Interface to Computation](https://www.haskell.org/arrows/index.html)
- [Don't Fear the Profunctor Optics!](https://github.com/hablapps/DontFearTheProfunctorOptics)
- [What You Needa Know about Yoneda - Profunctor Optics and the Yoneda Lemma](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)
- [Profunctor Optics: Modular Data Accessors](www.cs.ox.ac.uk/people/jeremy.gibbons/publications/poptics.pdf)
- [Categories of Optics](https://arxiv.org/abs/1809.00738)
- [Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire](https://maartenfokkinga.github.io/utwente/mmf91m.pdf)
- [Curse explicit recursion!](https://lahteenmaki.net/dev_*18/)
- [Recursion Schemes - haskell-shoen](https://scrapbox.io/haskell-shoen/Recursion_Schemes)
- [A Duality of Sorts](https://www.cs.ox.ac.uk/ralf.hinze/publications/Sorting.pdf)

---


![Category and Programming.092.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2249/b9cc4330-42cb-9dee-1a45-8798f03cb2a7.png)

以上になります。ご清聴ありがとうございました。