Mercurial > urweb

comparison lib/ur/monad.urs @ 1093:8d3aa6c7cee0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make summary unification more conservative; infer implicit arguments after applications
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Dec 2009 11:56:40 -0500
parents 37dd42935dad
children ad15700272f6
comparison
equal deleted inserted replaced
1092:6f4b05fc4361 1093:8d3aa6c7cee0
12 -> tr :: ({K} -> Type) 12 -> tr :: ({K} -> Type)
13 -> (nm :: Name -> t :: K -> rest :: {K} 13 -> (nm :: Name -> t :: K -> rest :: {K}
14 -> [[nm] ~ rest] => 14 -> [[nm] ~ rest] =>
15 tf t -> tr rest -> m (tr ([nm = t] ++ rest))) 15 tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
16 -> tr [] 16 -> tr []
17 -> r :: {K} -> folder r -> $(map tf r) -> m (tr r) 17 -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r)
18 18
19 val foldR2 : K --> m ::: (Type -> Type) -> monad m 19 val foldR2 : K --> m ::: (Type -> Type) -> monad m
20 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 20 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
21 -> tr :: ({K} -> Type) 21 -> tr :: ({K} -> Type)
22 -> (nm :: Name -> t :: K -> rest :: {K} 22 -> (nm :: Name -> t :: K -> rest :: {K}
23 -> [[nm] ~ rest] => 23 -> [[nm] ~ rest] =>
24 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) 24 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
25 -> tr [] 25 -> tr []
26 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) 26 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
27 27
28 val foldR3 : K --> m ::: (Type -> Type) -> monad m 28 val foldR3 : K --> m ::: (Type -> Type) -> monad m
29 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) 29 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
30 -> tr :: ({K} -> Type) 30 -> tr :: ({K} -> Type)
31 -> (nm :: Name -> t :: K -> rest :: {K} 31 -> (nm :: Name -> t :: K -> rest :: {K}
32 -> [[nm] ~ rest] => 32 -> [[nm] ~ rest] =>
33 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) 33 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
34 -> tr [] 34 -> tr []
35 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) 35 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
36 36
37 val mapR : K --> m ::: (Type -> Type) -> monad m 37 val mapR : K --> m ::: (Type -> Type) -> monad m
38 -> tf :: (K -> Type) 38 -> tf :: (K -> Type)
39 -> tr :: (K -> Type) 39 -> tr :: (K -> Type)
40 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) 40 -> (nm :: Name -> t :: K -> tf t -> m (tr t))
41 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) 41 -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
42 42
43 val mapR2 : K --> m ::: (Type -> Type) -> monad m 43 val mapR2 : K --> m ::: (Type -> Type) -> monad m
44 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 44 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
45 -> tr :: (K -> Type) 45 -> tr :: (K -> Type)
46 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) 46 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
47 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) 47 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))