Mercurial > urweb
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) |