Qiita Teams that are logged in
You are not logged in to any team

Log in to Qiita Team
Community
OrganizationEventAdvent CalendarQiitadon (β)
Service
Qiita JobsQiita ZineQiita Blog
357
Help us understand the problem. What are the problem?

More than 1 year has passed since last update.

posted at

updated at

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

この記事は、先日の 2020年01月25日に慶応大学で開催されたシンポジウム「圏論的世界像からはじまる複合知の展望」の登壇資料を文字起こししたものです。


Category and Programming.001.png

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


Category and Programming.002.png

まず簡単に自己紹介します。稲見泰宏といいます。
現在は、フリーランスのiOSアプリ開発者として活動しております。
ここに書いてあるのは、私の過去10年間のプログラミング経歴ですが、
PHPとJavaScriptを使ったWeb開発に始まり、iOSエンジニアに転向してObjective-C、
途中寄り道もしながらJavaを学び、そして現在はよりモダンなSwift言語と、趣味でHaskellを少しだけ書いています。

特にここ2年ほどは、より深くプログラミングを理解するために「圏論」を学んでいます。
元々は大学で物理学を専攻していて、最近はコンピュータ・サイエンス全般に興味があります。


Category and Programming.003.png

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


Category and Programming.004.png

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


Category and Programming.005.png

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

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


Category and Programming.006.png

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


Category and Programming.007.png

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


Category and Programming.008.png

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


Category and Programming.009.png

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

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


Category and Programming.010.png

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


Category and Programming.011.png

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


Category and Programming.012.png

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


Category and Programming.013.png

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

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


Category and Programming.014.png

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


Category and Programming.015.png

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


Category and Programming.016.png

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


Category and Programming.017.png

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


Category and Programming.018.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

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


Category and Programming.020.png

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


Category and Programming.021.png

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


Category and Programming.022.png

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


Category and Programming.023.png

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

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

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


Category and Programming.024.png

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

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


Category and Programming.025.png

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


Category and Programming.026.png

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


Category and Programming.027.png

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

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


Category and Programming.028.png

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


Category and Programming.029.png

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


Category and Programming.030.png

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


Category and Programming.031.png

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


Category and Programming.032.png

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


Category and Programming.033.png

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


Category and Programming.034.png

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


Category and Programming.035.png

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


Category and Programming.036.png

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


Category and Programming.037.png

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

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

参考: Haskellと随伴 - Qiita


Category and Programming.038.png

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


Category and Programming.039.png

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


Category and Programming.040.png

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


Category and Programming.041.png

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

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


Category and Programming.042.png

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


Category and Programming.043.png

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

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


Category and Programming.044.png

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


Category and Programming.045.png

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


Category and Programming.046.png

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

参考: プログラマのためのモナド(圏論) / #cat4pg - Speaker Deck


Category and Programming.047.png

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


Category and Programming.048.png

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


Category and Programming.049.png

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


Category and Programming.050.png

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


Category and Programming.051.png

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


Category and Programming.052.png

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


Category and Programming.053.png

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


Category and Programming.054.png

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


Category and Programming.055.png

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


Category and Programming.056.png

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


Category and Programming.057.png

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

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


Category and Programming.058.png

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


Category and Programming.059.png

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


Category and Programming.060.png

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


Category and Programming.061.png

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


Category and Programming.062.png

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


Category and Programming.063.png

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

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


Category and Programming.064.png

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


Category and Programming.065.png

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


Category and Programming.066.png

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


Category and Programming.067.png

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


Category and Programming.068.png

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


Category and Programming.069.png

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


Category and Programming.070.png

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


Category and Programming.071.png

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


Category and Programming.072.png

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


Category and Programming.073.png

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


Category and Programming.074.png

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


Category and Programming.075.png

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


Category and Programming.076.png

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


Category and Programming.077.png

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


Category and Programming.078.png

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


Category and Programming.079.png

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


Category and Programming.080.png

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


Category and Programming.081.png

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


Category and Programming.082.png

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


Category and Programming.083.png

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


Category and Programming.084.png

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


Category and Programming.085.png

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


Category and Programming.086.png

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


Category and Programming.087.png

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


Category and Programming.088.png

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

参考:挿入ソートと選択ソートは双対 - Qiita


Category and Programming.089.png

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


Category and Programming.090.png

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


Category and Programming.091.png

参考文献:


Category and Programming.092.png

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

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
357
Help us understand the problem. What are the problem?