エムスリーテックブログ

エムスリー(m3)のエンジニア・開発メンバーによる技術ブログです

プログラムから圏のことばまで，或はモナドについて（後半）

こんにちは，エムスリーエンジニアリングGの榎田（@niflh）です．最近は SEKIRO をトロコンしたり，確率論の勉強をしたりの日々です．

この記事は前半に引き続く，関数型言語で登場するモナドに関する記事の後半です．前半は数学成分控えめにモナドの解説を試みました．

後半では数学のことばをあまり控えずに著します．モナドを勉強するとあらわれる圏論のことば（のうち，「関手（かんしゅ）」と「自然変換」）について，プログラムに即した理解を試みるのが本稿後半の目的です．或いは，「関数型を勉強するとたまに圏論のことばが出てくるけれども，あのことばたちはプログラムの何に対応するの？」という疑問に（私に可能な範囲で）答える，と言ってもいいでしょう．

本稿は，「圏論のことばに置き換えて新しい知見を得る」ところまでは届きません．それでも，「関数型を勉強していたら突然圏論が出てきて困った」という状況に対するひとつの処方箋として，本稿の役立つところがあるのではないかと信じて書きます．

前半の復習

前半では，Monadが value のみならず computation を扱うための概念であること，および以下のパーツから構成できることを述べました．

  • 「どんな計算 computation がしたいのか」を示す型T
  • value to value の関数を computation to computation の関数に変換するmap
  • Tで包んで value から computation への橋渡しを担うpure
  • Tの入れ子を剥ぐflatten

それぞれのメソッドの型を明示するため，擬似コードを置いておきます．mapの引数の順番を前半とはわざと入れ替えています．

trait Monad[T[_]] {
  def map[A, B](f: A => B)(ta: T[A]): T[B]
  def pure[A](a: A): T[A]
  def flatten[A](tta: T[T[A]]): T[A]
}

以下では，Tおよびmapが併せて「関手（かんしゅ）」と呼ばれる概念であること，pureおよびflattenが「自然変換」と呼ばれる概念であることを見ていきます．

型クラス Functor と関手

本稿ではあまりmapの性質について議論してきませんでしたが，mapは以下の性質を充たすことが普通です．

  • 「なにもしない」関数をmapすると，引数の型は変わるが，実態は「なにもしない」関数のまま．A上の恒等関数をmapするとT[A]上の恒等関数にうつる，と言っても良い．
    • map(a => a) == (ta => ta)ということ．
    • 本稿前半のmapの引数の順番に即して書くと，(ta => map(ta)(a => a)) == (ta => ta)です *1 ．
  • mapしてから合成しても，合成してからmapしても結果は同じ．
    • ta: T[A]，f: A => B，g: B => Cに対して，map(a => g(f(a)))(ta) == map(g)(map(f)(ta))ということ．

このようなmapをもつ型クラスは，Cats においてFunctorと呼ばれます．functor は「関手（かんしゅ）」と訳される，圏論由来の概念です…というより，このmapは（Tと併せて）関手そのものです．それを見るために，上の性質を書き換えていきます．

上に挙げたmapは関数を変換するものですが，その実装は型Tごとに異なります．それを明示するために，型Tのmapを T_M と書いてみることにします．つまり，関数 f \colon A \to B に対して， f をmapで変換した結果を T_M(f) \colon T[A] \to T[B]と書く，ということです*2．更に色々なところを書き換えてみましょう．

  • A 上の恒等関数 \mathrm{id}_A を T_M で変換すると T[A] 上の恒等関数 \mathrm{id}_{T[A]} にうつる．
    • T_M(\mathrm{id}_A) = \mathrm{id}_{T[A]} ということ．
  • T_M してから合成しても，合成してから T_M しても結果は同じ．
    • f \colon A \to B および g\colon B \to C に対して， T_M(g \circ f) = T_M(g) \circ T_M(f) ということ．

ここでやや唐突ですが，（自己共変）関手の定義を述べます．定義していない用語が多数出てきますが，定義を理解してもらう必要はないです．文字面がなんとなく似ていることをお見せするのが目的です．

定義． \mathcal{C} を圏とする *3 ．「関数」 T が \mathcal{C} 上の関手 functor （正確には自己共変関手 covariant endofunctor） であるとは，次の条件を全て充たすことをいう．

  • T は \mathcal{C} の対象または射を入力として受け付ける．
  • T は \mathcal{C} の対象 A を入力すると \mathcal{C} の対象 T(A) を返す．
  • T は \mathcal{C} の射 f \colon A \to B を入力すると \mathcal{C} の射 T(f) \colon T(A) \to T(B) を返す．
  • A 上の恒等射 \mathrm{id}_A を T で変換すると T(A) 上の恒等射 \mathrm{id}_{T(A)} にうつる．すなわち T(\mathrm{id}_A) = \mathrm{id}_{T(A)} ということ．
  • どのような射 f \colon A \to B および g\colon B \to C に対しても， T(g \circ f) = T(g) \circ T(f) が成り立つ．

細かな点（ T_M と T で記号を分けているか， T[A] と書くか T(A) と書くか，等）を見逃せば，同じことを述べていることがわかります．特に，mapは型Tと併せて関手の定義を充たします．これが，Functor型クラスがその名を冠する所以です．

型構造の抽象としての圏

上に挙げたmapの性質と関手の定義をより丁寧に突き合わせていくと，次のような対応たちが見いだせます．

  • 「圏 \mathcal{C} の対象 A」は，型Aと対応している．
  • 「圏 \mathcal{C} の射 f \colon A \to B」は，（純粋）関数f: A => Bと対応している．
  • とくに，「 A 上の恒等射 \mathrm{id}_A」は，A上の恒等関数a => aと対応している．
  • f: A => Bとg: B => Cの合成関数a => g(f(a))があるように，「射の合成 g \circ f」というものもある．

正確な定義は述べませんが，上に挙げた「対象と射からなる，恒等射や合成という概念も持つなにか」を圏と呼びます．プログラミングで現れる型および関数の構造は，その具体例の一つとして捉えることができそうです*4．或いは，このような型や関数の構造の抽象化のひとつが圏であると言っても良いでしょう*5．

flatten と自然変換

前半で，Tの入れ子を剥ぐメソッドとしてflattenを紹介しました．機能としてはこれ以上紹介することはないのですが，このメソッドは「自然変換」として捉える見方もできます．

圏論の話と関係なしに，flattenには期待したい性質があります．それは，「関数fがあるとき，（必要ならmapでfの型を合わせる前提で）fしてからflattenしても，flattenしてからfしても結果が変わらない」ことです．入れ子を剥がすタイミングを間違えると結果が変わるのでは使いづらいですから．

この要請を正確に述べます．これ以降は，mapが関手であることを意識して，型Tのことも，それに付随するmapのことも T と書きます． T[T[A]] のことを T^2[A] と書きます． f \colon A \to B を関数とし，それを1回mapしたものを T(f) \colon T[A] \to T [B] と，2回mapしたものを T^2(f) \colon T^2[A] \to T^2 [B] と書くことにします ． T^2 という，「型に対しては二重でTで包み，関数に対しては二重でmapする」別の関手を考えていると言っても良いです．これらの記号の準備の下，先程の要請は次のような図で表すことができます．

f:id:ehlfin:20200726184341p:plain
flatten に対する要請をあらわした図式．

ただし， \mu_A は flatten[A]を， \mu_B は flatten[B]をそれぞれ示します *6 ．図式において「下に行ってから右に行く」のが「fしてからflatten」「右に行って下に行く」のが「flattenしてからf」にそれぞれ対応します．この「結果が図の中での道順に依らない」ことを，数学のことばで「図式が可換である」と言います．

再び唐突に，圏論における自然変換の定義を出します．

定義． \mathcal{C} を圏とし， S および T を \mathcal{C} 上の（自己共変）関手とする．「関数」 \mu は，以下の条件を全て充たすときに S から T への自然変換と言われる．

  • \mu は入力として \mathcal{C} の対象を受け付ける．
  • \mathcal{C} の対象 A を入力したときの返り値は， S(A) から T(A) への射である．この射を \mu_A と書く．
  • 返り値である射たちは次の性質を充たす；どのような射 f \colon A \to B に対しても，次の図式が可換となる．

f:id:ehlfin:20200726184417p:plain
自然変換が充たすべき可換性．

\mu が S から T への自然変換であることを， \mu \colon S \to T のように書く．

やはり細かな点を除けば，同じことを書いていることがわかると思います．すなわちflattenとは，関手 T^2 から関手 T への自然変換にほかなりません．

全く同様にして，pure は「恒等関手」 \mathrm{id} から関手 T への自然変換 \eta であると理解することができます．

後半まとめ：圏のことばでモナドを望む

ここまでで，モナドを構成するそれぞれの部品が，実は圏論に現れることばの具体例として位置づけられることを見てきました．或いは，プログラムに現れるモナドを数学のことばで抽象して圏論まで行き着いたとも言えます．

  • モナドはひとつの関手 T およびふたつの自然変換 \mu, \eta からなる．
  • 関手 T は，型Tおよびそれに付随するmapの圏論的な対応物である．
  • 自然変換 \mu \colon T^2 \to T は，flattenの抽象化にあたる．
  • 自然変換 \eta \colon \mathrm{id} \to T は，pureの抽象化である．

最初に述べたとおり，圏論の視点ゆえに得られる恩恵についてはここでは述べません*7．本稿では，様々な型とモナドとの関係，およびモナドに関わる概念たちと圏論のことばとの関係を述べることで，イメージが湧きにくい圏論のことばを，具体的なモナド，ないしは型に根ざして理解するひとつの方向性を描こうとしました．この試みが，読者の皆さんにとって何かしらの一助となることを願いつつ，筆を置くことにします．

この先に見えそうなもの

以下に，まだ勉強していないがぼんやり疑問に思っていることを書き並べておきます．なにか面白い話を見つけたら，どこかで記事を書くかもしれません．この記事を読んだ方でなにかご存じの方はぜひ教えて下さい．

  • pureとflattenは随伴対か？
  • モナド変換子は自然変換として捉えられるか？
  • プログラムと圏論の関係でよく顔を出すのはデカルト閉圏であるが，本稿で扱っていない冪対象の役割は何か？
  • 型と関数の圏に対して米田埋め込みをすると何が出てくるのか？
  • Curry-Howard-Lambek 対応を踏まえ，型理論に有益な知見が出せるか？

We are hiring!

本稿のきっかけとなった Scala with Cats 読み会をはじめ，社内では複数の勉強会をしています．ご興味のある方はぜひ話を聞きに来てください．

jobs.m3.com

*1:が，わかりづらいと思います．なので引数の順番を入れ替えています．

*2:ここから LaTeX 記法を使い始めていますが，単に記法を変えただけで，同じことを書き続けています．

*3:技術的な注：圏の大きさについては議論しません．本稿では集合論的に扱いが難しい部分に踏み込むことは目的ではないし，また私にその能力はないからです．おそらく (locally) small を仮定すれば本稿の範囲では問題は吹き出さないと思うのですが．

*4:が，具体的な型システムが圏と見做せるかどうかについては注意深い考察が必要です．例えば Haskell の型システムは Bottom 型のせいで圏を成しません．

*5:歴史的にはそうではないです．圏論ははじめ代数トポロジーにおいて発展し，それが後になって計算機科学への応用を見いだされたと聞いています．

*6:わざわざ記号を変えているのは，LaTeX の図式で “flatten” と書きたくないから，というのと，直後に出す自然変換の定義に合わせてのことです．

*7:実際のところ「これは誰もが納得する明確な恩恵だ」という具体例をいまだ知らないのが悲しいところで，ぜひ知りたいと思っています．しかしそれでも，圏論を補助輪にしてプログラミングの理解を深める窓口が開いているというだけで，私にとって間違いなく役に立っています．