[Finished the Hutton/Wright derivation. Noted that it has a bug.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080207005559] hunk ./HuttonsRazor.agda 123
-  Cont : Set
-  Cont = ℕ -> ℕ
+  -- ⑴ Add continuations.
+
+  module Step₁ where
+
+    Cont : Set
+    Cont = ℕ -> ℕ
+
+    mutual
+
+      -- Let us derive a function eval which satisfies
+      --   eval e c ≡ c ⟦ e ⟧.
+      -- The derivation is done in evalP, whose type guarantees
+      -- correctness.
+
+      eval : Expr -> Cont -> ℕ
+      eval e c = witness (evalP e c)
+
+      evalP : (e : Expr) (c : Cont) -> EqualTo (c ⟦ e ⟧)
+      evalP (val n)   c = ▷ begin c n ∎
+      evalP (e₁ ⊕ e₂) c = ▷ begin
+        c (⟦ e₁ ⟧ + ⟦ e₂ ⟧)
+          ≡⟨ ≡-refl ⟩
+        (\m -> c (m + ⟦ e₂ ⟧)) ⟦ e₁ ⟧
+          ≡⟨ proof (evalP e₁ (\m -> c (m + ⟦ e₂ ⟧))) ⟩
+        eval e₁ (\m -> c (m + ⟦ e₂ ⟧))
+          ≡⟨ ≡-refl ⟩
+        eval e₁ (\m -> (\n -> c (m + n)) ⟦ e₂ ⟧)
+          ≡⟨ ≡-cong (eval e₁)
+                    (≡-ext (\m -> proof (evalP e₂ (\n -> c (m + n))))) ⟩
+        eval e₁ (\m -> eval e₂ (\n -> c (m + n)))
+          ∎
+
+    -- The code above contains some continuations. Let us name them.
+    -- The identity continuation, used to connect eval to ⟦_⟧, is also
+    -- named.
+
+    c₁ : Cont
+    c₁ = \n -> n
+
+    c₃ : ℕ -> Cont -> Cont
+    c₃ m c = \n -> c (m + n)
+
+    c₂ : Expr -> Cont -> Cont
+    c₂ e c = \m -> eval e (c₃ m c)
+
+    -- The top-level evaluation function can be recovered by using the
+    -- identity continuation.
+
+    ⟦_⟧' : Expr -> ℕ
+    ⟦ e ⟧' = eval e c₁
+
+    correct : forall e -> ⟦ e ⟧ ≡ ⟦ e ⟧'
+    correct e = proof (evalP e c₁)
+
+  -- ⑵ Defunctionalise, i.e. get rid of the higher-order
+  --   continuations.
hunk ./HuttonsRazor.agda 180
-  mutual
+  module Step₂ where
hunk ./HuttonsRazor.agda 182
-    ⟦_⟧' : Expr -> Cont -> ℕ
-    ⟦ e ⟧' c = witness (eval' e c)
+    data Cont : Set where
+      c₁ : Cont
+      c₂ : Expr -> Cont -> Cont
+      c₃ : ℕ -> Cont -> Cont
hunk ./HuttonsRazor.agda 187
-    eval' : (e : Expr) (c : Cont) -> EqualTo (c ⟦ e ⟧)
-    eval' (val n)   c = ▷ begin c n ∎
-    eval' (e₁ ⊕ e₂) c = ▷ begin
-      c (⟦ e₁ ⟧ + ⟦ e₂ ⟧)
-        ≡⟨ ≡-refl ⟩
-      (\m -> c (m + ⟦ e₂ ⟧)) ⟦ e₁ ⟧
-        ≡⟨ proof (eval' e₁ (\m -> c (m + ⟦ e₂ ⟧))) ⟩
-      ⟦ e₁ ⟧' (\m -> c (m + ⟦ e₂ ⟧))
-        ≡⟨ ≡-refl ⟩
-      ⟦ e₁ ⟧' (\m -> (\n -> c (m + n)) ⟦ e₂ ⟧)
-        ≡⟨ ≡-cong ⟦ e₁ ⟧'
-                  (≡-ext (\m -> proof (eval' e₂ (\n -> c (m + n))))) ⟩
-      ⟦ e₁ ⟧' (\m -> ⟦ e₂ ⟧' (\n -> c (m + n)))
+    -- Define the semantics of the continuations in terms of the
+    -- higher-order ones.
+
+    ⟦_⟧c : Cont -> Step₁.Cont
+    ⟦ c₁     ⟧c = Step₁.c₁
+    ⟦ c₂ e c ⟧c = Step₁.c₂ e ⟦ c ⟧c
+    ⟦ c₃ m c ⟧c = Step₁.c₃ m ⟦ c ⟧c
+
+    mutual
+
+      -- Define a variant of Step₁.eval which uses first-order
+      -- continuations.
+
+      -- Also make sure that the semantics of continuations does not
+      -- refer to Step₁.eval (via Step₁.c₂).
+
+      eval : Expr -> Cont -> ℕ
+      eval e c = witness (evalP e c)
+
+      ⟦_⟧c' : Cont -> Step₁.Cont
+      ⟦ c ⟧c' n = witness (cSem c n)
+
+      evalP : (e : Expr) (c : Cont) ->
+              EqualTo (Step₁.eval e ⟦ c ⟧c)
+      evalP (val n) c = ▷ begin
+        ⟦ c ⟧c n
+          ≡⟨ proof (cSem c n) ⟩
+        ⟦ c ⟧c' n
+          ∎
+      evalP (e₁ ⊕ e₂) c = ▷ begin
+        Step₁.eval e₁ (\m -> Step₁.eval e₂ (\n -> ⟦ c ⟧c (m + n)))
+          ≡⟨ ≡-refl ⟩
+        Step₁.eval e₁ (Step₁.c₂ e₂ ⟦ c ⟧c)
+          ≡⟨ proof (evalP e₁ (c₂ e₂ c)) ⟩
+        eval e₁ (c₂ e₂ c)
+          ∎
+
+      cSem : (c : Cont) (n : ℕ) -> EqualTo (⟦ c ⟧c n)
+      cSem c₁       n = ▷ begin n ∎
+      cSem (c₂ e c) n = ▷ begin
+        Step₁.eval e (Step₁.c₃ n ⟦ c ⟧c)
+          ≡⟨ ≡-refl  ⟩
+        Step₁.eval e ⟦ c₃ n c ⟧c
+          ≡⟨ proof (evalP e (c₃ n c)) ⟩
+        eval e (c₃ n c)
+          ∎
+      cSem (c₃ m c) n = ▷ begin
+        ⟦ c ⟧c (m + n)
+          ≡⟨ proof (cSem c (m + n)) ⟩
+        ⟦ c ⟧c' (m + n)
+          ∎
+
+    -- The top-level evaluation function can be recovered.
+
+    ⟦_⟧' : Expr -> ℕ
+    ⟦ e ⟧' = eval e c₁
+
+    correct : forall e -> ⟦ e ⟧ ≡ ⟦ e ⟧'
+    correct e = begin
+      ⟦ e ⟧
+        ≡⟨ Step₁.correct e ⟩
+      Step₁.⟦_⟧' e
+        ≡⟨ proof (evalP e c₁) ⟩
+      ⟦ e ⟧'
hunk ./HuttonsRazor.agda 253
+  -- ⑶ Refactor.
+
+  module Step₃ where
+
+    -- Note that the Hutton/Wright paper contains a slight mistake
+    -- here: They define Step₂.eval by using Step₂.⟦_⟧c, but in this
+    -- step they assume (with no comment) that Step₂.⟦_⟧c and
+    -- Step₂.⟦_⟧c' are the same thing (they overload the name "apply",
+    -- so this is hard to spot in the paper).
+    --
+    -- I tried to fix their mistake (see the val case of Step₂.evalP),
+    -- but this makes the termination checker complain.
+
+    open Step₂ public
+      using (Cont; eval)
+      renaming ( c₁ to STOP; c₂ to EVAL; c₃ to ADD
+               ; ⟦_⟧c' to exec; ⟦_⟧' to run
+               )
+