Work on Delay Monad without musical notation

agda/src/Monad/Instance/K/Instance/D.lagda.md

@@ -0,0 +1,231 @@
+```agda 
+{-# OPTIONS --allow-unsolved-metas --guardedness #-}
+
+open import Level
+open import Function.Equality as SΠ renaming (id to idₛ)
+open import Relation.Binary
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_)
+open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
+
+
+module Monad.Instance.K.Instance.D {c ℓ} where
+
+open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
+open module eq (S : Setoid c (c ⊔ ℓ)) = IsEquivalence (Setoid.isEquivalence S) using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
+
+
+mutual
+
+  data Delay (A : Set c) : Set c where
+    now   : A        → Delay A
+    later : Delay′ A → Delay A
+
+  record Delay′ (A : Set c) : Set c where
+    coinductive
+    field
+      force : Delay A
+
+open Delay′ public
+
+module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
+
+  never : Delay ∣ A ∣
+  never′ : Delay′ ∣ A ∣
+
+  never = later never′
+  force never′ = never
+
+  -- Removes a later constructor, if possible.
+
+  drop-later : Delay ∣ A ∣ → Delay ∣ A ∣
+  drop-later (now   x) = now x
+  drop-later (later x) = force x
+
+  -- An unfolding lemma for Delay.
+
+  Delay↔ : Delay ∣ A ∣ ↔ (∣ A ∣ ⊎ Delay′ ∣ A ∣)
+  
+  Inverse.to Delay↔ ⟨$⟩ now x   = inj₁ x
+  Inverse.to Delay↔ ⟨$⟩ later x = inj₂ x
+  
+  Inverse.from Delay↔ ⟨$⟩ inj₁ x = now x
+  Inverse.from Delay↔ ⟨$⟩ inj₂ y = later y
+  
+  cong (Inverse.to Delay↔) Eq.refl   = Eq.refl
+  cong (Inverse.from Delay↔) Eq.refl = Eq.refl
+  
+  Inv._InverseOf_.left-inverse-of (Inverse.inverse-of Delay↔) (now _)   = Eq.refl
+  Inv._InverseOf_.left-inverse-of (Inverse.inverse-of Delay↔) (later _) = Eq.refl
+  Inv._InverseOf_.right-inverse-of (Inverse.inverse-of Delay↔) (inj₁ _) = Eq.refl
+  Inv._InverseOf_.right-inverse-of (Inverse.inverse-of Delay↔) (inj₂ _) = Eq.refl
+
+  mutual
+
+    -- adapted from https://www.cse.chalmers.se/∼nad/listings/delay-monad/Delay-monad.Bisimilarity.html
+    
+    data _∼_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where
+      now∼    : ∀ {x y} → [ A ][ x ≡ y ] → now x ∼ now y
+      later∼  : ∀ {x y} → force x ∼′ force y → later x ∼ later y
+
+    record _∼′_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where
+      coinductive
+      
+      field
+        force∼ : x ∼ y
+
+  open _∼′_ public
+
+  -- strong bisimilarity of now and later leads to a clash
+  now∼later : ∀ {ℓ'}{Z : Set ℓ'}{x : ∣ A ∣}{y : Delay′ ∣ A ∣} → now x ∼ later y → Z
+  now∼later ()
+
+  ∼-refl  : ∀ {x : Delay ∣ A ∣} → x ∼ x
+  ∼′-refl : ∀ {x : Delay ∣ A ∣} → x ∼′ x
+
+  ∼-refl {now x}   = now∼ (≡-refl A) 
+  ∼-refl {later x} = later∼ ∼′-refl
+
+  force∼ (∼′-refl {now x})   = now∼ (≡-refl A)
+  force∼ (∼′-refl {later x}) = later∼ ∼′-refl
+
+  ∼-sym  : ∀ {x y : Delay ∣ A ∣} → x ∼ y → y ∼ x
+  ∼′-sym : ∀ {x y : Delay ∣ A ∣} → x ∼′ y → y ∼′ x
+
+  ∼-sym (now∼ x≡y) = now∼ (≡-sym A x≡y)
+  ∼-sym (later∼ fx∼fy) = later∼ (∼′-sym fx∼fy)
+
+  force∼ (∼′-sym x∼′y) = ∼-sym (force∼ x∼′y)
+
+  ∼-trans  : ∀ {x y z : Delay ∣ A ∣} → x ∼ y → y ∼ z → x ∼ z
+  ∼′-trans : ∀ {x y z : Delay ∣ A ∣} → x ∼′ y → y ∼′ z → x ∼′ z
+
+  ∼-trans (now∼ x≡y) (now∼ y≡z) = now∼ (≡-trans A x≡y y≡z)
+  ∼-trans (later∼ x∼y) (later∼ y∼z) = later∼ (∼′-trans x∼y y∼z)
+
+  force∼ (∼′-trans x∼y y∼z) = ∼-trans (force∼ x∼y) (force∼ y∼z)
+
+  data _↓_ : Delay ∣ A ∣ → ∣ A ∣ → Set (c ⊔ ℓ) where
+    now↓   : ∀ {x y} → [ A ][ x ≡ y ] → now x ↓ y
+    later↓ : ∀ {x y} (x↓y : (force x) ↓ y) → later x ↓ y
+
+  unique↓ : ∀ {a : Delay ∣ A ∣ } {x y : ∣ A ∣} → a ↓ x → a ↓ y → [ A ][ x ≡ y ]
+  unique↓ (now↓ a≡x) (now↓ a≡y) = ≡-trans A (≡-sym A a≡x) a≡y
+  unique↓ (later↓ fb↓x) (later↓ fb↓y) = unique↓ fb↓x fb↓y
+
+  mutual
+  
+    data _≈_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where
+      ↓≈     : ∀ {x y a b} (a≡b : [ A ][ a ≡ b ]) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
+      later≈ : ∀ {x y} (x≈y : force x ≈′ force y) → later x ≈ later y
+
+    record _≈′_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where
+      coinductive
+      
+      field
+        force≈ : x ≈ y
+
+  open _≈′_ public
+
+  ≈→≈′ : ∀ {x y : Delay ∣ A ∣} → x ≈ y → x ≈′ y
+  force≈ (≈→≈′ x≈y) = x≈y
+
+  ≡↓ : ∀ {x y : ∣ A ∣} {z : Delay ∣ A ∣} → [ A ][ x ≡ y ] → z ↓ x → z ↓ y
+  ≡↓ {x} {y} {.(now _)} x≡y (now↓ a≡x) = now↓ (≡-trans A a≡x x≡y)
+  ≡↓ {x} {y} {.(later _)} x≡y (later↓ z↓x) = later↓ (≡↓ x≡y z↓x)
+
+  ≈↓  : ∀ {x y : Delay ∣ A ∣ } {a : ∣ A ∣} → x ≈ y → x ↓ a → y ↓ a
+
+  ≈↓ (↓≈ c≡b (now↓ x≡c) y↓b) (now↓ x≡a) = ≡↓ (≡-trans A (≡-trans A (≡-sym A c≡b) (≡-sym A x≡c)) x≡a) y↓b
+  ≈↓ (↓≈ c≡b (later↓ x↓c) y↓b) (later↓ x↓a) = ≡↓ (≡-trans A (≡-sym A c≡b) (≡-sym A (unique↓ x↓a x↓c))) y↓b
+  ≈↓ (later≈ fx≈fy) (later↓ fx↓a) = later↓ (≈↓ (force≈ fx≈fy) fx↓a)
+
+
+  ≈-refl  : ∀ {x : Delay ∣ A ∣} → x ≈ x
+  ≈′-refl : ∀ {x : Delay ∣ A ∣} → x ≈′ x
+
+  ≈-refl {now x}   = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (now↓ (≡-refl A))
+  ≈-refl {later x} = later≈ ≈′-refl
+
+  force≈ ≈′-refl = ≈-refl
+
+
+  ≈-sym  : ∀ {x y : Delay ∣ A ∣} → x ≈ y → y ≈ x
+  ≈′-sym : ∀ {x y : Delay ∣ A ∣} → x ≈′ y → y ≈′ x
+
+  ≈-sym (↓≈ a≡b x↓a y↓b) = ↓≈ (≡-sym A a≡b) y↓b x↓a
+  ≈-sym (later≈ x≈y) = later≈ (≈′-sym x≈y)
+
+  force≈ (≈′-sym x∼′y) = ≈-sym (force≈ x∼′y)
+
+
+  ≈-trans  : ∀ {x y z : Delay ∣ A ∣} → x ≈ y → y ≈ z → x ≈ z
+  ≈′-trans : ∀ {x y z : Delay ∣ A ∣} → x ≈′ y → y ≈′ z → x ≈′ z
+
+  ≈-trans (↓≈ a≡b x↓a y↓b) (↓≈ c≡d y↓c z↓d) = ↓≈ (≡-trans A (≡-trans A a≡b (unique↓ y↓b y↓c)) c≡d) x↓a z↓d
+  ≈-trans (↓≈ a≡b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a≡b z↓a (later↓ (≈↓ (force≈ x≈y) x↓b))
+  ≈-trans (later≈ x≈y) (↓≈ a≡b (later↓ y↓a) z↓b) = ↓≈ a≡b (later↓ (≈↓ (≈-sym (force≈ x≈y)) y↓a)) z↓b
+  ≈-trans (later≈ x≈y) (later≈ y≈z) = later≈ (≈′-trans x≈y y≈z) 
+
+  force≈ (≈′-trans x≈′y y≈′z) = ≈-trans (force≈ x≈′y) (force≈ y≈′z)
+
+open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
+
+
+module DelayMonad where
+  Delayₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
+  Delayₛ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
+  <_> = Π._⟨$⟩_
+
+  ∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ A ][ x ≈ y ]
+  ∼′⇒≈′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼′ y ] → [ A ][ x ≈′ y ]
+  ∼⇒≈ {A} {.(now _)} {.(now _)} (now∼ a≡b) = ↓≈ a≡b (now↓ (≡-refl A)) (now↓ (≡-refl A))
+  ∼⇒≈ {A} {.(later _)} {.(later _)} (later∼ x∼y) = later≈ (∼′⇒≈′ x∼y)
+  force≈ (∼′⇒≈′ {A} {x} {y} x∼y) = ∼⇒≈ (force∼ x∼y)
+
+  liftF : ∀ {A B : Set c} → (A → B) → Delay A → Delay B
+  liftF′ : ∀ {A B : Set c} → (A → B) → Delay′ A → Delay′ B
+  liftF f (now x) = now (f x)
+  liftF f (later x) = later (liftF′ f x)
+  force (liftF′ f x) = liftF f (force x)
+
+  lift↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay ∣ A ∣} {b : ∣ A ∣} → [ A ][ x ↓ b ] → [ B ][ (liftF (< f >) x) ↓ (f ⟨$⟩ b) ]
+  lift↓ {A} {B} f {now x} {b} (now↓ x≡a) = now↓ (cong f x≡a)
+  lift↓ {A} {B} f {later x} {b} (later↓ x↓b) = later↓ (lift↓ f x↓b)
+
+
+  lift-cong : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [ B ][ liftF < f > x ≈ liftF < f > y ]
+  lift-cong′ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ B ][ liftF < f > x ≈′ liftF < f > y ]
+  lift-cong {A} {B} f {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = ↓≈ (cong f a≡b) (now↓ (cong f x≡a)) (now↓ (cong f y≡b))
+  lift-cong {A} {B} f {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (cong f a≡b) (now↓ (cong f x≡a)) (later↓ (lift↓ f y↓b))
+  lift-cong {A} {B} f {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ (cong f a≡b) (later↓ (lift↓ f x↓a)) (now↓ (cong f y≡b))
+  lift-cong {A} {B} f {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (lift-cong′ f (≈→≈′ A (↓≈ a≡b x↓a y↓b)))
+  lift-cong {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (lift-cong′ {A} {B} f x≈y)
+  force≈ (lift-cong′ {A} {B} f {x} {y} x≈y) = lift-cong f (force≈ x≈y)
+
+  liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ A ⟶ Delayₛ B
+  liftFₛ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = lift-cong f }
+
+  now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ now x ≈ now y ]
+  now-cong {A} {x} {y} x≡y = ↓≈ x≡y (now↓ (≡-refl A)) (now↓ (≡-refl A))
+
+  η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delayₛ A
+  η A = record { _⟨$⟩_ = now ; cong = now-cong }
+
+  now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ 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))
+
+  -- this needs polymorphic universe levels
+  _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ')
+  _≋_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
+
+  -- later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay′ ∣ A ∣} {y : Delay ∣ A ∣} → [ A ][ later x ≈ y ] → [ A ][ force x ≈ y ] 
+  -- later-eq′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay′ ∣ A ∣} {y : Delay ∣ A ∣} → [ A ][ later x ≈′ y ] → [ A ][ force x ≈′ y ] 
+  -- force≈ (later-eq′ {A} {x} {y} x≈y) = later-eq (force≈ x≈y)
+  -- later-eq {A} {x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b x↓a (now↓ y≡b)
+  -- later-eq {A} {x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = ↓≈ a≡b x↓a (later↓ y↓b)
+  -- later-eq {A} {x} {later y} (later≈ x≈y) with force x
+  -- ...                                     | now a = {!   !}
+  -- ...                                     | later a = later≈ (later-eq′ x≈y)
+```