comparison lib/ur/monad.ur @ 1768:a613cae954ca

Some standard library additions from Edward Z. Yang
author Adam Chlipala <adam@chlipala.net>
date Sat, 19 May 2012 11:32:12 -0400
parents 18d18a70821e
children cbd294994c69
comparison
equal deleted inserted replaced
1766:92cfc69419bd 1768:a613cae954ca
9 fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return () 9 fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
10 10
11 fun mp [m] (_ : monad m) [a] [b] f m = 11 fun mp [m] (_ : monad m) [a] [b] f m =
12 v <- m; 12 v <- m;
13 return (f v) 13 return (f v)
14
15 val liftM = @@mp
14 16
15 fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type] 17 fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
16 (f : nm :: Name -> t :: K -> rest :: {K} 18 (f : nm :: Name -> t :: K -> rest :: {K}
17 -> [[nm] ~ rest] => 19 -> [[nm] ~ rest] =>
18 tf t -> tr rest -> m (tr ([nm = t] ++ rest))) 20 tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
120 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 => 122 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
121 acc (r1 -- nm) (r2 -- nm) (r3 -- nm); 123 acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
122 f [nm] [t] r1.nm r2.nm r3.nm) 124 f [nm] [t] r1.nm r2.nm r3.nm)
123 (fn _ _ _ => return ()) 125 (fn _ _ _ => return ())
124 fl 126 fl
127
128 fun liftM2 [m ::: Type -> Type] (_ : monad m) [a] [b] [c] (f : a -> b -> c) (mx : m a) (my : m b) : m c =
129 x <- mx;
130 y <- my;
131 return (f x y)