From 17ecc55223e3fcdf7552fb03eeb1b7a28180e192 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 13 Dec 2023 20:53:33 +0100 Subject: [PATCH] Work on delay monad --- .../{Setoid.lagda.md => Setoids.lagda.md} | 15 ++- .../Monad/Instance/K/Instance/Delay.lagda.md | 8 +- .../Instance/Setoids/Delay/PreElgot.lagda.md | 127 ++++++++++++++++++ 3 files changed, 142 insertions(+), 8 deletions(-) rename agda/src/Category/Ambient/{Setoid.lagda.md => Setoids.lagda.md} (89%) create mode 100644 agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md diff --git a/agda/src/Category/Ambient/Setoid.lagda.md b/agda/src/Category/Ambient/Setoids.lagda.md similarity index 89% rename from agda/src/Category/Ambient/Setoid.lagda.md rename to agda/src/Category/Ambient/Setoids.lagda.md index ba3aa7e..4361cf8 100644 --- a/agda/src/Category/Ambient/Setoid.lagda.md +++ b/agda/src/Category/Ambient/Setoids.lagda.md @@ -26,14 +26,15 @@ open Eq using (_≡_) Most of the required properties are already proven in the agda-categories library, we are only left to construct the natural numbers object. ```agda -module Category.Ambient.Setoid {ℓ} where +module Category.Ambient.Setoids {ℓ} where -- equality on setoid functions - _≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ - _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g - ≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f - ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g} - ≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h - ≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h} + private + _≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ + _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g + ≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f + ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g} + ≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h + ≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h} -- we define ℕ ourselves, instead of importing it, to avoid lifting the universe lifting (builtin Nats are defined on Set₀) data ℕ : Set ℓ where diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md index 5eb2f51..5129f2c 100644 --- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md +++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md @@ -25,6 +25,8 @@ open Eq using (_≡_) open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax) open import Codata.Musical.Notation import Category.Monad.Partiality + +open import Category.Ambient.Setoids ``` --> @@ -105,6 +107,11 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now y ] now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A)) + -- slightly different types than later≈ + -- TODO remove this is useless + later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ] + later-cong {A} {x} {y} x≈y = later≈ (♯ x≈y) + now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ now x ≈ now y ] → A [ x ∼ y ] now-inj {A} {x} {y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b)) @@ -239,7 +246,6 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where identityʳ {A} {now x} {y} x≈y = x≈y identityʳ {A} {later x} {y} x≈y = x≈y - delayMonad : Monad (Setoids c (c ⊔ ℓ)) delayMonad = record { F = record diff --git a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md new file mode 100644 index 0000000..963d347 --- /dev/null +++ b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md @@ -0,0 +1,127 @@ + + +# The delay monad on the category of setoids is pre-Elgot + +```agda +module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where + open import Monad.Instance.K.Instance.Delay {ℓ} {ℓ} + open import Category.Ambient.Setoids + open import Algebra.Elgot (setoidAmbient {ℓ}) + open import Monad.PreElgot (setoidAmbient {ℓ}) + open Equality + + conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''} + {x : Setoid.Carrier X} {y : Setoid.Carrier Y } → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z + conflict X Y () + + + iter : ∀ {A X : Setoid ℓ ℓ} → (Setoid.Carrier X → (Delay (Setoid.Carrier A) ⊎ Setoid.Carrier X)) → Setoid.Carrier X → Delay (Setoid.Carrier A) + iter {A} {X} f x with f x + ... | inj₁ a = a + ... | inj₂ b = later (♯ (iter {A} {X} f b)) + + inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier Y} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → Y [ a ∼ b ] + inj₁-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₁ {x = a} {y = b} helper + where + helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₁ b ] + helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y + + inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → X [ a ∼ b ] + inj₂-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₂ {x = a} {y = b} helper + where + helper : (Y ⊎ₛ X) [ inj₂ a ∼ inj₂ b ] + helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y + + absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a : Setoid.Carrier Y} {b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A + absurd-helper {ℓ'} {X} {Y} {A} f {x} {y} {a} {b} x∼y fi₁ fi₂ = conflict Y X helper + where + helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₂ b ] + helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y + + iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (delaySetoid A ⊎ₛ X)) {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (f ._⟨$⟩_) y ] + iter-cong {A} {X} f {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy + ... | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy + ... | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy + ... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx + ... | inj₂ a | inj₂ b = later≈ (♯ iter-cong {A} {X} f (inj₂-helper f x∼y eqx eqy)) + + iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ] + iter-fixpoint {A} {X} {f} {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy + ... | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy + ... | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy + ... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx + ... | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy))))) + + iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ] + iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy + ... | inj₁ a | inj₁ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc + ... | inj₁ c = drop-inj₁ {x = a} {y = c} helper + where + helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] + helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y) + helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] + helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) + helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ] + helper rewrite (≡-sym eqc) = helper' + ... | inj₂ c = conflict (delaySetoid A) Y helper + where + helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] + helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y) + helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] + helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) + helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₂ c ] + helper rewrite (≡-sym eqc) = helper' + iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy + iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx + iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc -- = ≈-sym (later-eq (later≈ (♯ {! !}))) -- (iter-uni {A} {X} {Y} {f} {{! !}} {h} hf≈gh ((inj₂-helper f x∼y eqx eqy))) + ... | inj₁ c = {! !} -- absurd, probably... + ... | inj₂ c = later≈ (♯ {! !}) + -- why does this not terminate?? + -- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) + where + helper''' : (delaySetoid A ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ] + helper''' rewrite eqc = ∼-refl (delaySetoid A ⊎ₛ Y) + helper'' : (delaySetoid A ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ] + helper'' = ∼-sym (delaySetoid A ⊎ₛ Y) (hf≈gh x∼y) + helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ] + helper' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y) + helper : Y [ c ∼ h ⟨$⟩ a ] + helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (delaySetoid A ⊎ₛ Y) helper''' (∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper')) + help : A [ later (♯ iter {A} {Y} (g ._⟨$⟩_) (h ⟨$⟩ a)) ≈ later (♯ (iter {A} {Y} (g ._⟨$⟩_) c)) ] + help = later≈ (♯ iter-cong g (∼-sym Y helper)) + + delay-algebras : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A) + delay-algebras {A} = record + { _# = λ {X} f → record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = λ {x} {y} x∼y → iter-cong {A} {X} f {x} {y} x∼y } + ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f} + ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} + ; #-Folding = {! !} + ; #-resp-≈ = {! !} + } + where + iterr : ∀ {X : Setoid ℓ ℓ} → X ⟶ ((delaySetoid A) ⊎ₛ X) → X ⟶ (delaySetoid A) + iterr {X} f = record { _⟨$⟩_ = {! !} ; cong = {! !} } + + delayPreElgot : IsPreElgot delayMonad + delayPreElgot = record + { elgotalgebras = delay-algebras + ; extend-preserves = {! !} + } + + +```