めもめも

このブログに記載の内容は個人の見解であり、必ずしも所属組織の立場、戦略、意見を代表するものではありません。

Haskell の Monad を圏論の Monad と対比する (1)

定義

Haskell 圏 : H

Objects O := "Haskell で定義される type の集合"
           = {Int, Char, String, (Int -> Int), ....}
Morphisms M := "Haskell で定義される全ての関数の集合"

Haskell の Monad m から誘導される Endofunctor T

Object mapping   T_O: Type -> m Type
Morphism mapping T_M: f -> ( >>= return . f)

定理

以下の Monad 則に従う場合、(T, return, >>=) は Kleisli triple を構成する。

return a >>= k == ka
m >>= return == m
m >>= (\x -> (k x >>= h)) == (m >>= k) >>= h

証明は省略。。。。Monad 則より、演算子 >>= は、return を恒等元とする monoid になる。

命題

Id を identity endofunctor として、Transformations η : Id -> T, μ : T^2 -> T を次のように定義する。

   μ : T^2 A ---> T A
          x |----> x >>= (\y -> y)

   η :  A -----> T A
         x |----> return x

この時、上記は natural transformation となり、トリプレット (T, η, μ)は、圏論における monad を構成する。(証明は略。。。)

メモ

いまさらですが・・・、Haskell のモナドの心は、集合 A = {type} の上の演算を集合 mA = {m type} の上の演算に写像することで、オリジナルの集合にはなかった追加の構造を導入して、演算を拡張することです。

例えば、

IO Monad => IO の副作用を追加の構造に持たせた世界に演算を拡張します。
Maybe Monad => オリジナルの世界では fail する可能性のある演算を fail しない世界に拡張します。
State Monad => ステート情報を追加の構造に持たせて、合成演算の間でやりとりします。