[Implemented the simply typed lambda calculus with multi-argument functions.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080314052458] hunk ./Wand2.agda 6
-{-# OPTIONS --no-positivity-check
-  #-}
-
-open import Data.Nat
+open import Data.Star.Nat
hunk ./Wand2.agda 15
-open import SimplyTyped.TypeSystem
-open import SimplyTyped.ApplicativeStructure
-import SimplyTyped.Environment as Env
-open import Logic
+open import Data.Star
+open import Data.Star.List
+open import Data.Star.Decoration
+import Data.Star.Environment as Env
+open import Data.Unit
+open import Relation.Binary
+open import Data.Function
+
+-- The language used is the simply typed lambda calculus with
+-- multi-argument functions.
+
+infixl 70 _·_
+infix  50 λ_
+infixr 30 _→_
+infix   4 _⊢_
+
+data Ty : Set where
+  base : ℕ -> Ty
+  _→_  : [ Ty ] -> Ty -> Ty
+
+open Env Ty
+
+mutual
+
+  data _⊢_ : Ctxt -> Ty -> Set where
+    var  : forall {Γ τ}    -> Γ ∋ τ -> Γ ⊢ τ
+    λ_   : forall {Γ Γ⁺ τ} -> Γ ▻▻ Γ⁺ ⊢ τ -> Γ ⊢ Γ⁺ → τ
+    _·_  : forall {Γ Γ⁺ τ} -> Γ ⊢ Γ⁺ → τ -> Args Γ Γ⁺ -> Γ ⊢ τ
+
+  -- An argument sequence is defined as a context extension decorated
+  -- with terms.
+
+  Args : Ctxt -> Ctxt -> Set
+  Args Γ Γ⁺ = All (\σ -> Γ ⊢ σ) Γ⁺
+
+------------------------------------------------------------------------
+-- An example, just to see how things work
+
+module Example (x : ε ⊢ base 0#) (y : ε ⊢ base 1#) where
+
+  Types : Ctxt
+  Types = ε ▻ base 0# ▻ base 1#
hunk ./Wand2.agda 58
--- 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.)
+  fun : ε ⊢ Types → base 0#
+  fun = λ var (vs vz)
+
+  args : Args ε Types
+  args = ε ▻ ↦ x ▻ ↦ y
+
+  application : ε ⊢ base 0#
+  application = fun · args
hunk ./Wand2.agda 82
-mutual
+⟦_⟧⋆ : Ty -> Set
+⟦ base n ⟧⋆ = Base n
+⟦ Γ⁺ → τ ⟧⋆ = Env ⟦_⟧⋆ Γ⁺ -> Cont ⟦ τ ⟧⋆
hunk ./Wand2.agda 86
-  ⟦_⟧⋆ : Ty -> Set
-  ⟦ base n ⟧⋆ = Base n
-  ⟦ σ → τ  ⟧⋆ = ⟦ σ ⟧⋆ -> Cont ⟦ τ ⟧⋆
+module Alternative where
hunk ./Wand2.agda 88
--- Environments.
+  -- The function above is terminating, since ⟦_⟧⋆ is only applied to
+  -- the elements of Γ⁺. We could make this explicit by defining a new
+  -- type here instead of using All, but I want to use Data.Star for
+  -- all sequences. Note that defining a new type would imply using a
+  -- form of induction-recursion, by the way:
hunk ./Wand2.agda 94
-open Env ⟦_⟧⋆
+  mutual
hunk ./Wand2.agda 96
--- The semantics.
+    data SemArgs : Ctxt -> Set where
+      ∅   : SemArgs ε
+      _▷_ : forall {Γ σ} -> SemArgs Γ -> ⟦ σ ⟧⋆' -> SemArgs (Γ ▻ σ)
hunk ./Wand2.agda 100
-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))
-  }
+    ⟦_⟧⋆' : Ty -> Set
+    ⟦ base n ⟧⋆' = Base n
+    ⟦ Γ⁺ → τ ⟧⋆' = SemArgs Γ⁺ -> Cont ⟦ τ ⟧⋆'
hunk ./Wand2.agda 104
-module Sem = ApplicativeStructure semantics
-open Sem using (Dom; ⟦_⟧)
+-- The interpreter.
hunk ./Wand2.agda 106
-------------------------------------------------------------------------
--- First step of the derivation: name subexpressions
-
-module Step₁ where
-
-  *fetch : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ
-  *fetch = Sem.Var
+-- These two functions are also terminating. Due to the use of
+-- "reverse" this is not apparent to the termination checker, though.
hunk ./Wand2.agda 109
-  *close : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ)
-  *close {τ = τ} = Sem.Lam {τ = τ}
+mutual
hunk ./Wand2.agda 111
-  -- App is broken up into two parts.
+  ⟦_⟧ : forall {Γ σ} -> Γ ⊢ σ -> Env ⟦_⟧⋆ Γ -> Cont ⟦ σ ⟧⋆
+  ⟦ var x  ⟧ ρ k = k (Env-lookup x ρ)
+  ⟦ λ t    ⟧ ρ k = k (\vs k' -> ⟦ t ⟧ (ρ ▻▻▻ vs) k')
+  ⟦ t · ts ⟧ ρ k = ⟦ t • ε • reverse id ts ⟧ ρ k
hunk ./Wand2.agda 116
-  Dom' : Ctxt -> Ty -> Ty -> Set
-  Dom' Γ σ τ = ⟦ σ ⟧⋆ -> Dom Γ τ
+  -- Note that this function exhibits a clowns/jokers structure, by
+  -- the way (a zipper where the things on the two sides have
+  -- different types).
+
+  ⟦_•_•_⟧ : forall {Γ Γ⁺ Δ⁺ τ} ->
+            Γ ⊢ Γ⁺ → τ -> Env ⟦_⟧⋆ Δ⁺ ->
+            Star (flip₁ (DecoratedWith (\σ -> Γ ⊢ σ)))
+                 (nonEmpty Δ⁺) (nonEmpty Γ⁺) ->
+            Env ⟦_⟧⋆ Γ -> Cont ⟦ τ ⟧⋆
+  ⟦ t • ρ' • ε        ⟧ ρ k = ⟦ t ⟧ ρ (\v -> v ρ' k)
+  ⟦ t • ρ' • ↦ a ◅ as ⟧ ρ k = ⟦ a ⟧ ρ (\v -> ⟦ t • ρ' ▻ ↦ v • as ⟧ ρ k)
hunk ./Wand2.agda 128
-  *evfn : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom' Γ σ τ
-  *evfn c = \v₂ ρ k -> c ρ (\v₁ -> v₁ v₂ k)
+------------------------------------------------------------------------
+-- Back to the example
hunk ./Wand2.agda 131
-  *jsr : forall {Γ σ τ} -> Dom Γ σ -> Dom' Γ σ τ -> Dom Γ τ
-  *jsr c cs = \ρ k -> c ρ \v -> cs v ρ k
+module Example₂ (x : ε ⊢ base 0#) (y : ε ⊢ base 1#) where
hunk ./Wand2.agda 133
-  -- We can get back App by combining the parts.
+  open Example x y
hunk ./Wand2.agda 135
-  correct : forall {Γ σ τ} (v₁ : Dom Γ (σ → τ)) (v₂ : Dom Γ σ) ->
-            *jsr {σ = σ} {τ = τ} v₂ (*evfn {σ = σ} {τ = τ} v₁) ≡
-            Sem.App {σ = σ} {τ = τ} v₁ v₂
-  correct v₁ v₂ = ≡-refl
+  sem : Cont (Base 0#)
+  sem = ⟦ application ⟧ ε