Nuprl Definition : monad-from
monad-from(Mnd) ==
mk-monad(functor(ob(T) = M-map(Mnd) T;
arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));
λx.M-return(Mnd);
λx,z. (M-bind(Mnd) z (λx.x)))
Definitions occuring in Statement :
M-bind: M-bind(Mnd),
M-return: M-return(Mnd),
M-map: M-map(mnd),
mk-monad: mk-monad,
mk-functor: mk-functor,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
M-map: M-map(mnd),
M-return: M-return(Mnd),
apply: f a,
M-bind: M-bind(Mnd),
lambda: λx.A[x]
FDL editor aliases :
monad-from
Latex:
monad-from(Mnd) ==
mk-monad(functor(ob(T) = M-map(Mnd) T;
arrow(X,Y,f) = \mlambda{}z.(M-bind(Mnd) z (\mlambda{}x.(M-return(Mnd) (f x)))));
\mlambda{}x.M-return(Mnd);
\mlambda{}x,z. (M-bind(Mnd) z (\mlambda{}x.x)))
Date html generated:
2020_05_20-AM-08_03_59
Last ObjectModification:
2020_01_16-PM-05_25_08
Theory : bags
Home
Index