PS

Haskell-monad

圏論 Haskell Monad

Haskell-monad

Monad laws - HaskellWikiより、Haskell-monad:

  • (T, {\tt return}, {\tt >>=})

とは、

  • endofunctor: T : \mathcal{Hask} \to \mathcal{Hask}
  • natural transformation: ({\tt return} _ a : a \to T a) _ a *1
  • 関数族: ({\tt >>=} _{a, b} : T a \to (a \to T b) \to T b) _ {a, b}

で、left identity則、right identity則、associativity則、および

を満たすものとする。

命題

MonadとHaskell-monadは同値。

Endofunctor:

  • T : \mathcal{Hask} \to \mathcal{Hask}

について、

  • \lbrace (\eta, \mu) \mid (T, \eta, \mu) : \text{monad} \rbrace
    • \cong \lbrace ({\tt return}, {\tt >>=}) \mid (T, {\tt return}, {\tt >>=}): \text{Haskell-monad} \rbrace

\mathcal{Set} でも同様。

証明

  • (\eta, \mu) \mapsto
    • {\tt return} := \eta
    • (m : T a)\ {\tt >>=} _ {a, b}\ (k : a \to T b) := \mu _ b( (T(k)(m) )
  • ({\tt return}, {\tt >>=}) \mapsto
    • \eta := {\tt return}
    • \mu _ a(m : T ^ 2 a) := m\ {\tt >>=}\ 1 _ {T a}

これらの対応は互いにinverse。

Free theoremがないと証明できない(と思う)ので、 \mathcal{Set} では同値にならない(と思う)。

参考文献

*1:free theoremを想定する場合、関数族で十分

*2:free theoremを想定する場合、fmapの一意性 - PSより必ず成立する