aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/monad.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-05-19 11:32:12 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-05-19 11:32:12 -0400
commitdf475a9256347564d3adc1fafc53c4d93b4e73f7 (patch)
tree04d2d95798a412261154293e71323e4069718bf6 /lib/ur/monad.ur
parent597f9bd0cee0f60fb7dd23d14c6125f5eb6d3f5d (diff)
Some standard library additions from Edward Z. Yang
Diffstat (limited to 'lib/ur/monad.ur')
-rw-r--r--lib/ur/monad.ur7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/ur/monad.ur b/lib/ur/monad.ur
index 3d03298e..ab7742fe 100644
--- a/lib/ur/monad.ur
+++ b/lib/ur/monad.ur
@@ -12,6 +12,8 @@ fun mp [m] (_ : monad m) [a] [b] f m =
v <- m;
return (f v)
+val liftM = @@mp
+
fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
@@ -122,3 +124,8 @@ fun appR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K
f [nm] [t] r1.nm r2.nm r3.nm)
(fn _ _ _ => return ())
fl
+
+fun liftM2 [m ::: Type -> Type] (_ : monad m) [a] [b] [c] (f : a -> b -> c) (mx : m a) (my : m b) : m c =
+ x <- mx;
+ y <- my;
+ return (f x y)