Nuprl Definition : monad
This definition of monad is the one that functional programmers use.
There is a categorical definition of monad in the section on category theory,
and a proof that from a monad as defined here, one can construct a 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 m return) = m ∈ (M T))
× (∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].
((bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U)))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
apply: f a,
lambda: λx.A[x],
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = 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: s = t ∈ T,
lambda: λx.A[x],
apply: f a
FDL editor aliases :
monad
Latex:
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