[Started formalising another of Wand's papers.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080314011924
 + He claims that the method used in that paper is easier than the one
   I tried formalising in Wand.agda.
] addfile ./README
hunk ./README 1
+The code in this repository uses code from the Agda standard library
+and from my library defining the simply typed lambda calculus.
+
+Note that you have to use library code from a suitable date to make
+things work. (If you use only the patches originating before the
+creation date of the last patch in this repository things usually work
+out.)
addfile ./Wand2.agda
hunk ./Wand2.agda 1
+------------------------------------------------------------------------
+-- Based on "From Interpreter to Compiler: A Representational
+-- Derivation" by Mitchell Wand
+------------------------------------------------------------------------
+
+{-# OPTIONS --no-positivity-check
+  #-}
+
+open import Data.Nat
+
+module Wand2
+         -- Semantic domains of base types.
+         (Base : ℕ -> Set)
+         -- The result type for the continuations.
+         (Result : Set)
+         where
+
+open import SimplyTyped.TypeSystem
+open import SimplyTyped.ApplicativeStructure
+import SimplyTyped.Environment as Env
+open import Logic
+
+-- The language used is the simply typed lambda calculus. (I only
+-- treat the case of single-argument lambdas; Wand's paper has
+-- multi-argument functions.)
+
+------------------------------------------------------------------------
+-- The semantics which Wand starts off with
+
+-- Continuations.
+
+Cont : Set -> Set
+Cont A = (A -> Result) -> Result
+
+-- Semantic domains. Note that the code in Wand's paper is untyped.
+-- Before I understood what the semantic domains should be I had
+-- trouble understanding his code. Wand presumably had something
+-- resembling these types in his head; writing them out would have
+-- made his paper more accessible (at least to people like me who
+-- usually write interpreters in a different way).
+
+mutual
+
+  ⟦_⟧⋆ : Ty -> Set
+  ⟦ base n ⟧⋆ = Base n
+  ⟦ σ → τ  ⟧⋆ = ⟦ σ ⟧⋆ -> Cont ⟦ τ ⟧⋆
+
+-- Environments.
+
+open Env ⟦_⟧⋆
+
+-- The semantics.
+
+semantics : ApplicativeStructure
+semantics = record
+  { Dom = \Γ σ -> Env Γ -> Cont ⟦ σ ⟧⋆
+  ; Var = \x ρ k -> k (lookup x ρ)
+  ; Lam = \t ρ k -> k (\v k' -> t (ρ ▷ v) k')
+  ; App = \t₁ t₂ ρ k -> t₂ ρ (\v₂ -> t₁ ρ (\v₁ -> v₁ v₂ k))
+  }
+
+module Sem = ApplicativeStructure semantics
+open Sem using (Dom; ⟦_⟧)
+
+------------------------------------------------------------------------
+-- First step of the derivation: name subexpressions
+
+module Step₁ where
+
+  *fetch : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ
+  *fetch = Sem.Var
+
+  *close : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ)
+  *close {τ = τ} = Sem.Lam {τ = τ}
+
+  -- App is broken up into two parts.
+
+  Dom' : Ctxt -> Ty -> Ty -> Set
+  Dom' Γ σ τ = ⟦ σ ⟧⋆ -> Dom Γ τ
+
+  *evfn : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom' Γ σ τ
+  *evfn c = \v₂ ρ k -> c ρ (\v₁ -> v₁ v₂ k)
+
+  *jsr : forall {Γ σ τ} -> Dom Γ σ -> Dom' Γ σ τ -> Dom Γ τ
+  *jsr c cs = \ρ k -> c ρ \v -> cs v ρ k
+
+  -- We can get back App by combining the parts.
+
+  correct : forall {Γ σ τ} (v₁ : Dom Γ (σ → τ)) (v₂ : Dom Γ σ) ->
+            *jsr {σ = σ} {τ = τ} v₂ (*evfn {σ = σ} {τ = τ} v₁) ≡
+            Sem.App {σ = σ} {τ = τ} v₁ v₂
+  correct v₁ v₂ = ≡-refl