PS

Monadはapplicative

命題

Haskell-monad:

  •  (T : \mathcal{Hask} \to \mathcal{Hask}, {\tt return}, {\tt >>=} )

について、

  •  {\tt pure} := {\tt return}
  •  mf\ {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}}\ mx := mf\ {\tt >>=}\ f \mapsto (mx\ {\tt >>=}\ {\tt return} \circ f)

とすると、

  •  (T, {\tt pure}, {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}})

は、applicative。

  • monoidal category:  (\mathcal{Set}, \times, { \lbrace \ast \rbrace } )
  • monad:  (T : \mathcal{Set} \to \mathcal{Set}, \eta, \mu)

について、

  •  \sigma _ {A, B} (x, y) :=  \mu _ {A, B} ( T \big( a \mapsto T( b \mapsto (a, b) )(y) \big) \big(x \big) )
  •  u := \eta _ { \lbrace \ast \rbrace }

とすると、 (T, \sigma, u) はmonoidal endofunctor on  (\mathcal{Set}, \times, { \lbrace \ast \rbrace } ) になる(と思う)。

参考文献