diff options
-rw-r--r-- | lib/ur/list.ur | 13 | ||||
-rw-r--r-- | lib/ur/list.urs | 2 | ||||
-rw-r--r-- | lib/ur/monad.ur | 7 | ||||
-rw-r--r-- | lib/ur/monad.urs | 7 | ||||
-rw-r--r-- | tests/monad.urp | 3 | ||||
-rw-r--r-- | tests/monadTest.ur | 3 |
6 files changed, 35 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 2d5addc9..bce5335e 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -424,3 +424,16 @@ fun drop [a] (n : int) (xs : list a) : list a = fun splitAt [a] (n : int) (xs : list a) : list a * list a = (take n xs, drop n xs) + +fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) = + let + fun mapXiM' i ls = + case ls of + [] => return <xml/> + | x :: ls => + this <- f i x; + rest <- mapXiM' (i+1) ls; + return <xml>{this}{rest}</xml> + in + mapXiM' 0 + end diff --git a/lib/ur/list.urs b/lib/ur/list.urs index 15204590..b26c9ad9 100644 --- a/lib/ur/list.urs +++ b/lib/ur/list.urs @@ -36,6 +36,8 @@ val mapPartialM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> val mapXM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit} -> (a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] []) +val mapXiM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit} -> (int -> a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] []) + val filter : a ::: Type -> (a -> bool) -> t a -> t a val exists : a ::: Type -> (a -> bool) -> t a -> bool 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) diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs index d07d5026..ce823f4a 100644 --- a/lib/ur/monad.urs +++ b/lib/ur/monad.urs @@ -7,6 +7,13 @@ val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type val mp : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> b) -> m a -> m b +val liftM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type + -> (a -> b) -> m a -> m b +(* Haskell-style synonym for [mp] *) + +val liftM2 : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> c ::: Type + -> (a -> b -> c) -> m a -> m b -> m c + val foldR : K --> m ::: (Type -> Type) -> monad m -> tf :: (K -> Type) -> tr :: ({K} -> Type) diff --git a/tests/monad.urp b/tests/monad.urp new file mode 100644 index 00000000..91523ca2 --- /dev/null +++ b/tests/monad.urp @@ -0,0 +1,3 @@ +$/monad +$/list +monadTest diff --git a/tests/monadTest.ur b/tests/monadTest.ur new file mode 100644 index 00000000..16a10f74 --- /dev/null +++ b/tests/monadTest.ur @@ -0,0 +1,3 @@ +val x : transaction int = Monad.liftM2 plus (return 1) (return 2) + +val x : transaction xbody = List.mapXiM (fn i x => return <xml><li>{[i]} = {[x]}</li></xml>) (1 :: 2 :: []) |