Haskell/圏論

出典: フリー教科書『ウィキブックス(Wikibooks)』



この項目では Haskell に関連する内容に限って圏論の概観を与えることを試みる。そのために、数学的な定義に併せて Haskell コードも示す。絶対的な厳密さは求めない。そのかわり、圏論の概念とはどんなものか、どのように Haskell に関連するかの直感的な理解を読者に与えることを追求する。

圏の導入[編集]

3つの対象A, B, C、3つの恒等射, , と、さらに別の射, からなる単純な圏。3つめの要素(どのように射を合成するかの定義)は示していない。

本質的に、圏とは単純な集まりである。これは次の3つの要素からなる。

  • 対象(Object)の集まり。
  • ふたつの対象(source objecttarget object)をひとつに結びつけるの集まり。(これらはarrowと呼ばれることもあるが、Haskellではこれは別の意味を持つ用語なので、ここではこの用語を避けることにする。) f がソースオブジェクト A からターゲットオブジェクト B への射であるとき、これを と書く。
  • これらの射の合成の概念。 h が射 f, g の合成であるとき、これを と書く。

様々なものが圏をつくる。例えば、Set は全ての集合を対象とし、射として標準的な関数、合成として通常の関数合成を持つ圏である。(圏の名前はしばしば太字で表される。)Grpは全ての群を対象とし、射として群の演算を保存する関数(群準同型)を持つ圏である。つまり、任意の2つの群 G, H (それぞれ演算, をもつ)について、 ならば、かつそのときに限り、Grp 内の射である。

射はいつも関数のようにも思えるが、そうである必要はない。例えば、いかなる半順序 (P, )も圏を定義する。ここで対象はPの要素であり、任意の2つの対象A, Bについてであるときかつそのときに限りABの間に射が存在する。また、複数の異なる射が同じソースオブジェクトとターゲットオブジェクトを持つことができる。Setの例でいえば、 はいずれもソースオブジェクト と ターゲットオブジェクト をもつが、もちろんこれらは同じ射ではない!


カテゴリ則[編集]

圏が従わなければならない規則が3つ存在する。最初に、非常に単純だが、射の合成は結合的である必要がある。つまり、

次に、圏は合成演算において閉じていなければならない。すなわち、もし かつ ならば、のような射がその圏に存在しなければならない。次の圏を使えば、これがどのように働くかを見ることができる。

fg はどちらも射であるので、これらを合成したらこの圏にあるいずれかの射を得るはずである。では、どれが射だろうか?唯一の答えはである。同様にもわかる。

最後に、いかなる対象 A についても恒等、すなわちその射との合成が恒等であるような射が圏 C に存在しなければならない。正確に言えば、任意の射 に対して

である。


Haskell の圏 Hask[編集]

この項目で我々が考えようとしている主な圏は、Haskellの型を対象とし、Haskell の関数を射とし、合成として(.)を使う圏 Hask である。型 A から Bの関数 f :: A -> BHask の射である。 この定義が最初の2つの規則を満たすことは容易に確認できる。 すなわち(.) は結合的であり、また任意の fgについて f . g は明らかに何らかの関数である。Hask における恒等射は id であり、次は自明である。 [1]


id . f = f . id = f


ただし、これは添え字を欠いてしまっており、上記の規則の厳密な翻訳ではない。Haskell の関数 id多相的である。すなわちその定義域や値域に異なる様々な型をとることができる、もしくは圏で言い換えれば、異なるソース及びターゲットオブジェクトをとることができる。しかし圏論における射は単相的である。すなわちどんな射もソースオブジェクトとターゲットオブジェクトを1つずつ指定して定義される。多相な Haskell 関数はその型を明示することによって単相化することができる(単相型によるインスタンス化)ため、『Hask圏の型Aに対する恒等射は(id :: A -> A)である』と書けばより正確になる。これを考慮すると、先程の則は次のように書き直せる。


(id :: B -> B) . f = f . (id :: A -> A) = f

しかしながら議論を単純にするため、意味が明らかであるときはこの違いを無視することにする。

演習
  • さきほど触れたとおり、任意の半順序 (P, ) はPの要素を対象、要素 ab について a b であるときかつそのときに限りa, b間に射をもつ圏である。上記の規則のどれがこのの推移性を保証しているか?
  • (難しい) もし上記の例に別の射を付け足すとこれは圏ではなくなる。なぜか?ヒント:合成演算の結合性を考えてみよ。


関手[編集]

ふたつの圏 の間の関手。対象の対応は黄色の、射の対応は青色の破線矢印で示した。注目すべきは対象 A と対象 Bの両方が の同じ対象に対応付けられていることである。それゆえ g はソースとターゲットが同じ対象である射に変換され(これは恒等射である必要はない)、は同じ射となる。


対象と対象を関連付ける射を持つ幾つかの圏を見てきた。圏論の次の大きな話題は圏どうしを関連づける関手(functor、ファンクタ)である。関手の本質は圏の間の変換である。つまり圏CDが与えられたとき、関手 は次のことをする。

  • C 内のあらゆる対象 Aを、D内のに対応付ける
  • C 内の射 D 内の に対応付ける

関手の好例のひとつは忘却関手(forgetful functor) である。これは群をその内在する集合に対応付け、群の射を同様に振る舞うがしかし群の代わりに集合の上で定義される関数に対応付ける。他の例としては冪集合関手 がある。これは集合をその冪集合に対応付け、関数 を関数 、つまり をとり と定義される、 f の下の U の像を返す関数にそれぞれ対応付ける。あらゆる圏 C について、C上の恒等関手として知られる関手、すなわち対象や射をそれ自身に対応付ける、を定義できる。これは後のモナド則の節で便利であることがじきにわかるであろう。 


関手が従わなければならない幾つかの公理を挙げておこう。最初に、任意の対象 A 上の恒等射 について、 は恒等射でなければならない。


ふたつめに、関手は射の合成を分配しなければならない。

演習
右の図において、関手の規則が成り立ってることを確かめよ。

Haskにおける関手[編集]

Haskellでお目にかかったことがあるかもしれない型クラス Functor は、実際に圏論における関手の概念と一致する。関手がふたつの構成要素からなることを思い出そう。関手はある圏の対象を別の圏の対象に対応付け、最初の圏の射をふたつめの圏の射に対応付ける。Haskell の関手は Hask から funcである。ここで func は関手の型の上でちょうど定義されるHaskの部分圏である。例えばリスト関手は Hask から Lstである。ここでLstリスト型、すなわち任意の型Tに対するリスト型[T]のみを含む圏である。Lstにおける射はリスト型の上で定義される関数であり、これは任意の型T, Uに関して [T] -> [U]の関数である。どのようにこれを Haskell のFunctor型クラスへと結びつけたらよいのであろうか?定義を思い出そう。

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> (f a -> f b)

インスタンスの例も示しておこう。

instance Functor Maybe where
  fmap f (Just x) = Just (f x)
  fmap _ Nothing  = Nothing

ここが鍵となる部分である。型構築子 Maybe は任意の型 T をとり新たな型Maybe Tとなる。また、Maybe 型へと狭められた fmap は関数 a -> b をとり関数 Maybe a -> Maybe b を返す。まさにこれがまさにそうではないか!ふたつの構成要素を定義した。ひとつはHaskの対象をとり別の圏(これはMaybe型を対象、Maybe型上の関数を射とする)の対象を返す何か、もうひとつはHask の射をとりこの圏の射を返す何か。ゆえに Maybe は関手である。

Haskellの関手が内容に関してmapできるような型を表すということは有用な直観である。これはリストや Maybeだけでなく、木のようなより複雑な構造もそうである。構造の内容にmapを行う関数はfmapを使って書くことができ、どんな関手構造もこの関数に渡すことができる。例えば、Data.List.map, Data.Map.map, Data.Array.IArray.amap などをすべてをカバーするジェネリックな関数を書くことができる。

関手の公理はどうだろうか?任意のAに対する として多相的な関数 id を使い、最初の則は次のように書ける。

fmap id = id

先程の直観によると、この式は『構造を辿ってしかし各要素に何もしないmapと、全く何もしないことは等しい」と解釈できる。次に、射の合成は単に (.) であり、つまり、

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

このふたつめの則は実用的に極めて役に立つ。関手をリストか何かのコンテナと考えると、右辺は2パスのアルゴリズムを表す。つまり構造についてまずgをmapし、さらにfをmapする。この関手の公理はこのような2パスのアルゴリズムをf . gを行う1パスのアルゴリズムへと変換できることを保証する。この処理は 融合(fusion)として知られている。

演習
リスト関手と Maybe 関手について、これらの規則を確かめよ。

圏論の概念から Haskellへの変換[編集]

関手はどのように圏論が Haskell へと変換されるかの良い例を提供する。次が理解の鍵となる。


  • Hask とその部分圏を扱う。
  • 対象は型である。
  • 射は関数である。
  • 型を取り別の型を返すものが型構成子である。
  • 関数をとり別の関数を返すものが高階関数である。
  • 圏論ではしばしば一度に多くの対象にわたって物事が定義されるという事実を、型クラスとそれが同時に提供する多相性はうまく捉えている。


モナド[編集]

モナドの全ての対象についてunitjoinのふたつの射が存在しなくてはならない。


モナドは言うまでもなく Haskell の極めて重要な概念であるが、実はこれらは本来圏論に由来するものである。モナド は圏から同じ圏への関手であり、さらにいくつかの追加の構造を提供する。では定義を見てみよう。モナドはC内のすべての対象 Xに対してふたつの射をともなう関手 である[2]

議論されているモナドが明らかなとき、これらの関数について上添字 M を省略することにし、単に何らかの X に対するについて述べることにする。


では、どのようにこれを Haskell の型クラス Monad に翻訳されるかをみよう。

class Functor m => Monad m where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

このクラス制約Functor mmがあらかじめ関手の構造、つまり対象と射の対応付けを持っていることを保証する。return は全ての X に対する の(多相的な)類義語である。しかしここには問題がある。returnの型はunitに非常に似ているけれども、もう一方の関数、しばしばbindとも呼ばれる (>>=)の型はjoinに似ていない。ここでさらに別のモナド関数join :: Monad m => m (m a) -> m aがあり、これは非常によく似ている。実際に、join(>>=)は次のように互いに表すことができる。


join :: Monad m => m (m a) -> m a
join x = x >>= id

(>>=) :: Monad m => m a -> (a -> m b) -> m b
x >>= f = join (fmap f x)

つまり、モナドの return, fmap, joinを定義することは、return(>>=)を定義することと同等である。圏論でモナドの定義をする典型的な方法がunitjoinを与えることであるのに対して、Haskell プログラマはreturn(>>=)を与えることを好むことがわかる。[3]多くの場合、圏論の方法のほうが理にかなっている。 何らかの構造があり、任意の対象Xとしたり、とできる自然な方法があるとき、それはしばしばモナドである。次の節で例を示す。


例: 冪集合関手もモナドである[編集]

先ほど述べた冪集合関手 はモナドをなす。任意の集合Sについて、要素をその単集合へ写す がある。これらの単集合のそれぞれは明らかに S の部分集合であり、よってSの冪集合の要素を返す、つまりモナドの要求を満たしている。同様に関数 を次のように定義できる。引数としてをとる。これは、

  • 冪集合の要素はもとの集合の部分集合、すなわち
  • つまり
  • つまりの部分集合の集合。

よってはこれらの部分集合の和を返すことで、Sのまた別の部分集合を与えるようにする。式で表せば、

.

従って、(次の節で探求する規則を満たすことが証明できれば)P はモナドである。

実際のところ、議論の対象が集合の代わりにリストになるという違いを除けば、Pはほとんどリストモナドと等しい。これらはほぼ同じものである。比較してみよう。

Setに対する冪集合関手 Haskellのリストモナド
関数の型 定義 関数の型 定義
集合を S 、射を とする 型を T 、関数を f :: A -> Bとする
fmap f :: [A] -> [B] fmap f xs = [ f a | a <- xs ]
return :: T -> [T] return x = [x]
join :: [[T]] -> [T] join xs = concat xs


モナド則とその重要性[編集]

関手がそう呼ばれるためには従わなければならない公理があるように、モナドにも幾つかそのような公理が存在する。まずはそれらを一覧し、次に Haskell へと翻訳し、なぜそれが重要なのかをみていくことにしよう。

モナド と、に射 があるとする。 このとき次が成り立たなくてはならない。


Haskell への翻訳はなるべく自明であってほしい。

  1. join . fmap join = join . join
  2. join . fmap return = join . return = id
  3. return . f = fmap f . return
  4. join . fmap (fmap f) = fmap f . join

(fmap が関手の構成要素のひとつで、射に作用するものであることを思い出そう。)これらの則は最初は少し不可解にも思える。いったいこれらの則はどういう意味で、なぜモナドはこれを満たすべきなのだろうか?ではこれらの法則について調べていこう。

最初の規則[編集]

join . fmap join = join . join

最初の規則のリスト版の説明。リストモナドでは joinconcat で、fmapmap であることを思い出そう。

この規則を理解するために、まずはリストの例を使っていこう。最初の規則はjoin . fmap join (左辺) と join . join (右辺)のふたつの関数について述べている。これらの型はどうなるだろうか?(今はリストモナドについて議論しているので)joinの型は[[a]] -> [a]であることを思い出そう。つまり両辺の型はどちらも[[[a]]] -> [a]である。(これが同じであるという事実は役に立つ。最終的には、両辺が全く同じ関数であることを示そうとしているのだ。)では、リストのリストのリストがあるとしよう。左辺はこの三重のリストに fmap joinを作用させ(1)、その結果に join を適用する(2)。 fmap はリストに対しては map と同じであるので、(1)の計算はまずいちばん外側のリストの要素に対してjoinmapで施す。各要素に対して、joinはリストのリストそれぞれを連結する。結果としてリストのリストが得られたら、(2)によりこれ全体にjoinを適用する。手短に言えば、トップレベルに'入り込み'、二番目と三番目のレベルを潰してひとつにして、次いでトップレベルとこの新しいレベルを潰してひとつにする。

では右辺についてはどうだろうか?最初にリストのリストのリストに対して join を実行する。普通joinは二重のリストに適用するものであるが、三重のリストにも適用できる。なぜなら、[[[a]]]b = [a]とおけば[[b]]と書けるからである。つまり三重のリストはある意味で二重のリストにすぎない、ただし最深部は'フラット'な値でなく別のリストからなっている。だからもしリストのリスト(のリスト)にjoinを適用すると、外側のふたつのリストがひとつに平坦化される。外から二番目の深さのリストの要素はフラットではなく三番目の層のリストが含まれているので、この結果はリストのリストであり、次にもう一方のjoin がこの構造を平坦化する。要約すると、左辺は内側のふたつの層を新しい層へと平坦化し、それから最も外側と新しい層を平坦化する。右辺は外側のふたつの層をまず平坦化し、それから新しい層と最も内側の層を平坦化する。これらの二つの操作は等しい。これはいわばjoinに関する結合則のようなものである。

次のようにしたMaybe もまたモナドである。

return :: a -> Maybe a
return x = Just x

join :: Maybe (Maybe a) -> Maybe a
join Nothing         = Nothing
join (Just Nothing)  = Nothing
join (Just (Just x)) = Just x

三重の Maybe (これはNothing, Just Nothing, Just (Just Nothing), Just (Just (Just x))といった値をとる)を考えて、一つめの規則は内側のふたつの層を先に潰し、それから外側の層を潰すことは、外側の層が先に潰し、それから最も内側の層を潰すことと全く同じであると述べている。

演習
層の平坦化がどのように働くかを見るために、リストモナドと Maybe モナドがこの規則に確かに従うことを、幾つかの例について確認せよ。

二番目の規則[編集]

join . fmap return = join . return = id

それでは、二番目の法則はどうだろうか?再び、リストの例で始めよう。二番目の法則で述べられている両辺は [a] -> [a]の関数である。左辺はまずリストのそれぞれの要素xを要素がそれひとつだけのリスト[x]へと変え、シングルトンリストのリストを得る。この二重のリストは再びjoinを使って一重のリストへと平坦化される。以上が左辺の表す関数である。一方右辺では、リスト全体[x, y, z, ...]をとり、これをリストのシングルトンリスト[[x, y, z, ...]]にし、それから再びこのふたつの層をひとつに平坦化する。この規則は一言で説明できるほどの自明さはないが、returnをモナドの値に適用しその結果をjoinすることは、returnを最上位の層の内側で実行しても外側で実行しても同じ結果になるべきであるということを本質的に述べている。


演習
Maybe モナドについて、二番目の規則を証明せよ。

3番目と4番目の規則[編集]

return . f = fmap f . return

join . fmap (fmap f) = fmap f . join

最後のふたつの法則は、どのようにモナドが振舞うべきかに関するもっと自明な事実を示す。これがどう真であるかを調べる最も簡単な方法は、展開した形式を使うためにこれらを展開することである。

  1. \x -> return (f x) = \x -> fmap f (return x)
  2. \x -> join (fmap (fmap f) x) = \x -> fmap f (join x)
演習
最初と二番目の規則を説明したのと同様の方法で、それらがどのような意味を持つかを探り、これらの規則がどんなモナドについても成り立つべきであることを確かめよ。

doブロックへの適用[編集]

モナドが従わなければならない規則について直観的に説明した。ではなぜこれは重要なのか?その答えは do ブロックについて考えたときに明らかになる。次のお決まりの変換が示しているように、do ブロックが文の組み合わせを(>>=)を使わずに表すためのただの構文糖衣であることを思い出そう。

do { x }                 -->  x
do { let { y = v }; x }  -->  let y = v in do { x }
do { v <- y; x }         -->  y >>= \v -> do { x }
do { y; x }              -->  y >>= \_ -> do { x }

ここで用いている4つの規則から、通常の return(>>=)を使ったモナド則を証明できることに注意したい。(非常に大掛かりな証明もあるので、ここは飛ばしてしまっても構わない。)


  1. return x >>= f = f x. 証明:
       return x >>= f
     = join (fmap f (return x)) -- (>>=)の定義より
     = join (return (f x))      -- 規則3より
     = (join . return) (f x)
     = id (f x)                 -- 規則2より
     = f x
    
  2. m >>= return = m. 証明:
       m >>= return
     = join (fmap return m)    -- (>>=)の定義より
     = (join . fmap return) m
     = id m                    -- 規則2より
     = m
    
  3. (m >>= f) >>= g = m >>= (\x -> f x >>= g). 証明 (fmap f . fmap g = fmap (f . g)を思い出そう):
       (m >>= f) >>= g
     = (join (fmap f m)) >>= g                          -- (>>=)の定義より
     = join (fmap g (join (fmap f m)))                  -- (>>=)の定義より
     = (join . fmap g) (join (fmap f m))
     = (join . fmap g . join) (fmap f m)
     = (join . join . fmap (fmap g)) (fmap f m)         -- 規則4より
     = (join . join . fmap (fmap g) . fmap f) m
     = (join . join . fmap (fmap g . f)) m              -- 関手の分配則より
     = (join . join . fmap (\x -> fmap g (f x))) m
     = (join . fmap join . fmap (\x -> fmap g (f x))) m -- 規則1より
     = (join . fmap (join . (\x -> fmap g (f x)))) m    -- 関手の分配則より
     = (join . fmap (\x -> join (fmap g (f x)))) m
     = (join . fmap (\x -> f x >>= g)) m                -- (>>=)の定義より
     = join (fmap (\x -> f x >>= g) m)
     = m >>= (\x -> f x >>= g)                          -- (>>=)の定義より
    

return(>>=)を使うこの新たなモナド則は、これをdo記法へと変換できる。


ポイントフリースタイル do記法
return x >>= f = f x do { v <- return x; f v } = do { f x }
m >>= return = m do { v <- m; return v } = do { m }
(m >>= f) >>= g = m >>= (\x -> f x >>= g)
   do { y <- do { x <- m; f x };
        g y }
 =
   do { x <- m;
        y <- f x;
        g y }

モナド則はいまやdoブロックがどのように機能すべきかという常識を述べた文である。もしこれらの規則がひとつでも無効であれば、doブロックを期待したとおりに操作できなくなるのでユーザが混乱する。要するに、モナド則はユーザビリティガイドラインなのである。


演習

規則をここでは2バージョン示した。

-- 圏論的:
join . fmap join = join . join
join . fmap return = join . return = id
return . f = fmap f . return
join . fmap (fmap f) = fmap f . join

-- 関数的:
m >>= return = m
return m >>= f = f m
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

これらは全く同等である。圏論的な規則から関数的な規則を作る方法は示した。逆をやってみよう。関数的な規則から始めて、圏論の規則が満たされることを示せ。以下の定義を思い出すと役に立つ。

join m = m >>= id
fmap f m = m >>= return . f
この問題を薦めてくれた Yitzchak Gale に感謝する。

まとめ[編集]

この章で長い道のりを辿ってきた。圏とは何か、どうやってHaskellに応用されるのかを見てきた。関手をはじめとする圏論の基本的な概念から、モナドのようなより発展的な内容まで、それらがいかにHaskellらしさに必要不可欠であるかについても紹介してきた。自然変換(natural transformations)など、我々の目的に必要なかった幾つかの圏論の基本的事項については触れなかったが、代わりにHaskellの構造の背後に根付く圏論の直観的な理解を提供した。


注釈[編集]

  1. ^ 実はここには微妙な部分が存在する。(.)は遅延評価関数であるため、もしfundefinedであるとid . f = \_ -> _|_となる。さて、全ての意図と目的においてこれは_|_と等しいように見えるかもしれないが、実は正格化関数seqを使うことでこれらを区別することができる。これは圏の最後の規則が破られることを意味する。新たに正格な合成関数f .! g = ((.) $! f) $! gを定義すればHaskを正しく圏にすることもできる。しかしここでは普通の(.)を使って進めていくことにする。全ての矛盾は seqが良い言語の性質をひどく破壊するということのせいにしておく。
  2. ^ 熟達した圏論の理論家は、ここで少し単純化していることに気付くだろう。unitjoinを自然変換(natural transformations)として導入する代わりに、これらを明示的に射として扱った。そしてnaturalityをモナド則の規則3と規則4として追加した。ここでは圏論全体を教えようとしているわけではなく、Haskellのある構造に対する理論的裏付けとしての圏論だけを示したいために、このような単純化を行った。これらの射にHaskellで対応するものを連想させる名前を与えていることに気付く読者もいるかも知れない。これは名前が直感的でないためである。
  3. ^ これはおそらく、圏論では様々な構造のコンテナとしての側面に重点が置かれるのに対して、Haskellプログラマはモナドを共通する機能を持つ計算を連鎖させる方法と考えることを好むことが原因であろう。joinはコンテナのふたつの層をひとつに潰すという意味でコンテナと自然に関連し、対して(>>=)は何かを行い、その結果を何かに与えるという意味で計算を連鎖させる自然な演算子である。

テンプレート:Haskell navigation