Simplify examples and remove `map`.

1 files changed, 40 insertions, 18 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 14d8c94..95d9be3 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -226,8 +226,11 @@ let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun index =>
-    let x = map (fun x => ih (snoc index x)) (heap index) in
-    match x with
+    let update = fun i => ih (snoc index i) in
+    let x = match heap (length, idxs) with
+      Leaf i        => Leaf (update i)
+    | Branch (i, j) => Branch (update i, update j)
+    in match x with
       Leaf f        => f
     | Branch (f, g) => fun x => f (g x)
   in go []
@@ -235,6 +238,26 @@ let compose (depth, heap) =
 \vspace{-\baselineskip}
 \end{listing}
 
+To keep our example small, we will perform a commuting conversion
+within \systemtinline{compose} to reduce the two match statements into
+one. After some further beta reductions, we obtain the simplified
+defintion
+
+\begin{listing}[H]
+\begin{systemt}
+let compose' (depth, heap) =
+  let go = primrec depth with
+    Zero   => arb
+  | Suc ih => fun index =>
+    let update = fun i => ih (snoc index i) in
+    match heap (length, idxs) with
+      Leaf i        => update i
+    | Branch (i, j) => fun x => update i (update j x)
+  in go []
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
 \subsection{Phase 3: Encoding Lists}%
 \label{subsec:lists}
 
@@ -342,19 +365,18 @@ let balanced n f = primrec n with
 \vspace{-\baselineskip}
 \end{listing}
 
-And \systemtinline{compose} reduces to:
+And \systemtinline{compose'} reduces to:
 \begin{listing}[H]
 \begin{systemt}
-let compose (depth, heap) =
+let compose' (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun (length, idxs) =>
-    let x = map (fun x => ih (Suc length, fun i =>
-                  if i == length then x else idxs i))
-                (heap (length, idxs))
-    in match x with
-      Leaf f        => f
-    | Branch (f, g) => fun x => f (g x)
+    let update = fun i => ih (Suc length, fun j =>
+                   if j == length then i else idxs j)
+    match heap (length, idxs) with
+      Leaf i        => update i
+    | Branch (i, j) => fun x => update i (update j x)
   in go
 \end{systemt}
 \vspace{-\baselineskip}
@@ -404,21 +426,21 @@ let balanced n f = primrec n with
 \vspace{-\baselineskip}
 \end{listing}
 
-The \systemtinline{compose} example demonstrates how pattern matching
+The \systemtinline{compose'} example demonstrates how pattern matching
 is encoded:
 
 \begin{listing}[H]
 \begin{systemt}
-let compose (depth, heap) =
+let compose' (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun (length, idxs) =>
-    let (tag, v) = map (fun x => ih (Suc length, fun i =>
-                         if i == length then x else idxs i))
-                       (heap (length, idxs))
-    in match tag with
-      0 => prj v 0
-    | 1 => let (f, g) = prj v 1 in fun x => f (g x)
+    let update = fun i => ih (Suc length, fun j =>
+                   if j == length then i else idxs j)
+    let (tag, v) = heap (length, idxs) in
+    match tag with
+      0 => update (prj v 0)
+    | 1 => let (i, j) = prj v 1 in fun x => update i (update j x)
   in go
 \end{systemt}
 \vspace{-\baselineskip}