定義
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 => ステート情報を追加の構造に持たせて、合成演算の間でやりとりします。