Nuprl Definition : monad

This definition of monad is the one that functional programmers use.
There is categorical  definition of monad in the section on category theory,
and proof that from monad as defined here, one can construct category
theoretical monad over the category of Types.⋅

Monad ==
  M:Type ⟶ Type
  × return:⋂T:Type. (T ⟶ (M T))
  × bind:⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
  × leftunit:∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)].  ((bind (return x) f) (f x) ∈ (M S))
  × rightunit:∀[T:Type]. ∀[m:M T].  ((bind return) m ∈ (M T))
  × (∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].
       ((bind (bind f) g) (bind x.(bind (f x) g))) ∈ (M U)))

Definitions occuring in Statement :  uall: [x:A]. B[x] apply: a lambda: λx.A[x] isect: x:A. B[x] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type equal: t ∈ T
Definitions occuring in definition :  isect: x:A. B[x] product: x:A × B[x] universe: Type uall: [x:A]. B[x] function: x:A ⟶ B[x] equal: t ∈ T lambda: λx.A[x] apply: a
FDL editor aliases :  monad

Monad  ==
    M:Type  {}\mrightarrow{}  Type
    \mtimes{}  return:\mcap{}T:Type.  (T  {}\mrightarrow{}  (M  T))
    \mtimes{}  bind:\mcap{}T,S:Type.    ((M  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (M  S))  {}\mrightarrow{}  (M  S))
    \mtimes{}  leftunit:\mforall{}[T,S:Type].  \mforall{}[x:T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].    ((bind  (return  x)  f)  =  (f  x))
    \mtimes{}  rightunit:\mforall{}[T:Type].  \mforall{}[m:M  T].    ((bind  m  return)  =  m)
    \mtimes{}  (\mforall{}[T,S,U:Type].  \mforall{}[m:M  T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].  \mforall{}[g:S  {}\mrightarrow{}  (M  U)].
              ((bind  (bind  m  f)  g)  =  (bind  m  (\mlambda{}x.(bind  (f  x)  g)))))

Date html generated: 2017_01_19-PM-02_31_09
Last ObjectModification: 2017_01_17-PM-06_06_53

Theory : monads

Home Index