Filters implementation type-checking

7 files changed, 303 insertions, 156 deletions

diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
index 04eb6dc5..59214348 100644
--- a/demo/more/dbgrid.ur
+++ b/demo/more/dbgrid.ur
@@ -2,17 +2,20 @@ con rawMeta = fn t :: Type =>
                  {New : transaction t,
                   Inj : sql_injectable t}
 
-con colMeta' = fn (row :: {Type}) (t :: Type) =>
+con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
                   {Header : string,
-                   Project : $row -> transaction t,
-                   Update : $row -> t -> transaction ($row),
-                   Display : t -> xbody,
-                   Edit : t -> xbody,
-                   Validate : t -> signal bool}
-
-con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
-                 {Initialize : transaction global_t.1,
-                  Handlers : global_t.1 -> colMeta' row global_t.2}
+                   Project : $row -> transaction input,
+                   Update : $row -> input -> transaction ($row),
+                   Display : input -> xbody,
+                   Edit : input -> xbody,
+                   Validate : input -> signal bool,
+                   CreateFilter : transaction filter,
+                   DisplayFilter : filter -> xbody,
+                   Filter : filter -> $row -> signal bool}
+
+con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
+                 {Initialize : transaction global_input_filter.1,
+                  Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
 
 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
                        {Initial : acc,
@@ -20,22 +23,26 @@ con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
                         Display : acc -> xbody}
 
 structure Direct = struct
-    con metaBase = fn actual_input :: (Type * Type) =>
-                  {Display : actual_input.2 -> xbody,
-                   Edit : actual_input.2 -> xbody,
-                   Initialize : actual_input.1 -> transaction actual_input.2,
-                   Parse : actual_input.2 -> signal (option actual_input.1)}
-
-    datatype metaBoth actual input =
-             NonNull of metaBase (actual, input) * metaBase (option actual, input)
-           | Nullable of metaBase (actual, input)
-
-    con meta = fn global_actual_input :: (Type * Type * Type) =>
-                  {Initialize : transaction global_actual_input.1,
-                   Handlers : global_actual_input.1
-                              -> metaBoth global_actual_input.2 global_actual_input.3}
-
-    con editableState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
+    con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
+                  {Display : actual_input_filter.2 -> xbody,
+                   Edit : actual_input_filter.2 -> xbody,
+                   Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
+                   Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
+                   CreateFilter : transaction actual_input_filter.3,
+                   DisplayFilter : actual_input_filter.3 -> xbody,
+                   Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
+
+    datatype metaBoth actual input filter =
+             NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
+           | Nullable of metaBase (actual, input, filter)
+
+    con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
+                  {Initialize : transaction global_actual_input_filter.1,
+                   Handlers : global_actual_input_filter.1
+                              -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
+                                          global_actual_input_filter.4}
+
+    con editableState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
     fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
                                                                                      (editableState ts) =
        let
@@ -48,7 +55,10 @@ structure Direct = struct
                                                 | Some v => r -- nm ++ {nm = v}),
                           Display = mr.Display,
                           Edit = mr.Edit,
-                          Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo)}
+                          Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
+                          CreateFilter = mr.CreateFilter,
+                          DisplayFilter = mr.DisplayFilter,
+                          Filter = fn i r => mr.Filter i r.nm}
        in
            {Initialize = m.Initialize,
             Handlers = fn data => case m.Handlers data of
@@ -56,7 +66,7 @@ structure Direct = struct
                                 | Nullable mr => doMr mr}
        end
         
-    con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
+    con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
     fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
                                                                                      (readOnlyState ts) =
        let
@@ -65,7 +75,10 @@ structure Direct = struct
                           Update = fn r _ => return r,
                           Display = mr.Display,
                           Edit = mr.Display,
-                          Validate = fn _ => return True}
+                          Validate = fn _ => return True,
+                          CreateFilter = mr.CreateFilter,
+                          DisplayFilter = mr.DisplayFilter,
+                          Filter = fn i r => mr.Filter i r.nm}
        in
            {Initialize = m.Initialize,
             Handlers = fn data => case m.Handlers data of
@@ -73,22 +86,30 @@ structure Direct = struct
                                     | Nullable mr => doMr mr}
        end
 
-    con metaBasic = fn actual_input :: (Type * Type) =>
-                       {Display : actual_input.2 -> xbody,
-                        Edit : source actual_input.2 -> xbody,
-                        Initialize : actual_input.1 -> actual_input.2,
-                        InitializeNull : actual_input.2,
-                        IsNull : actual_input.2 -> bool,
-                        Parse : actual_input.2 -> option actual_input.1}
+    con metaBasic = fn actual_input_filter :: (Type * Type * Type) =>
+                       {Display : actual_input_filter.2 -> xbody,
+                        Edit : source actual_input_filter.2 -> xbody,
+                        Initialize : actual_input_filter.1 -> actual_input_filter.2,
+                        InitializeNull : actual_input_filter.2,
+                        IsNull : actual_input_filter.2 -> bool,
+                        Parse : actual_input_filter.2 -> option actual_input_filter.1,
+                        CreateFilter : actual_input_filter.3,
+                        DisplayFilter : source actual_input_filter.3 -> xbody,
+                        Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool,
+                        FilterIsNull : actual_input_filter.3 -> bool}
 
     con basicState = source
-    fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) =
+    con basicFilter = source
+    fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) =
         {Initialize = return (),
          Handlers = fn () => NonNull (
                              {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
                               Edit = m.Edit,
                               Initialize = fn v => source (m.Initialize v),
-                              Parse = fn s => v <- signal s; return (m.Parse v)},
+                              Parse = fn s => v <- signal s; return (m.Parse v),
+                              CreateFilter = source m.CreateFilter,
+                              DisplayFilter = m.DisplayFilter,
+                              Filter = fn f v => f <- signal f; return (m.Filter f v)},
                              {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
                               Edit = m.Edit,
                               Initialize = fn v => source (case v of
@@ -100,9 +121,18 @@ structure Direct = struct
                                                  else
                                                      case m.Parse v of
                                                          None => None
-                                                       | Some v' => Some (Some v'))})}
-
-    fun nullable [global] [actual] [input] (m : meta (global, actual, input)) =
+                                                       | Some v' => Some (Some v')),
+                              CreateFilter = source m.CreateFilter,
+                              DisplayFilter = m.DisplayFilter,
+                              Filter = fn f v => f <- signal f;
+                                          return (if m.FilterIsNull f then
+                                                      Option.isNone v
+                                                  else
+                                                      case v of
+                                                          None => False
+                                                        | Some v => m.Filter f v) : signal bool})}
+
+    fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) =
         {Initialize = m.Initialize,
          Handlers = fn d => case m.Handlers d of
                                 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml>
@@ -110,33 +140,62 @@ structure Direct = struct
 
     type intGlobal = unit
     type intInput = basicState string
-    val int : meta (intGlobal, int, intInput) =
+    type intFilter = basicFilter string
+    val int : meta (intGlobal, int, intInput, intFilter) =
         basic {Display = fn s => <xml>{[s]}</xml>,
                Edit = fn s => <xml><ctextbox source={s}/></xml>,
                Initialize = fn n => show n,
                InitializeNull = "",
                IsNull = eq "",
-               Parse = fn v => read v}
+               Parse = fn v => read v,
+               CreateFilter = "",
+               DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
+               Filter = fn s n =>
+                           case read s of
+                               None => True
+                             | Some n' => n' = n,
+               FilterIsNull = eq ""}
 
     type stringGlobal = unit
     type stringInput = basicState string
-    val string : meta (stringGlobal, string, stringInput) =
+    type stringFilter = basicFilter string
+    val string : meta (stringGlobal, string, stringInput, stringFilter) =
         basic {Display = fn s => <xml>{[s]}</xml>,
                Edit = fn s => <xml><ctextbox source={s}/></xml>,
                Initialize = fn s => s,
                InitializeNull = "",
                IsNull = eq "",
-               Parse = fn s => Some s}
+               Parse = fn s => Some s,
+               CreateFilter = "",
+               DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
+               Filter = fn s n =>
+                           case read s of
+                               None => True
+                             | Some n' => n' = n,
+               FilterIsNull = eq ""}
 
     type boolGlobal = unit
     type boolInput = basicState bool
-    val bool : meta (boolGlobal, bool, boolInput) =
+    type boolFilter = basicFilter string
+    val bool : meta (boolGlobal, bool, boolInput, boolFilter) =
         basic {Display = fn b => <xml>{[b]}</xml>,
                Edit = fn s => <xml><ccheckbox source={s}/></xml>,
                Initialize = fn b => b,
                InitializeNull = False,
                IsNull = fn _ => False,
-               Parse = fn b => Some b}
+               Parse = fn b => Some b,
+               CreateFilter = "",
+               DisplayFilter = fn s => <xml><cselect source={s}>
+                 <coption/>
+                 <coption value="0">False</coption>
+                 <coption value="1">True</coption>
+               </cselect></xml> : xbody,
+               Filter = fn s b =>
+                           case s of
+                               "0" => b = False
+                             | "1" => b = True
+                             | _ => True,
+               FilterIsNull = eq ""}
 
     functor Foreign (M : sig
                          con row :: {Type}
@@ -152,8 +211,9 @@ structure Direct = struct
                      end) = struct
         open M
 
-        con global = list (t * string)
-        con input = source string * option (t * $row)
+        type global = list (t * string)
+        type input = source string * option (t * $row)
+        type filter = source string
 
         val getChoices = List.mapQuery (SELECT * FROM tab AS T)
                                        (fn r => (r.T.nm, render r.T))
@@ -162,7 +222,7 @@ structure Direct = struct
             r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]});
             return r.T
 
-        val meta : meta (global, M.t, input) =
+        val meta : meta (global, M.t, input, filter) =
             {Initialize = getChoices,
              Handlers = fn choices =>
                            NonNull (
@@ -182,7 +242,19 @@ structure Direct = struct
                             Initialize = fn k => s <- source (show k);
                                             r <- rpc (getChoice k);
                                             return (s, Some (k, r)),
-                            Parse = fn (s, _) => k <- signal s; return (read k : option t)},
+                            Parse = fn (s, _) => k <- signal s; return (read k : option t),
+                            CreateFilter = source "",
+                            DisplayFilter = fn s => 
+                                               <xml><cselect source={s}>
+                                                 <coption/>
+                                                 {List.mapX (fn (k, rend) =>
+                                                                <xml><coption value={show k}>{[rend]}</coption></xml>)
+                                                            choices}
+                                               </cselect></xml> : xbody,
+                            Filter = fn s k => s <- signal s;
+                                        return (case read s : option t of
+                                                    None => True
+                                                  | Some k' => k' = k)},
                            {Display = fn (_, kr) => case kr of
                                                           None => <xml>NULL</xml>
                                                         | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
@@ -212,11 +284,31 @@ structure Direct = struct
                                                    "" => Some None
                                                  | _ => case read ks : option t of
                                                             None => None
-                                                          | Some k => Some (Some k))})}
+                                                          | Some k => Some (Some k)),
+                            CreateFilter = source "",
+                            DisplayFilter = fn s => 
+                                               <xml><cselect source={s}>
+                                                 <coption/>
+                                                 <coption value="0">NULL</coption>
+                                                 {List.mapX (fn (k, rend) =>
+                                                                <xml><coption value={"1" ^ show k}>{[rend]}</coption>
+                                                                </xml>)
+                                                            choices}
+                                               </cselect></xml> : xbody,
+                            Filter = fn s ko => s <- signal s;
+                                        return (case s of
+                                                    "" => True
+                                                  | "0" => ko = None
+                                                  | _ =>
+                                                    case read (String.substring s {Start = 1,
+                                                                                   Len = String.length s - 1})
+                                                         : option t of
+                                                        None => True
+                                                      | Some k => ko = Some k)})}
     end
 end
 
-con computedState = (unit, xbody)
+con computedState = (unit, xbody, unit)
 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
     {Initialize = return (),
      Handlers = fn () => {Header = name,
@@ -224,7 +316,10 @@ fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedS
                           Update = fn r _ => return r,
                           Display = fn x => x,
                           Edit = fn _ => <xml>...</xml>,
-                          Validate = fn _ => return True}}
+                          Validate = fn _ => return True,
+                          CreateFilter = return (),
+                          DisplayFilter = fn _ => <xml/>,
+                          Filter = fn _ _ => return True}}
 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
     {Initialize = return (),
      Handlers = fn () => {Header = name,
@@ -232,7 +327,10 @@ fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
                           Update = fn r _ => return r,
                           Display = fn x => x,
                           Edit = fn _ => <xml>...</xml>,
-                          Validate = fn _ => return True}}
+                          Validate = fn _ => return True,
+                          CreateFilter = return (),
+                          DisplayFilter = fn _ => <xml/>,
+                          Filter = fn _ _ => return True}}
 
 functor Make(M : sig
                  con key :: {Type}
@@ -242,7 +340,7 @@ functor Make(M : sig
 
                  val raw : $(map rawMeta (key ++ row))
 
-                 con cols :: {(Type * Type)}
+                 con cols :: {(Type * Type * Type)}
                  val cols : $(map (colMeta (key ++ row)) cols)
 
                  val keyFolder : folder key
diff --git a/demo/more/dbgrid.urs b/demo/more/dbgrid.urs
index 404d0f62..58c5197a 100644
--- a/demo/more/dbgrid.urs
+++ b/demo/more/dbgrid.urs
@@ -2,17 +2,20 @@ con rawMeta = fn t :: Type =>
                  {New : transaction t,
                   Inj : sql_injectable t}
 
-con colMeta' = fn (row :: {Type}) (t :: Type) =>
+con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
                   {Header : string,
-                   Project : $row -> transaction t,
-                   Update : $row -> t -> transaction ($row),
-                   Display : t -> xbody,
-                   Edit : t -> xbody,
-                   Validate : t -> signal bool}
-
-con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
-                 {Initialize : transaction global_t.1,
-                  Handlers : global_t.1 -> colMeta' row global_t.2}
+                   Project : $row -> transaction input,
+                   Update : $row -> input -> transaction ($row),
+                   Display : input -> xbody,
+                   Edit : input -> xbody,
+                   Validate : input -> signal bool,
+                   CreateFilter : transaction filter,
+                   DisplayFilter : filter -> xbody,
+                   Filter : filter -> $row -> signal bool}
+
+con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
+                 {Initialize : transaction global_input_filter.1,
+                  Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
 
 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
                        {Initial : acc,
@@ -20,48 +23,55 @@ con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
                         Display : acc -> xbody}
 
 structure Direct : sig
-    con metaBase = fn actual_input :: (Type * Type) =>
-                  {Display : actual_input.2 -> xbody,
-                   Edit : actual_input.2 -> xbody,
-                   Initialize : actual_input.1 -> transaction actual_input.2,
-                   Parse : actual_input.2 -> signal (option actual_input.1)}
-
-    datatype metaBoth actual input =
-             NonNull of metaBase (actual, input) * metaBase (option actual, input)
-           | Nullable of metaBase (actual, input)
-
-    con meta = fn global_actual_input :: (Type * Type * Type) =>
-                  {Initialize : transaction global_actual_input.1,
-                   Handlers : global_actual_input.1
-                              -> metaBoth global_actual_input.2 global_actual_input.3}
-
-    con editableState :: (Type * Type * Type) -> (Type * Type)
-    val editable : ts ::: (Type * Type * Type) -> rest ::: {Type}
+    con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
+                  {Display : actual_input_filter.2 -> xbody,
+                   Edit : actual_input_filter.2 -> xbody,
+                   Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
+                   Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
+                   CreateFilter : transaction actual_input_filter.3,
+                   DisplayFilter : actual_input_filter.3 -> xbody,
+                   Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
+
+    datatype metaBoth actual input filter =
+             NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
+           | Nullable of metaBase (actual, input, filter)
+
+    con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
+                  {Initialize : transaction global_actual_input_filter.1,
+                   Handlers : global_actual_input_filter.1
+                              -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
+                                          global_actual_input_filter.4}
+
+    con editableState :: (Type * Type * Type * Type) -> (Type * Type * Type)
+    val editable : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
                    -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
                                                      -> colMeta ([nm = ts.2] ++ rest)
                                                                 (editableState ts)
 
-    con readOnlyState :: (Type * Type * Type) -> (Type * Type)
-    val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type}
+    con readOnlyState :: (Type * Type * Type * Type) -> (Type * Type * Type)
+    val readOnly : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
                    -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
                                                      -> colMeta ([nm = ts.2] ++ rest)
                                                                 (readOnlyState ts)
 
-    val nullable : global ::: Type -> actual ::: Type -> input ::: Type
-                   -> meta (global, actual, input)
-                   -> meta (global, option actual, input)
+    val nullable : global ::: Type -> actual ::: Type -> input ::: Type -> filter ::: Type
+                   -> meta (global, actual, input, filter)
+                   -> meta (global, option actual, input, filter)
 
     type intGlobal
     type intInput
-    val int : meta (intGlobal, int, intInput)
+    type intFilter
+    val int : meta (intGlobal, int, intInput, intFilter)
 
     type stringGlobal
     type stringInput
-    val string : meta (stringGlobal, string, stringInput)
+    type stringFilter
+    val string : meta (stringGlobal, string, stringInput, stringFilter)
 
     type boolGlobal
     type boolInput
-    val bool : meta (boolGlobal, bool, boolInput)
+    type boolFilter
+    val bool : meta (boolGlobal, bool, boolInput, boolFilter)
 
     functor Foreign (M : sig
                          con row :: {Type}
@@ -75,13 +85,14 @@ structure Direct : sig
                          table tab : ([nm = t] ++ row)
                          val render : $([nm = t] ++ row) -> string
                      end) : sig
-        con global :: Type
-        con input :: Type
-        val meta : meta (global, M.t, input)
+        type global
+        type input
+        type filter
+        val meta : meta (global, M.t, input, filter)
     end
 end
 
-con computedState :: (Type * Type)
+con computedState :: (Type * Type * Type)
 val computed : row ::: {Type} -> t ::: Type -> show t
                -> string -> ($row -> t) -> colMeta row computedState
 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
@@ -94,7 +105,7 @@ functor Make(M : sig
 
                  val raw : $(map rawMeta (key ++ row))
 
-                 con cols :: {(Type * Type)}
+                 con cols :: {(Type * Type * Type)}
                  val cols : $(map (colMeta (key ++ row)) cols)
 
                  val keyFolder : folder key
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 850836b0..d4a255ee 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -6,18 +6,19 @@ datatype dlist' t =
          Empty
        | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
 
-con dlist t = source (dlist' t)
+con dlist t = {Filter: t -> signal bool,
+               Elements : source (dlist' t)}
 
 type position = transaction unit
 
 fun headPos [t] (dl : dlist t) =
-    dl' <- get dl;
+    dl' <- get dl.Elements;
     case dl' of
         Nonempty { Head = Cons (_, tl), Tail = tl' } =>
         cur <- get tl;
-        set dl (case cur of
-                    Nil => Empty
-                  | _ => Nonempty {Head = cur, Tail = tl'})
+        set dl.Elements (case cur of
+                             Nil => Empty
+                           | _ => Nonempty {Head = cur, Tail = tl'})
       | _ => return ()
 
 fun tailPos [t] (cur : source (dlist'' t)) new tail =
@@ -28,17 +29,20 @@ fun tailPos [t] (cur : source (dlist'' t)) new tail =
         Nil => set tail cur
       | _ => return ()
 
-val create = fn [t] => source Empty
+fun create [t] r =
+    s <- source Empty;
+    return {Filter = r.Filter,
+            Elements = s}
 
-fun clear [t] (s : dlist t) = set s Empty
+fun clear [t] (s : dlist t) = set s.Elements Empty
 
 fun append [t] dl v =
-    dl' <- get dl;
+    dl' <- get dl.Elements;
     case dl' of
         Empty =>
         tl <- source Nil;
         tl' <- source tl;
-        set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
+        set dl.Elements (Nonempty {Head = Cons (v, tl), Tail = tl'});
         return (headPos dl)
                 
       | Nonempty {Tail = tl, ...} =>
@@ -49,7 +53,7 @@ fun append [t] dl v =
         return (tailPos cur new tl)
 
 fun render [ctx] [ctx ~ body] [t] f dl = <xml>
-  <dyn signal={dl' <- signal dl;
+  <dyn signal={dl' <- signal dl.Elements;
                return (case dl' of
                            Empty => <xml/>
                          | Nonempty {Head = hd, Tail = tlTop} => 
@@ -63,8 +67,13 @@ fun render [ctx] [ctx ~ body] [t] f dl = <xml>
                                                          None => headPos dl
                                                        | Some prev => tailPos prev tl tlTop
                                        in
-                                           <xml>{f v pos}<dyn signal={tl' <- signal tl;
-                                                                      return (render' (Some tl) tl')}/></xml>
+                                           <xml><dyn signal={b <- dl.Filter v;
+                                                             return (if b then
+                                                                         f v pos
+                                                                     else
+                                                                         <xml/>)}/>
+                                             <dyn signal={tl' <- signal tl;
+                                                          return (render' (Some tl) tl')}/></xml>
                                        end
                            in
                                render' None hd
@@ -82,7 +91,7 @@ fun elements' [t] (dl'' : dlist'' t) =
         return (x :: tl)
 
 fun elements [t] (dl : dlist t) =
-    dl' <- signal dl;
+    dl' <- signal dl.Elements;
     case dl' of
         Empty => return []
       | Nonempty {Head = hd, ...} => elements' hd
@@ -98,7 +107,7 @@ fun foldl [t] [acc] (f : t -> acc -> signal acc) =
                 foldl'' i' dl'
 
         fun foldl' (i : acc) (dl : dlist t) : signal acc =
-            dl <- signal dl;
+            dl <- signal dl.Elements;
             case dl of
                 Empty => return i
               | Nonempty {Head = dl, ...} => foldl'' i dl
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index fcfe15ee..a55a1774 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -1,7 +1,7 @@
 con dlist :: Type -> Type
 type position
 
-val create : t ::: Type -> transaction (dlist t)
+val create : t ::: Type -> {Filter : t -> signal bool} -> transaction (dlist t)
 val clear : t ::: Type -> dlist t -> transaction unit
 val append : t ::: Type -> dlist t -> t -> transaction position
 val delete : position -> transaction unit
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 74ce6b38..424c3b6f 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -1,14 +1,17 @@
-con colMeta' = fn (row :: Type) (t :: Type) =>
+con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
                   {Header : string,
-                   Project : row -> transaction t,
-                   Update : row -> t -> transaction row,
-                   Display : t -> xbody,
-                   Edit : t -> xbody,
-                   Validate : t -> signal bool}
-
-con colMeta = fn (row :: Type) (global_t :: (Type * Type)) =>
-                 {Initialize : transaction global_t.1,
-                  Handlers : global_t.1 -> colMeta' row global_t.2}                  
+                   Project : row -> transaction input,
+                   Update : row -> input -> transaction row,
+                   Display : input -> xbody,
+                   Edit : input -> xbody,
+                   Validate : input -> signal bool,
+                   CreateFilter : transaction filter,
+                   DisplayFilter : filter -> xbody,
+                   Filter : filter -> row -> signal bool}
+                  
+con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) =>
+                 {Initialize : transaction global_input_filter.1,
+                  Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
 
 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
                        {Initial : acc,
@@ -25,7 +28,7 @@ functor Make(M : sig
                  val save : key -> row -> transaction unit
                  val delete : key -> transaction unit
 
-                 con cols :: {(Type * Type)}
+                 con cols :: {(Type * Type * Type)}
                  val cols : $(map (colMeta row) cols)
 
                  val folder : folder cols
@@ -40,20 +43,21 @@ functor Make(M : sig
     style td
     style agg
 
-    fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row
+    fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
 
-    fun makeAll cols row = @@Monad.exec [transaction] _ [map snd M.cols]
-                               (map2 [fst] [colMeta M.row] [fn p :: (Type * Type) => transaction p.2]
-                                     (fn [p] data meta => make row [_] (meta.Handlers data))
+    fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
+                               (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
+                                     (fn [p] data meta => make row [_] [_] (meta.Handlers data))
                                      [_] M.folder cols M.cols)
                                (@@Folder.mp [_] [_] M.folder)
 
-    type grid = {Cols : $(map fst M.cols),
+    type grid = {Cols : $(map fst3 M.cols),
                  Rows : Dlist.dlist {Row : source M.row,
-                                     Cols : source ($(map snd M.cols)),
+                                     Cols : source ($(map snd3 M.cols)),
                                      Updating : source bool,
                                      Selected : source bool},
-                 Selection : source bool}
+                 Selection : source bool,
+                 Filters : $(map thd3 M.cols)}
 
     fun addRow cols rows row =
         rowS <- source row;
@@ -66,15 +70,29 @@ functor Make(M : sig
                                          Updating = ud,
                                          Selected = sd})
 
-    val createMetas = Monad.mapR [colMeta M.row] [fst]
-                           (fn [nm :: Name] [p :: (Type * Type)] meta => meta.Initialize)
-                           [_] M.folder M.cols
-
     val grid =
-        cols <- createMetas;
-        rows <- Dlist.create;
+        cols <- Monad.mapR [colMeta M.row] [fst3]
+                           (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
+                           [_] M.folder M.cols;
+
+        filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3]
+                               (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
+                                   (meta.Handlers state).CreateFilter)
+                               [_] M.folder M.cols cols;
+
+        rows <- Dlist.create {Filter = fn all =>
+                                          row <- signal all.Row;
+                                          foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
+                                                 (fn [nm :: Name] [p :: (Type * Type * Type)]
+                                                                  [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                                                                  meta state filter combinedFilter row =>
+                                                     previous <- combinedFilter row;
+                                                     this <- (meta.Handlers state).Filter filter row;
+                                                     return (previous && this))
+                                                 (fn _ => return True)
+                                                 [_] M.folder M.cols cols filters row};
         sel <- source False;
-        return {Cols = cols, Rows = rows, Selection = sel}
+        return {Cols = cols, Rows = rows, Selection = sel, Filters = filters}
 
     fun sync {Cols = cols, Rows = rows, ...} =
         Dlist.clear rows;
@@ -85,8 +103,8 @@ functor Make(M : sig
       <table class={tabl}>
         <tr class={tr}>
           <th/> <th/> <th/>
-          {foldRX2 [fst] [colMeta M.row] [_]
-                   (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
+          {foldRX2 [fst3] [colMeta M.row] [_]
+                   (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
                                     data (meta : colMeta M.row p) =>
                        <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
                    [_] M.folder grid.Cols M.cols}
@@ -109,8 +127,8 @@ functor Make(M : sig
                                   
                               val save =
                                   cols <- get colsS;
-                                  errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string]
-                                                         (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                  errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string]
+                                                         (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
                                                                           [[nm] ~ rest] data meta v errors =>
                                                              b <- current ((meta.Handlers data).Validate v);
                                                              return (if b then
@@ -128,9 +146,9 @@ functor Make(M : sig
                                     | None =>
                                       set ud False;
                                       row <- get rowS;
-                                      row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row]
-                                                           (fn [nm :: Name] [t :: (Type * Type)]
-                                                                            [rest :: {(Type * Type)}]
+                                      row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
+                                                           (fn [nm :: Name] [t :: (Type * Type * Type)]
+                                                                            [rest :: {(Type * Type * Type)}]
                                                                             [[nm] ~ rest] data meta v row' =>
                                                                (meta.Handlers data).Update row' v)
                                                            row [_] M.folder grid.Cols M.cols cols;
@@ -165,9 +183,9 @@ functor Make(M : sig
                                 </td>
 
                                 <dyn signal={cols <- signal colsS;
-                                             return (foldRX3 [fst] [colMeta M.row] [snd] [_]
-                                                             (fn [nm :: Name] [t :: (Type * Type)]
-                                                                              [rest :: {(Type * Type)}]
+                                             return (foldRX3 [fst3] [colMeta M.row] [snd3] [_]
+                                                             (fn [nm :: Name] [t :: (Type * Type * Type)]
+                                                                              [rest :: {(Type * Type * Type)}]
                                                                               [[nm] ~ rest] data meta v =>
                                                                  <xml><td class={td}>
                                                                    <dyn signal={b <- signal ud;
@@ -206,6 +224,13 @@ functor Make(M : sig
                                         <xml><td class={agg}>{meta.Display acc}</td></xml>)
                                     [_] M.aggFolder M.aggregates rows}
                          </tr></xml>}/>
+
+              <tr><th colspan={3}>Filters</th>
+                {foldRX3 [colMeta M.row] [fst3] [thd3] [_]
+                 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                                  meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
+                 [_] M.folder M.cols grid.Cols grid.Filters}
+              </tr>
           </table>
           
           <button value="New row" onclick={row <- rpc M.new;
diff --git a/demo/more/grid.urp b/demo/more/grid.urp
index 0736e4fe..a67abdb2 100644
--- a/demo/more/grid.urp
+++ b/demo/more/grid.urp
@@ -2,6 +2,7 @@
 $/option
 $/monad
 $/list
+$/string
 dlist
 grid
 dbgrid
diff --git a/demo/more/grid.urs b/demo/more/grid.urs
index e3d8f828..2ab9fbcc 100644
--- a/demo/more/grid.urs
+++ b/demo/more/grid.urs
@@ -1,14 +1,17 @@
-con colMeta' = fn (row :: Type) (t :: Type) =>
+con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
                   {Header : string,
-                   Project : row -> transaction t,
-                   Update : row -> t -> transaction row,
-                   Display : t -> xbody,
-                   Edit : t -> xbody,
-                   Validate : t -> signal bool}
+                   Project : row -> transaction input,
+                   Update : row -> input -> transaction row,
+                   Display : input -> xbody,
+                   Edit : input -> xbody,
+                   Validate : input -> signal bool,
+                   CreateFilter : transaction filter,
+                   DisplayFilter : filter -> xbody,
+                   Filter : filter -> row -> signal bool}
                   
-con colMeta = fn (row :: Type) (global_t :: (Type * Type)) =>
-                 {Initialize : transaction global_t.1,
-                  Handlers : global_t.1 -> colMeta' row global_t.2}
+con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) =>
+                 {Initialize : transaction global_input_filter.1,
+                  Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
 
 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
                        {Initial : acc,
@@ -25,7 +28,7 @@ functor Make(M : sig
                  val save : key -> row -> transaction unit
                  val delete : key -> transaction unit
 
-                 con cols :: {(Type * Type)}
+                 con cols :: {(Type * Type * Type)}
                  val cols : $(map (colMeta row) cols)
 
                  val folder : folder cols