update code examples

slides/code-examples/example.hs

@@ -8,6 +8,7 @@ main = do
   print (hd []::[String])
 
 reverse :: [a] -> [a]
-reverse = reverseAcc []
+reverse l = reverseAcc l []
   where
-    reverseAcc = foldl (flip (:))
+    reverseAcc []     a = a
+    reverseAcc (x:xs) a = reverseAcc xs (x:a)

slides/code-examples/reverse.agda

@@ -13,16 +13,12 @@ module reverse where
     now : A → Delay A
     later : ∞ (Delay A) → Delay A
 
-  foldl : ∀ {A B : Set} → (A → B → A) → A → Colist B → Delay A
-  foldl c n [] = now n
-  foldl c n (x ∷ xs) = later (♯ foldl c (c n x) (♭ xs))
-
-  -- reversing possibly infinite lists
   reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
   reverse {A} = reverseAcc []
     where
       reverseAcc : Colist A → Colist A → Delay (Colist A)
-      reverseAcc = foldl (λ xs x → x ∷ (♯ xs)) -- 'flip _∷_' with extra steps
+      reverseAcc [] a = now a
+      reverseAcc (x ∷ xs) a = later (♯ reverseAcc (♭ xs) (x ∷ (♯ a)))
 
   run_for_steps : ∀ {A : Set} → Delay A → ℕ → Delay A
   run now   x for n     steps = now x

slides/sections/00_intro.tex

@@ -19,9 +19,10 @@ head (x:xs) = x
     \vskip 1cm
     \begin{minted}{agda}
 reverse :: [a] -> [a]
-reverse = reverseAcc []
+reverse l = reverseAcc l []
   where
-    reverseAcc = foldl (flip (:))
+    reverseAcc []     a = a
+    reverseAcc (x:xs) a = reverseAcc xs (x:a)
 \end{minted}
     
     \mycallout<4->{21, 2}{
@@ -83,14 +84,11 @@ run later x for suc n steps = run ♭ x for n steps
 \begin{frame}[c, fragile]{Partiality in Agda}{Reversing (possibly infinite) lists}
 \centering
 \begin{minted}{agda}
-foldl : ∀ {A B : Set} → (A → B → A) → A → Colist B → Delay A
-foldl c n []       = now n
-foldl c n (x ∷ xs) = later (♯ foldl c (c n x) (♭ xs))
-
 reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
 reverse {A} = reverseAcc []
   where
     reverseAcc : Colist A → Colist A → Delay (Colist A)
-    reverseAcc = foldl (λ xs x → x ∷ (♯ xs))
+    reverseAcc [] a = now a
+    reverseAcc (x ∷ xs) a = later (♯ reverseAcc (♭ xs) (x ∷ (♯ a)))
 \end{minted}
 \end{frame}