"Hello world" compiles, after replacing type-level fold with map

25 files changed, 223 insertions, 416 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index b4a40fde..cd2468ba 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -120,31 +120,20 @@ con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
 con sql_subset :: {{Type}} -> {{Type}} -> Type
 val sql_subset : keep_drop :: {({Type} * {Type})}
                               -> sql_subset
-                                     (fold (fn nm (fields :: ({Type} * {Type}))
-                                                  acc [[nm] ~ acc]
-                                                  [fields.1 ~ fields.2] =>
-                                               [nm = fields.1 ++ fields.2]
-                                                   ++ acc) [] keep_drop)
-                                     (fold (fn nm (fields :: ({Type} * {Type}))
-                                                  acc [[nm] ~ acc] =>
-                                               [nm = fields.1] ++ acc)
-                                               [] keep_drop)
+                                     (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
+                                     (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
 
 val sql_query1 : tables ::: {{Type}}
                  -> grouped ::: {{Type}}
                  -> selectedFields ::: {{Type}}
                  -> selectedExps ::: {Type}
-                 -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
-                                       [nm = sql_table fields] ++ acc)
-                                       [] tables),
+                 -> {From : $(map (fn fields :: {Type} => sql_table fields) tables),
                      Where : sql_exp tables [] [] bool,
                      GroupBy : sql_subset tables grouped,
                      Having : sql_exp grouped tables [] bool,
                      SelectFields : sql_subset grouped selectedFields,
-                     SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
-                                             [nm = sql_exp grouped tables [] t]
-                                                 ++ acc) [] selectedExps) }
+                     SelectExps : $(map (fn (t :: Type) => sql_exp grouped tables [] t) selectedExps) }
                  -> sql_query1 tables selectedFields selectedExps
 
 type sql_relop 
@@ -291,8 +280,7 @@ val query : tables ::: {{Type}} -> exps ::: {Type}
             -> fn [tables ~ exps] =>
                   state ::: Type
                   -> sql_query tables exps
-                  -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
-                                         [nm = $fields] ++ acc) [] tables)
+                  -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                       -> state
                       -> transaction state)
                   -> state
@@ -306,17 +294,12 @@ val dml : dml -> transaction unit
 
 val insert : fields ::: {Type}
              -> sql_table fields
-             -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
-                           [nm = sql_exp [] [] [] t] ++ acc)
-                           [] fields)
+             -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
              -> dml
 
 val update : unchanged ::: {Type} -> changed :: {Type} ->
              fn [changed ~ unchanged] =>
-                $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
-                           [nm = sql_exp [T = changed ++ unchanged] [] [] t]
-                               ++ acc)
-                           [] changed)
+                $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
                 -> sql_table (changed ++ unchanged)
                 -> sql_exp [T = changed ++ unchanged] [] [] bool
                 -> dml
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 35e8519b..58e99f3c 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -8,17 +8,7 @@ con fstTTT (t :: (Type * Type * Type)) = t.1
 con sndTTT (t :: (Type * Type * Type)) = t.2
 con thdTTT (t :: (Type * Type * Type)) = t.3
 
-con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
-                                         [nm = f t] ++ acc) []
-
-con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
-                                     [nm = f] ++ acc) []
-
-con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
-                                                   [nm = f t] ++ acc) []
-
-con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
-                                                          [nm = f t] ++ acc) []
+con mapUT = fn f :: Type => map (fn _ :: Unit => f)
 
 con ex = fn tf :: (Type -> Type) =>
             res ::: Type -> (choice :: Type -> tf choice -> res) -> res
@@ -69,7 +59,7 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
                 -> fn [[nm] ~ rest] =>
                       tf t -> tr rest -> tr ([nm = t] ++ rest))
            (i : tr []) =
-    fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
+    fold [fn r :: {Type} => $(map tf r) -> tr r]
              (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest)
                               [[nm] ~ rest] r =>
                  f [nm] [t] [rest] r.nm (acc (r -- nm)))
@@ -80,7 +70,7 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
                  -> fn [[nm] ~ rest] =>
                        tf t -> tr rest -> tr ([nm = t] ++ rest))
             (i : tr []) =
-    fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
+    fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r]
              (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
                               (acc : _ -> tr rest) [[nm] ~ rest] r =>
                  f [nm] [t] [rest] r.nm (acc (r -- nm)))
@@ -91,7 +81,7 @@ fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -
                  -> fn [[nm] ~ rest] =>
                        tf t -> tr rest -> tr ([nm = t] ++ rest))
             (i : tr []) =
-    fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r]
+    fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r]
              (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
                               (acc : _ -> tr rest) [[nm] ~ rest] r =>
                  f [nm] [t] [rest] r.nm (acc (r -- nm)))
@@ -102,7 +92,7 @@ fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
                  -> fn [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
             (i : tr []) =
-    fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
+    fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r]
              (fn (nm :: Name) (t :: Type) (rest :: {Type})
                               (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
                  f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
@@ -114,7 +104,7 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
                   -> fn [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
              (i : tr []) =
-    fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
+    fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
              (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
                               (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
                  f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
@@ -126,7 +116,7 @@ fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type)
                   -> fn [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
              (i : tr []) =
-    fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r]
+    fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
              (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
                               (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
                  f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
@@ -195,8 +185,7 @@ fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type)
 
 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
            (q : sql_query tables exps) [tables ~ exps]
-           (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
-                                   [nm = $fields] ++ acc) [] tables)
+           (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> xml ctx [] []) =
     query q
           (fn fs acc => return <xml>{acc}{f fs}</xml>)
@@ -204,8 +193,7 @@ fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
 
 fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
             (q : sql_query tables exps) [tables ~ exps]
-            (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
-                                    [nm = $fields] ++ acc) [] tables)
+            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction (xml ctx [] [])) =
     query q
           (fn fs acc =>
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index d6315b92..49aad50c 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -8,17 +8,7 @@ con fstTTT = fn t :: (Type * Type * Type) => t.1
 con sndTTT = fn t :: (Type * Type * Type) => t.2
 con thdTTT = fn t :: (Type * Type * Type) => t.3
 
-con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
-                                             [nm = f t] ++ acc) []
-
-con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
-                                     [nm = f] ++ acc) []
-
-con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
-                                                       [nm = f t] ++ acc) []
-
-con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
-                                                              [nm = f t] ++ acc) []
+con mapUT = fn f :: Type => map (fn _ :: Unit => f)
 
 con ex = fn tf :: (Type -> Type) =>
             res ::: Type -> (choice :: Type -> tf choice -> res) -> res
@@ -53,19 +43,19 @@ val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
              -> (nm :: Name -> t :: Type -> rest :: {Type}
                  -> fn [[nm] ~ rest] =>
                        tf t -> tr rest -> tr ([nm = t] ++ rest))
-             -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
+             -> tr [] -> r :: {Type} -> $(map tf r) -> tr r
 
 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
               -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
                   -> fn [[nm] ~ rest] =>
                         tf t -> tr rest -> tr ([nm = t] ++ rest))
-              -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
+              -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r
 
 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
               -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
                   -> fn [[nm] ~ rest] =>
                         tf t -> tr rest -> tr ([nm = t] ++ rest))
-              -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r
+              -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r
 
 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
               -> tr :: ({Type} -> Type)
@@ -73,7 +63,7 @@ val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
                   -> fn [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
               -> tr []
-              -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
+              -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r
                                                                     
 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
                -> tr :: ({(Type * Type)} -> Type)
@@ -81,7 +71,7 @@ val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
                    -> fn [[nm] ~ rest] =>
                          tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
                -> tr [] -> r :: {(Type * Type)}
-               -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
+               -> $(map tf1 r) -> $(map tf2 r) -> tr r
 
 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
                -> tr :: ({(Type * Type * Type)} -> Type)
@@ -89,32 +79,32 @@ val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * T
                    -> fn [[nm] ~ rest] =>
                          tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
                -> tr [] -> r :: {(Type * Type * Type)}
-               -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r
+               -> $(map tf1 r) -> $(map tf2 r) -> tr r
 
 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
               -> (nm :: Name -> t :: Type -> rest :: {Type}
                   -> fn [[nm] ~ rest] =>
                         tf t -> xml ctx [] [])
-              -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
+              -> r :: {Type} -> $(map tf r) -> xml ctx [] []
 
 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
                -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
                    -> fn [[nm] ~ rest] =>
                          tf t -> xml ctx [] [])
-               -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
+               -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] []
 
 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
                -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
                    -> fn [[nm] ~ rest] =>
                          tf t -> xml ctx [] [])
-               -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] []
+               -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] []
 
 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
                -> (nm :: Name -> t :: Type -> rest :: {Type}
                    -> fn [[nm] ~ rest] =>
                          tf1 t -> tf2 t -> xml ctx [] [])
                -> r :: {Type}
-               -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
+               -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
 
 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
                 -> ctx :: {Unit}
@@ -122,7 +112,7 @@ val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
                     -> fn [[nm] ~ rest] =>
                           tf1 t -> tf2 t -> xml ctx [] [])
                 -> r :: {(Type * Type)}
-                -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
+                -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
 
 
 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
@@ -131,21 +121,19 @@ val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type *
                     -> fn [[nm] ~ rest] =>
                           tf1 t -> tf2 t -> xml ctx [] [])
                 -> r :: {(Type * Type * Type)}
-                -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] []
+                -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
              -> sql_query tables exps
              -> fn [tables ~ exps] =>
-                   ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
-                                       [nm = $fields] ++ acc) [] tables)
+                   ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                     -> xml ctx [] [])
                    -> transaction (xml ctx [] [])
 
 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
               -> sql_query tables exps
               -> fn [tables ~ exps] =>
-                    ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
-                                        [nm = $fields] ++ acc) [] tables)
+                    ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                      -> transaction (xml ctx [] []))
                     -> transaction (xml ctx [] [])
                        
@@ -155,20 +143,14 @@ val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
                         transaction
                             (option
                                  $(exps
-                                       ++ fold (fn nm (fields :: {Type}) acc
-                                                      [[nm] ~ acc] =>
-                                                   [nm = $fields] ++ acc)
-                                                   [] tables))
+                                       ++ map (fn fields :: {Type} => $fields) tables))
 
 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
              -> sql_query tables exps
              -> fn [tables ~ exps] =>
                    transaction
                        $(exps
-                             ++ fold (fn nm (fields :: {Type}) acc
-                                            [[nm] ~ acc] =>
-                                         [nm = $fields] ++ acc)
-                                         [] tables)
+                             ++ map (fn fields :: {Type} => $fields) tables)
 
 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
                  -> t ::: Type -> sql_injectable (option t)
diff --git a/src/core.sml b/src/core.sml
index c6e0cfef..d7a57493 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -54,7 +54,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
-       | CFold of kind * kind
+       | CMap of kind * kind
 
        | CUnit
 
diff --git a/src/core_print.sml b/src/core_print.sml
index 405ae14e..db8c3907 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -138,7 +138,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
-      | CFold _ => string "fold"
+      | CMap _ => string "map"
       | CUnit => string "()"
 
       | CTuple cs => box [string "(",
diff --git a/src/core_util.sml b/src/core_util.sml
index a222dca4..e76da387 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -178,11 +178,11 @@ fun compare ((c1, _), (c2, _)) =
       | (CConcat _, _) => LESS
       | (_, CConcat _) => GREATER
 
-      | (CFold (d1, r1), CFold (d2, r2)) =>
+      | (CMap (d1, r1), CMap (d2, r2)) =>
         join (Kind.compare (d1, r2),
               fn () => Kind.compare (r1, r2))
-      | (CFold _, _) => LESS
-      | (_, CFold _) => GREATER
+      | (CMap _, _) => LESS
+      | (_, CMap _) => GREATER
 
       | (CUnit, CUnit) => EQUAL
       | (CUnit, _) => LESS
@@ -261,12 +261,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
-              | CFold (k1, k2) =>
+              | CMap (k1, k2) =>
                 S.bind2 (mfk k1,
                          fn k1' =>
                             S.map2 (mfk k2,
                                     fn k2' =>
-                                       (CFold (k1', k2'), loc)))
+                                       (CMap (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
 
diff --git a/src/corify.sml b/src/corify.sml
index 2383ee03..c464e5a5 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -473,7 +473,7 @@ fun corifyCon st (c, loc) =
       | L.CRecord (k, xcs) =>
         (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
       | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
-      | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
+      | L.CMap (k1, k2) => (L'.CMap (corifyKind k1, corifyKind k2), loc)
       | L.CUnit => (L'.CUnit, loc)
 
       | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
diff --git a/src/disjoint.sml b/src/disjoint.sml
index c6a8d50f..81023972 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -213,37 +213,8 @@ fun decomposeRow (env, denv) c =
                                                 ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
                 case #1 (#1 (hnormCon (env, denv) c)) of
                     CApp (
-                    (CApp (
-                     (CApp ((CFold (dom, ran), _), f), _),
-                     i), _),
-                    r) =>
-                    let
-                        val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
-                        val (env', v) = E.pushCNamed env' "v" dom NONE
-                        val (env', st) = E.pushCNamed env' "st" ran NONE
-
-                        val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
-                                                                              (CUnit, loc))]), loc),
-                                                             (CNamed st, loc))
-
-                        val c' = (CApp (f, (CNamed nm, loc)), loc)
-                        val c' = (CApp (c', (CNamed v, loc)), loc)
-                        val c' = (CApp (c', (CNamed st, loc)), loc)
-                        val (ps, gs'') = decomposeRow (env', denv') c'
-
-                        fun covered p =
-                            case p of
-                                Unknown _ => false
-                              | Piece p =>
-                                case p of
-                                    (NameN n, []) => n = nm
-                                  | (RowN n, []) => n = st
-                                  | _ => false
-
-                        val ps = List.filter (not o covered) ps
-                    in
-                        decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
-                    end
+                    (CApp ((CMap _, _), _), _),
+                    r) => decomposeRow' (r, (acc, gs))
                   | _ => default ()
             end
     in
diff --git a/src/elab.sml b/src/elab.sml
index 8e44c43c..ec8a910a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -66,7 +66,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
-       | CFold of kind * kind
+       | CMap of kind * kind
 
        | CUnit
 
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 0648d704..c3e9274c 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -114,181 +114,98 @@ fun hnormCon env (cAll as (c, loc)) =
                                           ("sc", ElabPrint.p_con env sc)];*)
                  sc
              end
-           | c1' as CApp (c', i) =>
+           | c1' as CApp (c', f) =>
              let
                  fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
              in
                  case #1 (hnormCon env c') of
-                     CApp (c', f) =>
-                     (case #1 (hnormCon env c') of
-                          CFold ks =>
-                          (case #1 (hnormCon env c2) of
-                               CRecord (_, []) => hnormCon env i
-                             | CRecord (k, (x, c) :: rest) =>
-                               hnormCon env
-                                        (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                               (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
-                                                      (CRecord (k, rest), loc)), loc)), loc)
-                             | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
-                               let
-                                   val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
-
-                               (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                                  (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
-                                                         rest''), loc)), loc)*)
-                               in
-                                   (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
-                                   hnormCon env
-                                            (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                                   (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
-                                                          rest''), loc)), loc)
-                               end
-                             | _ =>
-                               let
-                                   fun cunif () =
-                                       let
-                                           val r = ref NONE
-                                       in
-                                           (r, (CUnif (loc, (KType, loc), "_", r), loc))
-                                       end
-
-                                   val (nmR, nm) = cunif ()
-                                   val (vR, v) = cunif ()
-                                   val (rR, r) = cunif ()
-
-                                   val c = f
-                                   val c = (CApp (c, nm), loc)
-                                   val c = (CApp (c, v), loc)
-                                   val c = (CApp (c, r), loc)
-                                   fun unconstraint c =
-                                       case hnormCon env c of
-                                           (CDisjoint (_, _, _, c), _) => unconstraint c
-                                         | c => c
-                                   val c = unconstraint c
-
-                                   fun tryDistributivity () =
-                                       let
-                                           fun distribute (c1, c2) =
-                                               let
-                                                   val c = (CFold ks, loc)
-                                                   val c = (CApp (c, f), loc)
-                                                   val c = (CApp (c, i), loc)
-
-                                                   val c1 = (CApp (c, c1), loc)
-                                                   val c2 = (CApp (c, c2), loc)
-                                                   val c = (CConcat (c1, c2), loc)
-                                               in
-                                                   hnormCon env c
-                                               end
-                                       in
-                                           case (hnormCon env i, hnormCon env c2, hnormCon env c) of
-                                               ((CRecord (_, []), _),
-                                                (CConcat (arg1, arg2), _),
-                                                (CConcat (c1, c2'), _)) =>
-                                               (case (hnormCon env c1, hnormCon env c2') of
-                                                    ((CRecord (_, [(nm', v')]), _),
-                                                     (CUnif (_, _, _, rR'), _)) =>
-                                                    (case hnormCon env nm' of
-                                                         (CUnif (_, _, _, nmR'), _) =>
-                                                         if nmR' = nmR andalso rR' = rR then
-                                                             distribute (arg1, arg2)
-                                                         else
-                                                             default ()
-                                                       | _ => default ())
-                                                  | _ => default ())
-                                             | _ => default ()
-                                       end
-
-                                   fun tryFusion () =
-                                       let
-                                           fun fuse (dom, new_v, r') =
-                                               let
-                                                   val ran = #2 ks
-
-                                                   val f = (CApp (f, (CRel 2, loc)), loc)
-                                                   val f = (CApp (f, new_v), loc)
-                                                   val f = (CApp (f, (CRel 0, loc)), loc)
-                                                   val f = (CAbs ("acc", ran, f), loc)
-                                                   val f = (CAbs ("v", dom, f), loc)
-                                                   val f = (CAbs ("nm", (KName, loc), f), loc)
-
-                                                   val c = (CFold (dom, ran), loc)
-                                                   val c = (CApp (c, f), loc)
-                                                   val c = (CApp (c, i), loc)
-                                                   val c = (CApp (c, r'), loc)
-                                               in
-                                                   hnormCon env c
-                                               end
-                                       in
-                                           case #1 (hnormCon env c2) of
-                                               CApp (f, r') =>
-                                               (case #1 (hnormCon env f) of
-                                                    CApp (f, inner_i) =>
-                                                    (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of
-                                                         (CApp (f, inner_f), CRecord (_, [])) =>
-                                                         (case #1 (hnormCon env f) of
-                                                              CFold (dom, _) =>
-                                                              let
-                                                                  val c = inner_f
-                                                                  val c = (CApp (c, nm), loc)
-                                                                  val c = (CApp (c, v), loc)
-                                                                  val c = (CApp (c, r), loc)
-                                                                  val c = unconstraint c
-
-                                                                  (*val () = Print.prefaces "Onto something!"
-                                                                           [("c", ElabPrint.p_con env cAll),
-                                                                            ("c'", ElabPrint.p_con env c)]*)
-
-                                                              in
-                                                                  case #1 (hnormCon env c) of
-                                                                      CConcat (first, rest) =>
-                                                                      (case (#1 (hnormCon env first),
-                                                                             #1 (hnormCon env rest)) of
-                                                                           (CRecord (_, [(nm', v')]),
-                                                                            CUnif (_, _, _, rR')) =>
-                                                                           (case #1 (hnormCon env nm') of
-                                                                                CUnif (_, _, _, nmR') =>
-                                                                                if rR' = rR andalso nmR' = nmR then
-                                                                                    (nmR := SOME (CRel 2, loc);
-                                                                                     vR := SOME (CRel 1, loc);
-                                                                                     rR := SOME (CError, loc);
-                                                                                     fuse (dom, v', r'))
-                                                                                else
-                                                                                    tryDistributivity ()
-                                                                              | _ => tryDistributivity ())
-                                                                         | _ => tryDistributivity ())
-                                                                    | _ => tryDistributivity ()
-                                                              end
-                                                            | _ => tryDistributivity ())
-                                                       | _ => tryDistributivity ())
-                                                  | _ => tryDistributivity ())
-                                             | _ => tryDistributivity ()
-                                       end
-
-                               in
-                                   (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
-                                   case (hnormCon env i, unconstraint c) of
-                                       ((CRecord (_, []), _),
-                                        (CConcat (c1, c2'), _)) =>
-                                       (case (hnormCon env c1, hnormCon env c2') of
-                                            ((CRecord (_, [(nm', v')]), _),
-                                             (CUnif (_, _, _, rR'), _)) =>
-                                            (case (hnormCon env nm', hnormCon env v') of
-                                                 ((CUnif (_, _, _, nmR'), _),
-                                                  (CUnif (_, _, _, vR'), _)) =>
-                                                 if nmR' = nmR andalso vR' = vR andalso rR' = rR then
-                                                     hnormCon env c2
-                                                 else
-                                                     tryFusion ()
-                                               | _ => tryFusion ())
-                                          | _ => tryFusion ())
-                                     | _ => tryFusion ()
-                               end)
-                        | _ => default ())
+                     CMap (ks as (k1, k2)) =>
+                     (case #1 (hnormCon env c2) of
+                          CRecord (_, []) => (CRecord (k2, []), loc)
+                        | CRecord (_, (x, c) :: rest) =>
+                          hnormCon env
+                                   (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+                                             (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
+                        | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+                          let
+                              val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+                          in
+                              hnormCon env
+                                       (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+                                                 (CApp (c1, rest''), loc)), loc)
+                          end
+                        | _ =>
+                          let
+                              fun unconstraint c =
+                                  case hnormCon env c of
+                                      (CDisjoint (_, _, _, c), _) => unconstraint c
+                                    | c => c
+
+                              fun tryDistributivity () =
+                                  case hnormCon env c2 of
+                                      (CConcat (c1, c2'), _) =>
+                                      let
+                                          val c = (CMap ks, loc)
+                                          val c = (CApp (c, f), loc)
+                                                  
+                                          val c1 = (CApp (c, c1), loc)
+                                          val c2 = (CApp (c, c2'), loc)
+                                          val c = (CConcat (c1, c2), loc)
+                                      in
+                                          hnormCon env c
+                                      end
+                                    | _ => default ()
+
+                              fun tryFusion () =
+                                  case #1 (hnormCon env c2) of
+                                      CApp (f', r') =>
+                                      (case #1 (hnormCon env f') of
+                                           CApp (f', inner_f) =>
+                                           (case #1 (hnormCon env f') of
+                                                CMap (dom, _) =>
+                                                let
+                                                    val f' = (CApp (inner_f, (CRel 0, loc)), loc)
+                                                    val f' = (CApp (f, f'), loc)
+                                                    val f' = (CAbs ("v", dom, f'), loc)
+
+                                                    val c = (CMap (dom, k2), loc)
+                                                    val c = (CApp (c, f'), loc)
+                                                    val c = (CApp (c, r'), loc)
+                                                in
+                                                    hnormCon env c
+                                                end
+                                              | _ => tryDistributivity ())
+                                         | _ => tryDistributivity ())
+                                    | _ => tryDistributivity ()
+
+                              fun tryIdentity () =
+                                  let
+                                      fun cunif () =
+                                          let
+                                              val r = ref NONE
+                                          in
+                                              (r, (CUnif (loc, (KType, loc), "_", r), loc))
+                                          end
+                                          
+                                      val (vR, v) = cunif ()
+
+                                      val c = (CApp (f, v), loc)
+                                  in
+                                      case unconstraint c of
+                                          (CUnif (_, _, _, vR'), _) =>
+                                          if vR' = vR then
+                                              hnormCon env c2
+                                          else
+                                              tryFusion ()
+                                        | _ => tryFusion ()
+                                  end
+                          in
+                              tryIdentity ()
+                          end)
                    | _ => default ()
              end
            | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
-
+        
       | CConcat (c1, c2) =>
         (case (hnormCon env c1, hnormCon env c2) of
              ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 0e6c9767..098c9259 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -167,7 +167,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
-      | CFold _ => string "fold"
+      | CMap _ => string "map"
 
       | CUnit => string "()"
 
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6e78907d..f052a06d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -168,12 +168,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
-              | CFold (k1, k2) =>
+              | CMap (k1, k2) =>
                 S.bind2 (mfk k1,
                          fn k1' =>
                             S.map2 (mfk k2,
                                     fn k2' =>
-                                       (CFold (k1', k2'), loc)))
+                                       (CMap (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 39cb85b2..fa97bdf8 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -182,13 +182,10 @@
        | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
        | L.KWild => kunif loc
 
- fun foldKind (dom, ran, loc)=
-     (L'.KArrow ((L'.KArrow ((L'.KName, loc),
-                             (L'.KArrow (dom,
-                                         (L'.KArrow (ran, ran), loc)), loc)), loc),
-                 (L'.KArrow (ran,
-                             (L'.KArrow ((L'.KRecord dom, loc),
-                                         ran), loc)), loc)), loc)
+ fun mapKind (dom, ran, loc)=
+     (L'.KArrow ((L'.KArrow (dom, ran), loc),
+                 (L'.KArrow ((L'.KRecord dom, loc),
+                             (L'.KRecord ran, loc)), loc)), loc)
 
  fun hnormKind (kAll as (k, _)) =
      case k of
@@ -355,13 +352,13 @@
              ((L'.CConcat (c1', c2'), loc), k,
               D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
          end
-       | L.CFold =>
+       | L.CMap =>
          let
              val dom = kunif loc
              val ran = kunif loc
          in
-             ((L'.CFold (dom, ran), loc),
-              foldKind (dom, ran, loc),
+             ((L'.CMap (dom, ran), loc),
+              mapKind (dom, ran, loc),
               [])
          end
 
@@ -489,7 +486,7 @@
 
        | L'.CRecord (k, _) => (L'.KRecord k, loc)
        | L'.CConcat (c, _) => kindof env c
-       | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
+       | L'.CMap (dom, ran) => mapKind (dom, ran, loc)
 
        | L'.CUnit => (L'.KUnit, loc)
 
@@ -504,41 +501,21 @@
 
  val hnormCon = D.hnormCon
 
- datatype con_summary =
-          Nil
-        | Cons
-        | Unknown
-
- fun compatible cs =
-     case cs of
-         (Unknown, _) => false
-       | (_, Unknown) => false
-       | (s1, s2) => s1 = s2
-
- fun summarizeCon (env, denv) c =
+ fun deConstraintCon (env, denv) c =
      let
          val (c, gs) = hnormCon (env, denv) c
      in
          case #1 c of
-             L'.CRecord (_, []) => (Nil, gs)
-           | L'.CRecord (_, _ :: _) => (Cons, gs)
-           | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
-           | L'.CDisjoint (_, _, _, c) =>
+             L'.CDisjoint (_, _, _, c) =>
              let
-                 val (s, gs') = summarizeCon (env, denv) c
+                 val (c', gs') = deConstraintCon (env, denv) c
              in
-                 (s, gs @ gs')
+                 (c', gs @ gs')
              end
-           | _ => (Unknown, gs)
+           | _ => (c, gs)
      end
 
- fun p_con_summary s =
-     Print.PD.string (case s of
-                          Nil => "Nil"
-                        | Cons => "Cons"
-                        | Unknown => "Unknown")
-
- exception SummaryFailure
+ exception GuessFailure
 
  fun isUnitCon env (c, loc) =
      case c of
@@ -574,7 +551,7 @@
 
        | L'.CRecord _ => false
        | L'.CConcat _ => false
-       | L'.CFold _ => false
+       | L'.CMap _ => false
 
        | L'.CUnit => true
 
@@ -720,14 +697,14 @@
 
          fun isGuessable (other, fs) =
              let
-                 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
+                 val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure)
              in
                  List.all (fn (loc, env, denv, c1, c2) =>
                               case D.prove env denv (c1, c2, loc) of
                                   [] => true
                                 | _ => false) gs
              end
-             handle SummaryFailure => false
+             handle GuessFailure => false
 
          val (fs1, fs2, others1, others2) =
              case (fs1, fs2, others1, others2) of
@@ -783,79 +760,68 @@
                                        ("#2", p_summary env s2)]*)
      end
 
- and guessFold (env, denv) (c1, c2, gs, ex) =
+ and guessMap (env, denv) (c1, c2, gs, ex) =
      let
          val loc = #2 c1
 
-         fun unfold (dom, ran, f, i, r, c) =
+         fun unfold (dom, ran, f, r, c) =
              let
-                 val nm = cunif (loc, (L'.KName, loc))
-                 val v =
-                     case dom of
-                         (L'.KUnit, _) => (L'.CUnit, loc)
-                       | _ => cunif (loc, dom)
-                 val rest = cunif (loc, (L'.KRecord dom, loc))
-                 val acc = (L'.CFold (dom, ran), loc)
-                 val acc = (L'.CApp (acc, f), loc)
-                 val acc = (L'.CApp (acc, i), loc)
-                 val acc = (L'.CApp (acc, rest), loc)
-
-                 val (iS, gs3) = summarizeCon (env, denv) i
-
-                 val app = (L'.CApp (f, nm), loc)
-                 val app = (L'.CApp (app, v), loc)
-                 val app = (L'.CApp (app, acc), loc)
-                 val (appS, gs4) = summarizeCon (env, denv) app
-
-                 val (cS, gs5) = summarizeCon (env, denv) c
-             in
-                 (*prefaces "Summaries" [("iS", p_con_summary iS),
-                                         ("appS", p_con_summary appS),
-                                         ("cS", p_con_summary cS)];*)
-
-                 if compatible (iS, appS) then
-                     raise ex
-                 else if compatible (cS, iS) then
+                 fun unfold (r, c) =
                      let
-                         (*val () = prefaces "Same?" [("i", p_con env i),
-                                                    ("c", p_con env c)]*)
-                         val gs6 = unifyCons (env, denv) i c
-                         (*val () = TextIO.print "Yes!\n"*)
-
-                         val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+                         val (c', gs1) = deConstraintCon (env, denv) c
                      in
-                         gs @ gs3 @ gs5 @ gs6 @ gs7
-                     end
-                 else if compatible (cS, appS) then
-                     let
-                         (*val () = prefaces "Same?" [("app", p_con env app),
-                                                      ("c", p_con env c),
-                                                      ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
-                         val gs6 = unifyCons (env, denv) app c
-                         (*val () = TextIO.print "Yes!\n"*)
-
-                         val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
-                         val concat = (L'.CConcat (singleton, rest), loc)
-                         (*val () = prefaces "Pre-crew" [("r", p_con env r),
-                                                         ("concat", p_con env concat)]*)
-                         val gs7 = unifyCons (env, denv) r concat
-                     in
-                         (*prefaces "The crew" [("nm", p_con env nm),
-                                                ("v", p_con env v),
-                                                ("rest", p_con env rest)];*)
+                         case #1 c' of
+                             L'.CRecord (_, []) =>
+                             let
+                                 val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+                             in
+                                 gs1 @ gs2
+                             end
+                           | L'.CRecord (_, [(x, v)]) =>
+                             let
+                                 val v' = case dom of
+                                              (L'.KUnit, _) => (L'.CUnit, loc)
+                                            | _ => cunif (loc, dom)
+                                 val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc)
 
-                         gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
+                                 val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
+                             in
+                                 gs1 @ gs2 @ gs3
+                             end
+                           | L'.CRecord (_, (x, v) :: rest) =>
+                             let
+                                 val r1 = cunif (loc, (L'.KRecord dom, loc))
+                                 val r2 = cunif (loc, (L'.KRecord dom, loc))
+                                 val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+
+                                 val gs3 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
+                                 val gs4 = unfold (r2, (L'.CRecord (ran, rest), loc))
+                             in
+                                 gs1 @ gs2 @ gs3 @ gs4
+                             end
+                           | L'.CConcat (c1', c2') =>
+                             let
+                                 val r1 = cunif (loc, (L'.KRecord dom, loc))
+                                 val r2 = cunif (loc, (L'.KRecord dom, loc))
+                                 val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+
+                                 val gs3 = unfold (r1, c1')
+                                 val gs4 = unfold (r2, c2')
+                             in
+                                 gs1 @ gs2 @ gs3 @ gs4
+                             end
+                           | _ => raise ex
                      end
-                 else
-                     raise ex
+             in
+                 unfold (r, c)
              end
              handle _ => raise ex
      in
          case (#1 c1, #1 c2) of
-             (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
-             unfold (dom, ran, f, i, r, c2)
-           | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
-             unfold (dom, ran, f, i, r, c1)
+             (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
+             unfold (dom, ran, f, r, c2)
+           | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
+             unfold (dom, ran, f, r, c1)
            | _ => raise ex
      end
 
@@ -890,7 +856,7 @@
                                                                                  (Time.- (Time.now (), befor)))))];*)
                      gs1 @ gs2 @ gs3
                  end
-                 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
+                 handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
              end
 
  and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
@@ -1017,7 +983,7 @@
                  (r := SOME c1All;
                   [])
 
-           | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
+           | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
              (unifyKinds dom1 dom2;
               unifyKinds ran1 ran2;
               [])
@@ -2740,7 +2706,7 @@ fun positive self =
 
               | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
               | CConcat (c1, c2) => none c1 andalso none c2
-              | CFold => true
+              | CMap => true
 
               | CUnit => true
 
@@ -2766,7 +2732,7 @@ fun positive self =
 
               | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
               | CConcat (c1, c2) => pos c1 andalso pos c2
-              | CFold => true
+              | CMap => true
 
               | CUnit => true
 
diff --git a/src/elisp/urweb-defs.el b/src/elisp/urweb-defs.el
index 5551b7a2..e1382692 100644
--- a/src/elisp/urweb-defs.el
+++ b/src/elisp/urweb-defs.el
@@ -107,7 +107,7 @@ notion of \"the end of an outline\".")
                  "if" "then" "else" "case" "of" "fn" "fun" "val" "and"
                  "datatype" "type" "open" "include"
                  urweb-module-head-syms
-                 "con" "fold" "where" "extern" "constraint" "constraints"
+                 "con" "map" "where" "extern" "constraint" "constraints"
                  "table" "sequence" "class" "cookie")
   "Symbols starting an sexp.")
 
@@ -192,7 +192,7 @@ for all symbols and in all lines starting with the given symbol."
   "The starters of new expressions.")
 
 (defconst urweb-exptrail-syms
-  '("if" "then" "else" "case" "of" "fn" "with" "fold"))
+  '("if" "then" "else" "case" "of" "fn" "with" "map"))
 
 (defconst urweb-pipeheads
    '("|" "of" "fun" "fn" "and" "datatype")
diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el
index 223006fc..e7615cc3 100644
--- a/src/elisp/urweb-mode.el
+++ b/src/elisp/urweb-mode.el
@@ -133,7 +133,7 @@ See doc for the variable `urweb-mode-info'."
 
 (defconst urweb-keywords-regexp
   (urweb-syms-re "and" "case" "class" "con" "constraint" "constraints"
-	       "datatype" "else" "end" "extern" "fn" "fold"
+	       "datatype" "else" "end" "extern" "fn" "map"
 	       "fun" "functor" "if" "include"
 	       "of" "open" "let" "in"
 	       "rec" "sequence" "sig" "signature" "cookie"
diff --git a/src/expl.sml b/src/expl.sml
index cce0fc22..c0d291b5 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -54,7 +54,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
-       | CFold of kind * kind
+       | CMap of kind * kind
 
        | CUnit
 
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 2ce0c5e2..7044bfa2 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -149,7 +149,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
-      | CFold _ => string "fold"
+      | CMap _ => string "map"
       | CUnit => string "()"
 
       | CTuple cs => box [string "(",
diff --git a/src/expl_util.sml b/src/expl_util.sml
index d2073a23..a2b5f2f6 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -145,12 +145,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
-              | CFold (k1, k2) =>
+              | CMap (k1, k2) =>
                 S.bind2 (mfk k1,
                          fn k1' =>
                             S.map2 (mfk k2,
                                     fn k2' =>
-                                       (CFold (k1', k2'), loc)))
+                                       (CMap (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
 
diff --git a/src/explify.sml b/src/explify.sml
index a10037ef..a4eab0ba 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -63,7 +63,7 @@ fun explifyCon (c, loc) =
 
       | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
       | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
-      | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
+      | L.CMap (dom, ran) => (L'.CMap (explifyKind dom, explifyKind ran), loc)
 
       | L.CUnit => (L'.CUnit, loc)
 
diff --git a/src/monoize.sml b/src/monoize.sml
index 4efa2fea..898d3e61 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -206,7 +206,7 @@ fun monoType env =
 
                   | L.CRecord _ => poly ()
                   | L.CConcat _ => poly ()
-                  | L.CFold _ => poly ()
+                  | L.CMap _ => poly ()
                   | L.CUnit => poly ()
 
                   | L.CTuple _ => poly ()
diff --git a/src/reduce.sml b/src/reduce.sml
index b428c01f..949b2a6d 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -103,14 +103,13 @@ fun conAndExp (namedC, namedE) =
                         CAbs (_, _, b) =>
                         con (KnownC c2 :: deKnown env) b
 
-                      | CApp ((CApp ((CFold _, _), f), _), i) =>
+                      | CApp ((CMap (dom, ran), _), f) =>
                         (case #1 c2 of
-                             CRecord (_, []) => i
-                           | CRecord (k, (x, c) :: rest) =>
+                             CRecord (_, []) => (CRecord (ran, []), loc)
+                           | CRecord (_, (x, c) :: rest) =>
                              con (deKnown env)
-                                 (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                        (CApp (c1,
-                                               (CRecord (k, rest), loc)), loc)), loc)
+                                 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
+                                           (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
                            | _ => (CApp (c1, c2), loc))                           
 
                       | _ => (CApp (c1, c2), loc)
@@ -130,7 +129,7 @@ fun conAndExp (namedC, namedE) =
                         (CRecord (k, xcs1 @ xcs2), loc)
                       | _ => (CConcat (c1, c2), loc)
                 end
-              | CFold _ => all
+              | CMap _ => all
 
               | CUnit => all
 
diff --git a/src/source.sml b/src/source.sml
index a5c86f66..d70d0f5d 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -60,7 +60,7 @@ datatype con' =
 
        | CRecord of (con * con) list
        | CConcat of con * con
-       | CFold
+       | CMap
 
        | CUnit
 
diff --git a/src/source_print.sml b/src/source_print.sml
index d6568efe..148157c2 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -139,7 +139,7 @@ fun p_con' par (c, _) =
                                               string "++",
                                               space,
                                               p_con c2])
-      | CFold => string "fold"
+      | CMap => string "map"
 
       | CUnit => string "()"
 
diff --git a/src/urweb.grm b/src/urweb.grm
index 5f2c0575..d425caec 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -184,7 +184,7 @@ fun tagIn bt =
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
  | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
- | CON | LTYPE | VAL | REC | AND | FUN | FOLD | UNIT | KUNIT | CLASS
+ | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS
  | DATATYPE | OF
  | TYPE | NAME
  | ARROW | LARROW | DARROW | STAR | SEMI
@@ -681,7 +681,7 @@ cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
        | path DOT INT                   (CProj ((CVar path, s (pathleft, pathright)), Int64.toInt INT),
                                          s (pathleft, INTright))
        | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
-       | FOLD                           (CFold, s (FOLDleft, FOLDright))
+       | MAP                            (CMap, s (MAPleft, MAPright))
        | UNIT                           (CUnit, s (UNITleft, UNITright))
        | LPAREN ctuplev RPAREN          (CTuple ctuplev, s (LPARENleft, RPARENright))
 
diff --git a/src/urweb.lex b/src/urweb.lex
index aef68ad1..29e07194 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -290,6 +290,7 @@ notags = [^<{\n]+;
 <INITIAL> "and"       => (Tokens.AND (pos yypos, pos yypos + size yytext));
 <INITIAL> "fun"       => (Tokens.FUN (pos yypos, pos yypos + size yytext));
 <INITIAL> "fn"        => (Tokens.FN (pos yypos, pos yypos + size yytext));
+<INITIAL> "map"       => (Tokens.MAP (pos yypos, pos yypos + size yytext));
 <INITIAL> "fold"      => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
 <INITIAL> "case"      => (Tokens.CASE (pos yypos, pos yypos + size yytext));
 <INITIAL> "if"        => (Tokens.IF (pos yypos, pos yypos + size yytext));