メモ

Haskell

Haskellのモナドの話には圏論の言葉がよく出てくるのですが、ざっくりとした理解しかできていません。自分の理解をまとめるためにメモを残します。間違っているかもしれないので、鵜呑みにはしないでください。圏論はなんとなく集合論をさらに抽象化したような印象です。

  • 圏は対象と、対象から対象への射を持った構造
  • 関手はある圏ともう1つの圏の間で、対象を対象に写し、射を射に写す
  • その際、恒等な射と、射の結合法則を保存しなければいけない

これは、HaskellのFunctorにあてはめると以下のようになります。

  • Haskellのすべての型の値を対象として、関数を射とすることで、圏にできる
  • 関手はFunctorの値コンストラクタとfmapで、これで写すことで、Haskellのすべての型の圏はFunctorの圏に対応させることができる
  • 関手で写す前後の、恒等な射と、射の結合法則の保存は、Functor則そのもの
fmap id ≡ id
fmap (p . q) ≡ (fmap p) . (fmap q)

HaskellのMonadについてはもう少し複雑で、Haskellのすべての型の圏からMonadの圏への関手 (MonadもHaskellの型なので、自分から自分への自己関手になる) が、自然変換を射とすることでまた圏を為し、この関手の圏において、モノイドの性質を持つような対象であるMonadの値コンストラクタ (と自然変換の組) がモナドです。

  • Haskellのすべての型の値を対象として、関数を射とすることで、圏にできる
  • Monadの値コンストラクタを関手とすることで、Haskellのすべての型の圏はMonadの圏に対応させることができる
  • この関手であるMonad (の値コンストラクタ, 以下では省略) に対して、自然変換を射として導入することで、圏にできる
  • 自然変換は構造を保存したままMonadをMonadに写すような変換で、ここでは恒等関手をMonadに写すような変換returnと、Monadによって写したMonadを、Monadに写すような変換join
return :: a -> m a -- 自身に対応させる (何もしない) 関手を、mに写す関手に変換していると捉えられる
join :: m (m a) -> m a

return x >>= f ≡ f x
m >>= return ≡ m
(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
  • joinはbindと以下のように変換できるので、bindをつなげていくことは、Monadの適用を繰り返していくことに等しくなる。
m >>= f ≡ join $ fmap f m

まとめるとMonadの値コンストラクタはHaskellのすべての型の圏からMonadの圏への関手で、この関手自体が自然変換returnとjoinを射として圏をなし、モノイドの性質を持っています。モノイドなのでどこから演算を始めても結果は変わりません。

意識していませんでしたが、ここでは、型クラスFunctorやMonadのインスタンスである型の値が対象である圏をそれぞれFunctorの圏やMonadの圏と呼んでいます。値コンストラクタについても同様です。

自分の語彙の使用は正確ではないかもしれない…。もっと正確で詳細な内容が知りたい方はこちらなどをご参照ください。
Haskell/圏論 - Wikibooks