[Started extending the calculation to exceptions.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080207023248
 + The calculation is mostly finished, but suffers from the same
   problem as the one in HuttonsRazor.agda.
 + Note that my calculation is not quite identical to the Hutton/Wright
   one.
] addfile ./Exceptions.agda
hunk ./Exceptions.agda 1
+-- Formalisation of "Calculating an Exceptional Machine" by Graham
+-- Hutton and Joel Wright.
+
+-- Note that the development below does not quite correspond to what
+-- Graham and Joel did. I tried following the ideas from
+-- HuttonsRazor.agda without looking at the paper, and ended up with a
+-- slightly different end product. The difference seems to be that I
+-- treated the computations in the Maybe monad as opaque (analogously
+-- to the additions), but it seems reasonable to incorporate those
+-- directly into the abstract machine, which I believe that Graham and
+-- Joel did.
+
+-- This module formalises Hutton's razor plus exceptions.
+
+open import Logic
+
+module Exceptions
+         -- Assume extensionality; it appears to be necessary for a
+         -- proof below.
+         (≡-ext : forall {a b : Set} {f g : a -> b} ->
+                    (forall x -> f x ≡ g x) -> f ≡ g)
+       where
+
+open import Data.Nat
+open import Data.Maybe
+open import Category.Monad
+open import GVec
+open import Vec
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Derivation
+open RawMonadPlus MaybeMonadPlus renaming (_++_ to _<+>_)
+
+------------------------------------------------------------------------
+-- Expressions
+
+data Expr : Set where
+  val   : ℕ -> Expr
+  _⊕_   : Expr -> Expr -> Expr
+  throw : Expr
+  catch : Expr -> Expr -> Expr
+
+⟦_⟧ : Expr -> Maybe ℕ
+⟦ val n   ⟧     = return n
+⟦ e₁ ⊕ e₂ ⟧     = pure _+_ <*> ⟦ e₁ ⟧ <*> ⟦ e₂ ⟧
+⟦ throw   ⟧     = mzero
+⟦ catch e₁ e₂ ⟧ = ⟦ e₁ ⟧ <+> ⟦ e₂ ⟧
+
+------------------------------------------------------------------------
+-- Calculation of an abstract machine
+
+module Calculational where
+
+  -- ⑴ Add continuations.
+
+  module Step₁ where
+
+    Cont : Set
+    Cont = Maybe ℕ -> Maybe ℕ
+
+    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 -> Maybe ℕ
+      eval e c = witness (evalP e c)
+
+      evalP : (e : Expr) (c : Cont) -> EqualTo (c ⟦ e ⟧)
+      evalP (val n)       c = ▷ begin c (return n) ∎
+      evalP (e₁ ⊕ e₂)     c = ▷ begin
+        c (pure _+_ <*> ⟦ e₁ ⟧ <*> ⟦ e₂ ⟧)
+          ≡⟨ ≡-refl ⟩
+        (\m -> c (pure _+_ <*> m <*> ⟦ e₂ ⟧)) ⟦ e₁ ⟧
+          ≡⟨ proof (evalP e₁ (\m -> c (pure _+_ <*> m <*> ⟦ e₂ ⟧))) ⟩
+        eval e₁ (\m -> c (pure _+_ <*> m <*> ⟦ e₂ ⟧))
+          ≡⟨ ≡-refl ⟩
+        eval e₁ (\m -> (\n -> c (pure _+_ <*> m <*> n)) ⟦ e₂ ⟧)
+          ≡⟨ ≡-cong (eval e₁)
+               (≡-ext (\m -> proof (evalP e₂
+                        (\n -> c (pure _+_ <*> m <*> n))))) ⟩
+        eval e₁ (\m -> eval e₂ (\n -> c (pure _+_ <*> m <*> n)))
+          ∎
+      evalP throw         c = ▷ begin c mzero ∎
+      evalP (catch 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 -> Maybe ℕ -> Cont
+    c₂ c m = \n -> c (pure _+_ <*> m <*> n)
+
+    c₃ : Expr -> Cont -> Cont
+    c₃ e c = \m -> eval e (c₂ c m)
+
+    c₄ : Cont -> Maybe ℕ -> Cont
+    c₄ c m = \n -> c (m <+> n)
+
+    c₅ : Expr -> Cont -> Cont
+    c₅ e c = \m -> eval e (c₄ c m)
+
+    -- The top-level evaluation function can be recovered by using the
+    -- identity continuation.
+
+    ⟦_⟧' : Expr -> Maybe ℕ
+    ⟦ 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.
+
+  module Step₂ where
+
+    data Cont : Set where
+      c₁ : Cont
+      c₂ : Cont -> Maybe ℕ -> Cont
+      c₃ : Expr -> Cont -> Cont
+      c₄ : Cont -> Maybe ℕ -> Cont
+      c₅ : Expr -> Cont -> Cont
+
+    -- Define the semantics of the continuations in terms of the
+    -- higher-order ones.
+
+    ⟦_⟧c : Cont -> Step₁.Cont
+    ⟦ c₁     ⟧c = Step₁.c₁
+    ⟦ c₂ c n ⟧c = Step₁.c₂ ⟦ c ⟧c n
+    ⟦ c₃ e c ⟧c = Step₁.c₃ e ⟦ c ⟧c
+    ⟦ c₄ c n ⟧c = Step₁.c₄ ⟦ c ⟧c n
+    ⟦ c₅ e c ⟧c = Step₁.c₅ e ⟦ c ⟧c
+
+    mutual
+
+      -- Define a variant of Step₁.eval which uses first-order
+      -- continuations.
+
+      eval : Expr -> Cont -> Maybe ℕ
+      eval e c = witness (evalP e c)
+
+      evalP : (e : Expr) (c : Cont) ->
+              EqualTo (Step₁.eval e ⟦ c ⟧c)
+      evalP (val n)       c = ▷ begin ⟦ c ⟧c (return n) ∎
+      evalP (e₁ ⊕ e₂)     c = ▷ begin
+        Step₁.eval e₁ (\m -> Step₁.eval e₂
+                         (\n -> ⟦ c ⟧c (pure _+_ <*> m <*> n)))
+          ≡⟨ ≡-refl ⟩
+        Step₁.eval e₁ ⟦ c₃ e₂ c ⟧c
+          ≡⟨ proof (evalP e₁ (c₃ e₂ c)) ⟩
+        eval e₁ (c₃ e₂ c)
+          ∎
+      evalP throw         c = ▷ begin ⟦ c ⟧c mzero ∎
+      evalP (catch e₁ e₂) c = ▷ begin
+        Step₁.eval e₁ (\m -> Step₁.eval e₂ (\n -> ⟦ c ⟧c (m <+> n)))
+          ≡⟨ ≡-refl ⟩
+        Step₁.eval e₁ ⟦ c₅ e₂ c ⟧c
+          ≡⟨ proof (evalP e₁ (c₅ e₂ c)) ⟩
+        eval e₁ (c₅ e₂ c)
+          ∎
+
+    mutual
+
+      -- Also make sure that the semantics of continuations does not
+      -- refer to Step₁.eval.
+
+      -- Note that eval above uses ⟦_⟧c, so it has to be updated.
+
+      -- Note that the code in this block does not please the
+      -- termination checker.
+
+      ⟦_⟧c' : Cont -> Step₁.Cont
+      ⟦ c ⟧c' n = witness (cSem c n)
+
+      eval' : Expr -> Cont -> Maybe ℕ
+      eval' e c = witness (evalP' e c)
+
+      cSem : (c : Cont) (n : Maybe ℕ) -> EqualTo (⟦ c ⟧c n)
+      cSem c₁       n = ▷ begin n ∎
+      cSem (c₂ c m) n = ▷ begin
+        ⟦ c ⟧c (pure _+_ <*> m <*> n)
+          ≡⟨ proof (cSem c (pure _+_ <*> m <*> n)) ⟩
+        ⟦ c ⟧c' (pure _+_ <*> m <*> n)
+          ∎
+      cSem (c₃ e c) n = ▷ begin
+        Step₁.eval e ⟦ c₂ c n ⟧c
+          ≡⟨ proof (evalP e (c₂ c n)) ⟩
+        eval e (c₂ c n)
+          ≡⟨ proof (evalP' e (c₂ c n)) ⟩
+        eval' e (c₂ c n)
+          ∎
+      cSem (c₄ c m) n = ▷ begin
+        ⟦ c ⟧c (m <+> n)
+          ≡⟨ proof (cSem c (m <+> n)) ⟩
+        ⟦ c ⟧c' (m <+> n)
+          ∎
+      cSem (c₅ e c) n = ▷ begin
+        Step₁.eval e ⟦ c₄ c n ⟧c
+          ≡⟨ proof (evalP e (c₄ c n)) ⟩
+        eval e (c₄ c n)
+          ≡⟨ proof (evalP' e (c₄ c n)) ⟩
+        eval' e (c₄ c n)
+          ∎
+
+      evalP' : (e : Expr) (c : Cont) ->
+               EqualTo (eval e c)
+      evalP' (val n) c = ▷ begin
+        ⟦ c ⟧c (return n)
+          ≡⟨ proof (cSem c (return n)) ⟩
+        ⟦ c ⟧c' (return n)
+          ∎
+      evalP' (e₁ ⊕ e₂) c = ▷ begin
+        eval e₁ (c₃ e₂ c)
+          ≡⟨ proof (evalP' e₁ (c₃ e₂ c)) ⟩
+        eval' e₁ (c₃ e₂ c)
+          ∎
+      evalP' throw c = ▷ begin
+        ⟦ c ⟧c mzero
+          ≡⟨ proof (cSem c mzero) ⟩
+        ⟦ c ⟧c' mzero
+          ∎
+      evalP' (catch e₁ e₂) c = ▷ begin
+        eval e₁ (c₅ e₂ c)
+          ≡⟨ proof (evalP' e₁ (c₅ e₂ c)) ⟩
+        eval' e₁ (c₅ e₂ c)
+          ∎
+
+    -- The top-level evaluation function can be recovered.
+
+    ⟦_⟧' : Expr -> Maybe ℕ
+    ⟦ e ⟧' = eval' e c₁
+
+    correct : forall e -> ⟦ e ⟧ ≡ ⟦ e ⟧'
+    correct e = begin
+      ⟦ e ⟧
+        ≡⟨ Step₁.correct e ⟩
+      Step₁.⟦_⟧' e
+        ≡⟨ proof (evalP e c₁) ⟩
+      eval e c₁
+        ≡⟨ proof (evalP' e c₁) ⟩
+      ⟦ e ⟧'
+        ∎
+
+  -- ⑶ Refactor. TODO.