[Found a way to rewrite the evaluator in "accumulator" style. Nils Anders Danielsson **20101211171210 Ignore-this: d3a1baca37d2adf1a348de7ccfa6f75a ] hunk ./CompositionBased/Lambda.agda 21 - hiding (module Derivation) + hiding (module Derivation; app) hunk ./CompositionBased/Lambda.agda 177 +-- TODO: Is accumulator really the right term? + hunk ./CompositionBased/Lambda.agda 185 + open MoreLaws∥ + + -- We need to decide what kind of accumulator/composition to use. ƛ + -- is complicated: in order to make use of the inductive hypothesis + -- we need to ensure that + -- + -- f ◌ (λ ρ v → ⟦ t ⟧S (v , ρ)) + -- + -- (for some notion of accumulator f and composition _◌_) can be + -- rewritten as + -- + -- f′ (f″ ◌ ⟦ t ⟧S) + -- + -- for some f′ and f″. Note that the environment changes above. For + -- this reason I've found it useful if the accumulator + -- (continuation?) gets direct access to the environment, as in + -- + -- ⟦ t ⟧′ κ = λ ρ → κ ⟦ t ⟧ ρ = κ ⟦ t ⟧. + -- + -- With this specification of ⟦_⟧′ we get the following result: + -- + -- ⟦ t₁ · t₂ ⟧′ κ = + -- κ (λ ρ → (⟦ t₁ ⟧ ρ) (⟦ t₂ ⟧ ρ)) = + -- ⟦ t₁ ⟧′ (λ f → ⟦ t₂ ⟧′ (λ g → κ (λ ρ → (f ρ) (g ρ)))) + -- + -- Note that ⟦ t₂ ⟧′ occurs under a lambda. I want to incorporate + -- this lambda in the definition of composition, so I'm defining + -- composition as follows: + + infixr 9 _◌_ + + _◌_ : ∀ {As} {A B : Set} → A → As ⇨ (A → B) → As ⇨ B + x ◌ f = RC.map (λ g → g x) f + + -- With As = [] we get reverse application, and with As = C ∷ [] we + -- get (roughly) x ◌ f = λ v → f v x. + + -- TODO: As seems to stay constant in the computations below, so I + -- think I've made some kind of mistake. + + -- A lemma related to _◌_. + + ◌-cong : ∀ {As A B} (x : A) {f₁ f₂ : As ⇨ (A → B)} → + f₁ ≈ f₂ → x ◌ f₁ ≈ x ◌ f₂ + ◌-cong x f₁≈f₂ = map-cong (λ g → P.refl {x = g x}) f₁≈f₂ hunk ./CompositionBased/Lambda.agda 233 - top : ∀ {Γ σ τ} → Dom (σ ∷ Γ) (σ ⟶ τ) → Dom (σ ∷ Γ) τ - top f = Λ λ v → RC.map (λ g → g v) (f ∙ v) + -- TODO: Simplify things? The moral code for top is + -- + -- top κ = λ ρ → κ ρ (λ (v , ρ) → v). + + top : ∀ {Γ σ As B} → As ⇨ (Dom (σ ∷ Γ) σ → B) → As ⇨ B + top = RC.map (λ f → f (Λ λ v → return∥ v)) hunk ./CompositionBased/Lambda.agda 240 - drop : ∀ {Γ σ τ χ} → - (Dom Γ σ → Dom Γ τ) → (Dom (χ ∷ Γ) σ → Dom (χ ∷ Γ) τ) - drop g f = Λ λ v → g (f ∙ v) + drop : ∀ {Γ σ τ As} {B : Set} → + As ⇨ (Dom (σ ∷ Γ) τ → B) → As ⇨ (Dom Γ τ → B) + drop = RC.map (λ f g → f (Λ λ _ → g)) + + drop-lemma : ∀ {Γ σ τ As B} + (f : Dom Γ τ) (κ : As ⇨ (Dom (σ ∷ Γ) τ → B)) → + C.drop f ◌ κ ≈ f ◌ drop κ + drop-lemma {B = B} f κ = + C.drop f ◌ κ ≡⟨ P.refl ⟩ + RC.map (λ g → g (Λ λ _ → f)) κ ≈⟨ sym $ map-∘ (λ (g : _ → B) → g f) (λ f g → f (Λ (λ _ → g))) κ ⟩ + RC.map (λ (g : _ → B) → g f) (RC.map (λ f g → f (Λ λ _ → g)) κ) ≡⟨ P.refl ⟩ + f ◌ drop κ ∎ hunk ./CompositionBased/Lambda.agda 255 - lookup : ∀ {Γ σ τ} → Γ ∋ σ → Dom Γ (σ ⟶ τ) → Dom Γ τ + lookup : ∀ {Γ σ As B} → Γ ∋ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B hunk ./CompositionBased/Lambda.agda 258 - lookup′ : ∀ {Γ σ τ} (x : Γ ∋ σ) (f : Dom Γ (σ ⟶ τ)) → - EqualTo (f ⊛∥ C.lookup x) - lookup′ (zero {Γ = Γ}) f = ▷ - f ⊛∥ C.lookup (zero {Γ = Γ}) ≡⟨ P.refl ⟩ - f ⊛∥ C.top ≡⟨ P.refl ⟩ - Λ (λ v → f ∙ v) ⊛∥ (Λ λ v → return∥ v) ≡⟨ P.refl ⟩ - Λ (λ v → f ∙ v ⊛∥ return∥ v) ≈⟨ Λ-cong (λ v → MoreLaws∥.⊛∥-return∥ (f ∙ v) v) ⟩ - Λ (λ v → RC.map (λ g → g v) (f ∙ v)) ≡⟨ P.refl ⟩ - top f ∎ - - lookup′ (suc {τ = τ} x) f = ▷ - f ⊛∥ C.lookup (suc x) ≡⟨ P.refl ⟩ - f ⊛∥ C.drop (C.lookup x) ≡⟨ P.refl ⟩ - f ⊛∥ (Λ λ _ → C.lookup x) ≡⟨ P.refl ⟩ - (Λ λ v → f ∙ v ⊛∥ C.lookup x) ≈⟨ Λ-cong (λ v → proof (lookup′ x (f ∙ v))) ⟩ - (Λ λ v → lookup x (f ∙ v)) ≡⟨ P.refl ⟩ - drop (lookup x) f ∎ + lookup′ : ∀ {Γ σ As B} (x : Γ ∋ σ) (κ : As ⇨ (Dom Γ σ → B)) → + EqualTo (C.lookup x ◌ κ) + lookup′ zero κ = ▷ + C.lookup zero ◌ κ ≡⟨ P.refl ⟩ + C.top ◌ κ ≡⟨ P.refl ⟩ + top κ ∎ hunk ./CompositionBased/Lambda.agda 265 - -- Note that defunctionalisation of the last case above leads to - -- tree-structured code. + lookup′ (suc x) κ = ▷ + C.lookup (suc x) ◌ κ ≡⟨ P.refl ⟩ + C.drop (C.lookup x) ◌ κ ≈⟨ drop-lemma (C.lookup x) κ ⟩ + C.lookup x ◌ drop κ ≈⟨ proof (lookup′ x _) ⟩ + lookup x (drop κ) ∎ hunk ./CompositionBased/Lambda.agda 273 + app : ∀ {Γ σ τ As B} → + As ⇨ (Dom Γ τ → B) → As ⇨ (Dom Γ σ → Dom Γ (σ ⟶ τ) → B) + app = RC.map (λ κ x f → κ (f ⊛∥ x)) + + app-lemma : ∀ {Γ σ τ As B} + (f : Dom Γ (σ ⟶ τ)) (g : Dom Γ σ) + (κ : As ⇨ (Dom Γ τ → B)) → + (f ⊛∥ g) ◌ κ ≈ f ◌ g ◌ app κ + app-lemma {B = B} f g κ = + (f ⊛∥ g) ◌ κ ≡⟨ P.refl ⟩ + RC.map (λ h → h (f ⊛∥ g)) κ ≈⟨ sym $ map-∘ (λ (h : _ → B) → h f) (λ κ f → κ (f ⊛∥ g)) κ ⟩ + RC.map (λ (h : _ → B) → h f) + (RC.map (λ κ f → κ (f ⊛∥ g)) κ) ≡⟨ P.refl ⟩ + f ◌ RC.map (λ κ f → κ (f ⊛∥ g)) κ ≈⟨ sym $ ◌-cong f $ map-∘ (λ (h : _ → _ → B) → h g) (λ κ x f → κ (f ⊛∥ x)) κ ⟩ + f ◌ RC.map (λ (h : _ → _ → B) → h g) + (RC.map (λ κ x f → κ (f ⊛∥ x)) κ) ≡⟨ P.refl ⟩ + f ◌ g ◌ app κ ∎ + + push : ∀ {Γ σ τ As B} → + As ⇨ (Dom Γ (σ ⟶ τ) → B) → As ⇨ (Dom (σ ∷ Γ) τ → B) + push = RC.map (λ κ f → κ (C.push f)) + + push-lemma : ∀ {Γ σ τ As B} + (f : Dom (σ ∷ Γ) τ) (κ : As ⇨ (Dom Γ (σ ⟶ τ) → B)) → + C.push f ◌ κ ≈ f ◌ push κ + push-lemma {B = B} f κ = + C.push f ◌ κ ≡⟨ P.refl ⟩ + RC.map (λ g → g (C.push f)) κ ≈⟨ sym $ map-∘ (λ (g : _ → B) → g f) (λ κ f → κ (C.push f)) κ ⟩ + RC.map (λ (g : _ → B) → g f) (RC.map (λ κ f → κ (C.push f)) κ) ≡⟨ P.refl ⟩ + f ◌ push κ ∎ + hunk ./CompositionBased/Lambda.agda 306 - ⟦_⟧ : ∀ {Γ σ τ} → Γ ⊢ σ → Dom Γ (σ ⟶ τ) → Dom Γ τ + ⟦_⟧ : ∀ {Γ σ As B} → Γ ⊢ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B hunk ./CompositionBased/Lambda.agda 309 - ⟦_⟧′ : ∀ {Γ σ τ} (t : Γ ⊢ σ) (f : Dom Γ (σ ⟶ τ)) → - EqualTo (f ⊛∥ ⟦ t ⟧C) - ⟦ var x ⟧′ f = ▷ - f ⊛∥ ⟦ var x ⟧C ≡⟨ P.refl ⟩ - f ⊛∥ C.lookup x ≈⟨ proof (lookup′ x f) ⟩ - lookup x f ∎ - - ⟦ t₁ · t₂ ⟧′ f = ▷ - f ⊛∥ ⟦ t₁ · t₂ ⟧C ≡⟨ P.refl ⟩ - f ⊛∥ (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ≈⟨ sym $ composition _ _ _ ⟩ - RC.map _∘′_ f ⊛∥ ⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C ≈⟨ proof (⟦ t₁ ⟧′ _) ⊛∥-cong refl _ ⟩ - ⟦ t₁ ⟧ (RC.map _∘′_ f) ⊛∥ ⟦ t₂ ⟧C ≈⟨ proof (⟦ t₂ ⟧′ _) ⟩ - ⟦ t₂ ⟧ (⟦ t₁ ⟧ (RC.map _∘′_ f)) ∎ - where open MoreLaws∥ + ⟦_⟧′ : ∀ {Γ σ As B} (t : Γ ⊢ σ) (κ : As ⇨ (Dom Γ σ → B)) → + EqualTo (⟦ t ⟧C ◌ κ) + ⟦ var x ⟧′ κ = ▷ + ⟦ var x ⟧C ◌ κ ≡⟨ P.refl ⟩ + C.lookup x ◌ κ ≈⟨ proof (lookup′ x κ) ⟩ + lookup x κ ∎ hunk ./CompositionBased/Lambda.agda 316 - ⟦_⟧′ {Γ = Γ} (ƛ t) f = ▷ - f ⊛∥ ⟦ ƛ t ⟧C ≡⟨ P.refl ⟩ - f ⊛∥ C.push ⟦ t ⟧C ≈⟨ ⊛∥-curry-uncurry f (C.push ⟦ t ⟧C) ⟩ - RC.curry (λ ρ → - RC.uncurry f ρ (RC.uncurry (C.push ⟦ t ⟧C) ρ)) ≡⟨ P.refl ⟩ - RC.curry (λ ρ → - RC.uncurry f ρ (RC.uncurry (RC.curry {As = Values Γ} - (λ ρ v → RC.uncurry ⟦ t ⟧C (v , ρ))) ρ)) ≈⟨ curry-cong (λ ρ → P.cong (RC.uncurry f ρ) $ - uncurry∘curry (Values Γ) _ ρ) ⟩ - RC.curry (λ ρ → RC.uncurry f ρ (λ v → RC.uncurry ⟦ t ⟧C (v , ρ))) ≈⟨ {!!} ⟩ - {!!} ∎ - where - open MoreLaws∥ - open CurryLaws + ⟦ t₁ · t₂ ⟧′ κ = ▷ + ⟦ t₁ · t₂ ⟧C ◌ κ ≡⟨ P.refl ⟩ + (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ◌ κ ≈⟨ app-lemma ⟦ t₁ ⟧C ⟦ t₂ ⟧C κ ⟩ + ⟦ t₁ ⟧C ◌ ⟦ t₂ ⟧C ◌ app κ ≈⟨ ◌-cong ⟦ t₁ ⟧C (proof (⟦ t₂ ⟧′ _)) ⟩ + ⟦ t₁ ⟧C ◌ ⟦ t₂ ⟧ (app κ) ≈⟨ proof (⟦ t₁ ⟧′ _) ⟩ + ⟦ t₁ ⟧ (⟦ t₂ ⟧ (app κ)) ∎ hunk ./CompositionBased/Lambda.agda 323 - -- My goal is to find f′ and ρ′ which solve the following - -- equation: - -- - -- f ρ (λ v → g (v , ρ)) ≈ f′ ρ′ (g ρ′) - -- - -- In that case I can apply the inductive hypothesis to ⟦ t ⟧C. - -- However, this equation does not seem to have a solution. + ⟦ ƛ t ⟧′ κ = ▷ + ⟦ ƛ t ⟧C ◌ κ ≡⟨ P.refl ⟩ + C.push ⟦ t ⟧C ◌ κ ≈⟨ push-lemma ⟦ t ⟧C κ ⟩ + ⟦ t ⟧C ◌ push κ ≈⟨ proof (⟦ t ⟧′ _) ⟩ + ⟦ t ⟧ (push κ) ∎ hunk ./CompositionBased/Lambda.agda 329 - halt : ∀ {Γ σ} → Dom Γ (σ ⟶ σ) - halt = return∥ id + halt : ∀ {Γ σ} → [] ⇨ (Dom Γ σ → Dom Γ σ) + halt = return id hunk ./CompositionBased/Lambda.agda 333 - ∃ λ f → RC.curry {As = Values Γ} ⟦ t ⟧S ≈ ⟦ t ⟧ f + ∃ λ κ → RC.curry {As = Values Γ} ⟦ t ⟧S ≈ run (⟦ t ⟧ κ) hunk ./CompositionBased/Lambda.agda 335 - RC.curry ⟦ t ⟧S ≈⟨ proof $ Compositional.⟦_⟧′ t ⟩ - ⟦ t ⟧C ≈⟨ sym $ identity-⊛∥ ⟦ t ⟧C ⟩ - halt ⊛∥ ⟦ t ⟧C ≈⟨ proof $ ⟦ t ⟧′ (halt) ⟩ - ⟦ t ⟧ (halt) ∎) - where open MoreLaws∥ + RC.curry ⟦ t ⟧S ≈⟨ proof $ Compositional.⟦_⟧′ t ⟩ + ⟦ t ⟧C ≡⟨ P.refl ⟩ + run (⟦ t ⟧C ◌ halt) ≡⟨ run-cong $ proof $ ⟦ t ⟧′ halt ⟩ + run (⟦ t ⟧ halt) ∎) + + -- lookup and ⟦_⟧ preserve equality of the accumulator. + + top-cong : ∀ {Γ σ As B} {κ₁ κ₂ : As ⇨ (Dom (σ ∷ Γ) σ → B)} → + κ₁ ≈ κ₂ → top κ₁ ≈ top κ₂ + top-cong = map-cong (λ f → P.refl {x = f (Λ λ v → return∥ v)}) + + drop-cong : ∀ {Γ σ τ As B} {κ₁ κ₂ : As ⇨ (Dom (σ ∷ Γ) τ → B)} → + κ₁ ≈ κ₂ → drop κ₁ ≈ drop κ₂ + drop-cong = map-cong (λ f → P.refl {x = λ g → f (Λ λ _ → g)}) + + app-cong : ∀ {Γ σ τ As B} {κ₁ κ₂ : As ⇨ (Dom Γ τ → B)} → + κ₁ ≈ κ₂ → app {σ = σ} κ₁ ≈ app {σ = σ} κ₂ + app-cong = map-cong (λ κ → P.refl {x = λ x f → κ (f ⊛∥ x)}) + + push-cong : ∀ {Γ σ τ As B} {κ₁ κ₂ : As ⇨ (Dom Γ (σ ⟶ τ) → B)} → + κ₁ ≈ κ₂ → push κ₁ ≈ push κ₂ + push-cong = map-cong (λ κ → P.refl {x = λ f → κ (C.push f)}) + + lookup-cong : ∀ {Γ σ As B} (x : Γ ∋ σ) {κ₁ κ₂ : As ⇨ (Dom Γ σ → B)} → + κ₁ ≈ κ₂ → lookup x κ₁ ≈ lookup x κ₂ + lookup-cong zero = top-cong + lookup-cong (suc x) = lookup-cong x ∘ drop-cong + + ⟦_⟧-cong : ∀ {Γ σ As B} (t : Γ ⊢ σ) {κ₁ κ₂ : As ⇨ (Dom Γ σ → B)} → + κ₁ ≈ κ₂ → ⟦ t ⟧ κ₁ ≈ ⟦ t ⟧ κ₂ + ⟦ var x ⟧-cong = lookup-cong x + ⟦ t₁ · t₂ ⟧-cong = ⟦ t₁ ⟧-cong ∘ ⟦ t₂ ⟧-cong ∘ app-cong + ⟦ ƛ t ⟧-cong = ⟦ t ⟧-cong ∘ push-cong + + -- As an aside, note that the right-hand sides of lookup and ⟦_⟧ can + -- be written as compositions: + + private + + lookup″ : ∀ {Γ σ As B} → Γ ∋ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B + lookup″ zero = top + lookup″ (suc x) = lookup″ x ∘ drop + + ⟦_⟧″ : ∀ {Γ σ As B} → Γ ⊢ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B + ⟦ var x ⟧″ = lookup″ x + ⟦ t₁ · t₂ ⟧″ = ⟦ t₁ ⟧″ ∘ ⟦ t₂ ⟧″ ∘ app + ⟦ ƛ t ⟧″ = ⟦ t ⟧″ ∘ push