module mono where open import Data.Nat open import Function open import Relation.Binary.PropositionalEquality infixr 5 _⇒_ -- type data typ : Set where Nat : typ _⇒_ : typ → typ → typ -- source term mutual data value[_]_ (var : typ → Set) : typ → Set where Var : {τ₁ : typ} → var τ₁ → value[ var ] τ₁ Num : (n : ℕ) → value[ var ] Nat Fun : {τ₁ τ₂ : typ} → (e₁ : var τ₂ → term[ var ] τ₁) → value[ var ] (τ₂ ⇒ τ₁) data term[_]_ (var : typ → Set) : typ → Set where Val : {τ₁ : typ} → value[ var ] τ₁ → term[ var ] τ₁ App : {τ₁ τ₂ : typ} → (e₁ : term[ var ] (τ₂ ⇒ τ₁)) → (e₂ : term[ var ] τ₂) → term[ var ] τ₁ Value : typ → Set₁ Value τ₁ = (var : typ → Set) → value[ var ] τ₁ Term : typ → Set₁ Term τ₁ = (var : typ → Set) → term[ var ] τ₁ -- substitution relation mutual data SubstVal {var : typ → Set} : {τ τ₁ : typ} → (var τ → value[ var ] τ₁) → value[ var ] τ → value[ var ] τ₁ → Set where sVar= : {τ : typ} → {v : value[ var ] τ} → SubstVal (λ x → Var x) v v sVar≠ : {τ τ₁ : typ} → {x : var τ₁} → {v : value[ var ] τ} → SubstVal (λ y → Var x) v (Var x) sNum : {τ : typ} → {n : ℕ} → {v : value[ var ] τ} → SubstVal (λ y → Num n) v (Num n) sFun : {τ τ₁ τ₂ : typ} → {e₁ : var τ → var τ₂ → term[ var ] τ₁} → {v : value[ var ] τ} → {e₁′ : var τ₂ → term[ var ] τ₁} → ((x : var τ₂) → Subst (λ y → (e₁ y) x) v (e₁′ x)) → SubstVal (λ y → Fun (e₁ y)) v (Fun e₁′) data Subst {var : typ → Set} : {τ τ₁ : typ} → (var τ → term[ var ] τ₁) → value[ var ] τ → term[ var ] τ₁ → Set where sVal : {τ τ₁ : typ} → {v₁ : var τ → value[ var ] τ₁} → {v : value[ var ] τ} → {v₁′ : value[ var ] τ₁} → SubstVal v₁ v v₁′ → Subst (λ y → Val (v₁ y)) v (Val v₁′) sApp : {τ τ₁ τ₂ : typ} → {e₁ : var τ → term[ var ] (τ₂ ⇒ τ₁)} → {e₂ : var τ → term[ var ] τ₂} → {v : value[ var ] τ} → {e₁′ : term[ var ] (τ₂ ⇒ τ₁)} → {e₂′ : term[ var ] τ₂} → Subst e₁ v e₁′ → Subst e₂ v e₂′ → Subst (λ y → App (e₁ y) (e₂ y)) v (App e₁′ e₂′) -- frame data frame[_,_] (var : typ → Set) : typ → typ → Set where App₁ : {τ₁ τ₂ : typ} → (e₂ : term[ var ] τ₂) → frame[ var , τ₂ ⇒ τ₁ ] τ₁ App₂ : {τ₁ τ₂ : typ} → (v₁ : value[ var ] (τ₂ ⇒ τ₁)) → frame[ var , τ₂ ] τ₁ frame-plug : {var : typ → Set} → {τ₁ τ₂ : typ} → frame[ var , τ₂ ] τ₁ → term[ var ] τ₂ → term[ var ] τ₁ frame-plug (App₁ e₂) e₁ = App e₁ e₂ frame-plug (App₂ v₁) e₂ = App (Val v₁) e₂ -- reduction relation (= preservation) data Reduce {var : typ → Set} : {τ₁ : typ} → term[ var ] τ₁ → term[ var ] τ₁ → Set where RBeta : {τ₁ τ₂ : typ} → {e : var τ₂ → term[ var ] τ₁} → {v₂ : value[ var ] τ₂} → {e′ : term[ var ] τ₁} → Subst e v₂ e′ → Reduce (App (Val (Fun e)) (Val v₂)) e′ RFrame : {τ₁ τ₂ : typ} → {e : term[ var ] τ₁} → {e′ : term[ var ] τ₁} → (f : frame[ var , τ₁ ] τ₂) → Reduce e e′ → Reduce (frame-plug f e) (frame-plug f e′) data Reduce* {var : typ → Set} : {τ₁ : typ} → term[ var ] τ₁ → term[ var ] τ₁ → Set where R*Id : {τ₁ : typ} → (e : term[ var ] τ₁) → Reduce* e e R*Trans : {τ₁ : typ} → (e₁ : term[ var ] τ₁) → (e₂ : term[ var ] τ₁) → (e₃ : term[ var ] τ₁) → Reduce e₁ e₂ → Reduce* e₂ e₃ → Reduce* e₁ e₃ -- equational reasoning -- see ≡-Reasoning in Relation.Binary.PropositionalEquality.agda infix 3 _∎ infixr 2 _⟶⟨_⟩_ _⟶*⟨_⟩_ _≡⟨_⟩_ infix 1 begin_ begin_ : {var : typ → Set} → {τ : typ} → {e₁ e₂ : term[ var ] τ} → Reduce* e₁ e₂ → Reduce* e₁ e₂ begin_ red = red _⟶⟨_⟩_ : {var : typ → Set} → {τ : typ} → (e₁ {e₂ e₃} : term[ var ] τ) → Reduce e₁ e₂ → Reduce* e₂ e₃ → Reduce* e₁ e₃ _⟶⟨_⟩_ e₁ {e₂} {e₃} e₁-red-e₂ e₂-red*-e₃ = R*Trans e₁ e₂ e₃ e₁-red-e₂ e₂-red*-e₃ _⟶*⟨_⟩_ : {var : typ → Set} → {τ : typ} → (e₁ {e₂ e₃} : term[ var ] τ) → Reduce* e₁ e₂ → Reduce* e₂ e₃ → Reduce* e₁ e₃ _⟶*⟨_⟩_ e₁ {.e₁} {e₃} (R*Id .e₁) e₁-red*-e₃ = e₁-red*-e₃ _⟶*⟨_⟩_ e₁ {.e₂} {e₃} (R*Trans .e₁ e₁′ e₂ e₁-red-e₁′ e₁′-red*-e₂) e₂-red*-e₃ = R*Trans e₁ e₁′ e₃ e₁-red-e₁′ (e₁′ ⟶*⟨ e₁′-red*-e₂ ⟩ e₂-red*-e₃) _≡⟨_⟩_ : {var : typ → Set} → {τ : typ} → (e₁ {e₂ e₃} : term[ var ] τ) → e₁ ≡ e₂ → Reduce* e₂ e₃ → Reduce* e₁ e₃ _≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-red*-e₃ = e₂-red*-e₃ _∎ : {var : typ → Set} → {τ : typ} → (e : term[ var ] τ) → Reduce* e e _∎ e = R*Id e -- CPS transformation of types cpsT : typ → typ cpsT Nat = Nat cpsT (t₁ ⇒ t₂) = cpsT t₁ ⇒ (cpsT t₂ ⇒ Nat) ⇒ Nat -- CPS transformation (that produces no eta-redex) mutual cpsEtaV : {var : typ → Set} → {τ₁ : typ} → value[ var ∘ cpsT ] τ₁ → value[ var ] cpsT τ₁ cpsEtaV (Var x) = Var x cpsEtaV (Num n) = Num n cpsEtaV (Fun e₁) = Fun (λ x → Val (Fun (λ k → cpsEta′ (e₁ x) (Var k)))) cpsEta : {var : typ → Set} → {τ₁ : typ} → term[ var ∘ cpsT ] τ₁ → (value[ var ] (cpsT τ₁) → term[ var ] Nat) → term[ var ] Nat cpsEta (Val v) k = k (cpsEtaV v) cpsEta (App e₁ e₂) k = cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ → App (App (Val v₁) (Val v₂)) (Val (Fun (λ v → k (Var v)))))) cpsEta′ : {var : typ → Set} → {τ₁ : typ} → term[ var ∘ cpsT ] τ₁ → value[ var ] (cpsT τ₁ ⇒ Nat) → term[ var ] Nat cpsEta′ (Val v) k = App (Val k) (Val (cpsEtaV v)) cpsEta′ (App e₁ e₂) k = cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ → App (App (Val v₁) (Val v₂)) (Val k))) -- schematic schematic : {var : typ → Set} → {τ : typ} → (k : value[ var ] cpsT τ → term[ var ] Nat) → Set schematic {var} {τ} k = (v : value[ var ] cpsT τ) → Subst (λ y → k (Var y)) v (k v) -- disappears afterward schematic′ : {var : typ → Set} → {τ₁ τ₂ : typ} → (k : value[ var ] τ₂ → value[ var ] cpsT τ₁ → term[ var ] Nat) → Set schematic′ {var} {τ₁} {τ₂} k = {v : value[ var ] τ₂} → (x : value[ var ] cpsT τ₁) → Subst (λ y → k (Var y) x) v (k v x) -- disappears afterward cont-equal : {var : typ → Set} → {τ₁ τ₂ : typ} → (k₁ : var (cpsT τ₂) → value[ var ] cpsT τ₁ → term[ var ] Nat) → (v : value[ var ∘ cpsT ] τ₂) → (k₂ : value[ var ] cpsT τ₁ → term[ var ] Nat) → Set cont-equal {var} {τ₁} {τ₂} k₁ v k₂ = {v₁ : var (cpsT τ₂) → value[ var ] (cpsT τ₁)} → {v₁′ : value[ var ] (cpsT τ₁)} → SubstVal v₁ (cpsEtaV v) v₁′ → Subst (λ y → (k₁ y) (v₁ y)) (cpsEtaV v) (k₂ v₁′) mutual SubstV≠ : {var : typ → Set} → {τ₁ τ₂ : typ} → {t : value[ var ] τ₁} → {v : value[ var ] τ₂} → SubstVal (λ y → t) v t SubstV≠ {t = Var x} = sVar≠ SubstV≠ {t = Num n} = sNum SubstV≠ {t = Fun e₁} = sFun (λ x → Subst≠) Subst≠ : {var : typ → Set} → {τ₁ τ₂ : typ} → {t : term[ var ] τ₁} → {v : value[ var ] τ₂} → Subst (λ y → t) v t Subst≠ {t = Val x} = sVal SubstV≠ Subst≠ {t = App e₁ e₂} = sApp Subst≠ Subst≠ mutual eSubstV : {var : typ → Set} → {τ₁ τ₂ : typ} → {v₁ : var (cpsT τ₂) → value[ var ∘ cpsT ] τ₁} → {v₁′ : value[ var ∘ cpsT ] τ₁} → {v : value[ var ∘ cpsT ] τ₂} → SubstVal v₁ v v₁′ → SubstVal (λ y → cpsEtaV {var} (v₁ y)) (cpsEtaV v) (cpsEtaV v₁′) eSubstV sVar= = sVar= eSubstV sVar≠ = sVar≠ eSubstV sNum = sNum eSubstV (sFun s) = sFun (λ x → sVal (sFun (λ k → eSubst′ k (s x)))) eSubst : {var : typ → Set} → {τ₁ τ₂ : typ} → {e : var (cpsT τ₂) → term[ var ∘ cpsT ] τ₁} → {e′ : term[ var ∘ cpsT ] τ₁} → {v₁ : value[ var ∘ cpsT ] τ₂} → Subst e v₁ e′ → {k₁ : var (cpsT τ₂) → value[ var ] (cpsT τ₁) → term[ var ] Nat} → {k₂ : value[ var ] (cpsT τ₁) → term[ var ] Nat} → cont-equal k₁ v₁ k₂ → Subst (λ y → cpsEta {var} (e y) (k₁ y)) (cpsEtaV v₁) (cpsEta e′ k₂) eSubst (sVal s) eq = eq (eSubstV s) eSubst (sApp s₁ s₂) eq = eSubst s₁ (λ sub₁ → eSubst s₂ (λ sub₂ → sApp (sApp (sVal sub₁) (sVal sub₂)) (sVal (sFun (λ k → eq sVar≠))))) eSubst′ : {var : typ → Set} → {τ₁ τ₂ : typ} → {e : var (cpsT τ₂) → term[ var ∘ cpsT ] τ₁} → {e′ : term[ var ∘ cpsT ] τ₁} → {v : value[ var ∘ cpsT ] τ₂} → (k : var (cpsT τ₁ ⇒ Nat)) → Subst e v e′ → Subst (λ y → cpsEta′ {var} (e y) (Var k)) (cpsEtaV v) (cpsEta′ e′ (Var k)) eSubst′ k (sVal s) = sApp (sVal sVar≠) (sVal (eSubstV s)) eSubst′ k (sApp s₁ s₂) = eSubst s₁ (λ sub₁ → eSubst s₂ (λ sub₂ → sApp (sApp (sVal sub₁) (sVal sub₂)) (sVal sVar≠))) mutual kSubst : {var : typ → Set} → {τ₁ τ₂ : typ} → (e : term[ var ∘ cpsT ] τ₁) → {v : value[ var ] τ₂} → (k : value[ var ] τ₂ → value[ var ] cpsT τ₁ → term[ var ] Nat) → schematic′ k → Subst (λ y → cpsEta e (k (Var y))) v (cpsEta e (k v)) kSubst (Val v) k sch-k = sch-k (cpsEtaV v) kSubst (App e₁ e₂) k sch-k = kSubst e₁ (λ v′ v₁ → cpsEta e₂ (λ v₂ → App (App (Val v₁) (Val v₂)) (Val (Fun (λ v → k v′ (Var v)))))) (λ v₁ → kSubst e₂ (λ v′ v₂ → App (App (Val v₁) (Val v₂)) (Val (Fun (λ v → k v′ (Var v))))) (λ v₂ → sApp Subst≠ (sVal (sFun (λ k′ → sch-k (Var k′)))))) kSubst′ : {var : typ → Set} → {τ : typ} → (e : term[ var ∘ cpsT ] τ) → {v : value[ var ] (cpsT τ ⇒ Nat)} → Subst (λ k₁ → cpsEta′ e (Var k₁)) v (cpsEta′ e v) kSubst′ (Val x) = sApp (sVal sVar=) Subst≠ kSubst′ (App e₁ e₂) = kSubst e₁ (λ k v₁ → cpsEta e₂ (λ v₂ → App (App (Val v₁) (Val v₂)) (Val k))) (λ v₁ → kSubst e₂ (λ k v₂ → App (App (Val v₁) (Val v₂)) (Val k)) (λ v₂ → sApp Subst≠ (sVal sVar=))) -- the last 0 or 1 step in correctEta* cpsEtaEta′ : {var : typ → Set} → {τ : typ} → (e : term[ var ∘ cpsT ] τ) → (k : value[ var ] cpsT τ → term[ var ] Nat) → schematic k → Reduce* (cpsEta′ e (Fun (λ v → k (Var v)))) (cpsEta e k) cpsEtaEta′ (Val x) k sch-k = begin App (Val (Fun (λ v → k (Var v)))) (Val (cpsEtaV x)) ⟶⟨ RBeta (sch-k (cpsEtaV x)) ⟩ -- 1 step k (cpsEtaV x) ∎ cpsEtaEta′ (App e₁ e₂) k sch-k = begin cpsEta′ (App e₁ e₂) (Fun (λ v → k (Var v))) -- 0 step ∎ -- main correctEta : {var : typ → Set} → {τ : typ} → {e : term[ var ∘ cpsT ] τ} → {e′ : term[ var ∘ cpsT ] τ} → (k : value[ var ] cpsT τ → term[ var ] Nat) → Reduce e e′ → schematic k → Reduce* (cpsEta e k) (cpsEta e′ k) correctEta {e′ = e′} k (RBeta {e = e} {v₂} sub) sch-k = begin cpsEta (App (Val (Fun e)) (Val v₂)) k ≡⟨ refl ⟩ App (App (Val (Fun (λ x → Val (Fun (λ k′ → cpsEta′ (e x) (Var k′)))))) (Val (cpsEtaV v₂))) (Val (Fun (λ v → k (Var v)))) ⟶⟨ RFrame (App₁ (Val (Fun (λ v → k (Var v))))) (RBeta (sVal (sFun (λ k′ → eSubst′ k′ sub)))) ⟩ frame-plug (App₁ (Val (Fun (λ v → k (Var v))))) (Val (Fun (λ k′ → cpsEta′ e′ (Var k′)))) ≡⟨ refl ⟩ App (Val (Fun (λ k′ → cpsEta′ e′ (Var k′)))) (Val (Fun (λ v → k (Var v)))) ⟶⟨ RBeta (kSubst′ e′) ⟩ cpsEta′ e′ (Fun (λ v → k (Var v))) ⟶*⟨ cpsEtaEta′ e′ k sch-k ⟩ cpsEta e′ k ∎ correctEta k (RFrame {e = e} {e′} (App₁ e₂) red) sch-k = begin cpsEta (frame-plug (App₁ e₂) e) k ⟶*⟨ correctEta (λ v₁ → cpsEta e₂ (λ v₂ → App (App (Val v₁) (Val v₂)) (Val (Fun (λ v → k (Var v)))))) red (λ v → kSubst e₂ (λ y v₂ → App (App (Val y) (Val v₂)) (Val (Fun (λ v₁ → k (Var v₁))))) (λ v₂ → sApp (sApp (sVal sVar=) Subst≠) Subst≠)) ⟩ cpsEta (frame-plug (App₁ e₂) e′) k ∎ correctEta k (RFrame {e = e} {e′} (App₂ v₁) red) sch-k = begin cpsEta (frame-plug (App₂ v₁) e) k ⟶*⟨ correctEta (λ v₂ → App (App (Val (cpsEtaV v₁)) (Val v₂)) (Val (Fun (λ v → k (Var v))))) red (λ v → sApp (sApp (sVal SubstV≠) (sVal sVar=)) Subst≠) ⟩ cpsEta (frame-plug (App₂ v₁) e′) k ∎