Mercurial > urweb

comparison lib/ur/monad.urs @ 1175:79f487f51d9f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monad.foldMapR
author Adam Chlipala <adamc@hcoop.net>
date Tue, 02 Mar 2010 10:33:49 -0500
parents ad15700272f6
children fd1a49b51db5
comparison
equal deleted inserted replaced
1174:9df124fcab3d 1175:79f487f51d9f
48 val mapR2 : K --> m ::: (Type -> Type) -> monad m 48 val mapR2 : K --> m ::: (Type -> Type) -> monad m
49 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 49 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
50 -> tr :: (K -> Type) 50 -> tr :: (K -> Type)
51 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) 51 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
52 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) 52 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
53
54 val foldMapR : K --> m ::: (Type -> Type) -> monad m
55 -> tf :: (K -> Type)
56 -> tf' :: (K -> Type)
57 -> tr :: ({K} -> Type)
58 -> (nm :: Name -> t :: K -> rest :: {K}
59 -> [[nm] ~ rest] =>
60 tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest)))
61 -> tr []
62 -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tf' r) * tr r)