Ur/Web: lib/ur/monad.urs annotate

Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 09 Aug 2009 16:13:27 -0400
parents	d1d0b18afd3d
children	8e540df3294d

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@905	25 val mapR : K --> m ::: (Type -> Type) -> monad m
adamc@905	26 -> tf :: (K -> Type)
adamc@905	27 -> tr :: (K -> Type)
adamc@905	28 -> (nm :: Name -> t :: K -> tf t -> m (tr t))
adamc@905	29 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))

Mercurial > urweb