Mercurial > urweb
annotate lib/ur/monad.urs @ 915:5e8b6fa5b48f
Start 'more' demo with dbgrid
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 08 Sep 2009 07:48:57 -0400 |
parents | 8e540df3294d |
children | 321a2d6feb40 |
rev | line source |
---|---|
adamc@834 | 1 val exec : m ::: (Type -> Type) -> monad m -> ts ::: {Type} |
adamc@834 | 2 -> $(map m ts) -> folder ts -> m $ts |
adamc@898 | 3 |
adamc@898 | 4 val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type |
adamc@898 | 5 -> m t -> m unit |
adamc@905 | 6 |
adamc@905 | 7 val foldR : K --> m ::: (Type -> Type) -> monad m |
adamc@905 | 8 -> tf :: (K -> Type) |
adamc@905 | 9 -> tr :: ({K} -> Type) |
adamc@905 | 10 -> (nm :: Name -> t :: K -> rest :: {K} |
adamc@905 | 11 -> [[nm] ~ rest] => |
adamc@905 | 12 tf t -> tr rest -> m (tr ([nm = t] ++ rest))) |
adamc@905 | 13 -> tr [] |
adamc@905 | 14 -> r :: {K} -> folder r -> $(map tf r) -> m (tr r) |
adamc@905 | 15 |
adamc@905 | 16 val foldR2 : K --> m ::: (Type -> Type) -> monad m |
adamc@905 | 17 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) |
adamc@905 | 18 -> tr :: ({K} -> Type) |
adamc@905 | 19 -> (nm :: Name -> t :: K -> rest :: {K} |
adamc@905 | 20 -> [[nm] ~ rest] => |
adamc@905 | 21 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) |
adamc@905 | 22 -> tr [] |
adamc@905 | 23 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) |
adamc@905 | 24 |
adamc@910 | 25 val foldR3 : K --> m ::: (Type -> Type) -> monad m |
adamc@910 | 26 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) |
adamc@910 | 27 -> tr :: ({K} -> Type) |
adamc@910 | 28 -> (nm :: Name -> t :: K -> rest :: {K} |
adamc@910 | 29 -> [[nm] ~ rest] => |
adamc@910 | 30 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) |
adamc@910 | 31 -> tr [] |
adamc@910 | 32 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) |
adamc@910 | 33 |
adamc@905 | 34 val mapR : K --> m ::: (Type -> Type) -> monad m |
adamc@905 | 35 -> tf :: (K -> Type) |
adamc@905 | 36 -> tr :: (K -> Type) |
adamc@905 | 37 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) |
adamc@905 | 38 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) |