------------------------------------------------------------------------
-- The Agda standard library
--
-- The partiality monad
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe --guardedness #-}
module Effect.Monad.Partiality where
open import Codata.Musical.Notation using (∞; ♯_; ♭)
open import Data.Bool.Base using (Bool; false; true)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product as Prod using (∃; ∄; -,_; ∃₂; _,_; _×_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Function.Base using (_∘′_; flip; id; _∘_; _$_; _⟨_⟩_)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core as B hiding (Rel; _⇔_)
open import Relation.Binary.Definitions
using (DecidableEquality; Reflexive; Symmetric; Transitive)
open import Relation.Binary.Structures
using (IsPreorder; IsEquivalence)
open import Relation.Binary.Bundles
using (Preorder; Setoid; Poset)
import Relation.Binary.Properties.Setoid as SetoidProperties
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as ≡
open import Relation.Nullary.Decidable using (yes; no; False; Dec; ¬¬-excluded-middle)
open import Relation.Nullary.Negation using (¬_; ¬¬-Monad)
private
variable
a b c f s ℓ : Level
A : Set a
B : Set b
C : Set c
------------------------------------------------------------------------
-- The partiality monad
data _⊥ (A : Set a) : Set a where
now : (x : A) → A ⊥
later : (x : ∞ (A ⊥)) → A ⊥
bind : A ⊥ → (A → B ⊥) → B ⊥
bind (now x) f = f x
bind (later x) f = later (♯ (bind (♭ x) f))
functor : RawFunctor {ℓ} _⊥
functor = record { _<$>_ = map } where
map : (A → B) → A ⊥ → B ⊥
map f (now a) = now (f a)
map f (later d) = later (♯ map f (♭ d))
applicative : RawApplicative {f = f} _⊥
applicative = record
{ rawFunctor = functor
; pure = now
; _<*>_ = λ mf mx → bind mf (λ f → bind mx (now ∘′ f))
}
monad : RawMonad {f = f} _⊥
monad = record
{ rawApplicative = applicative
; _>>=_ = bind
}
join : (A ⊥) ⊥ → A ⊥
join = Join.join monad
private module M {f} = RawMonad (monad {f})
-- Non-termination.
never : A ⊥
never = later (♯ never)
-- run x for n steps peels off at most n "later" constructors from x.
run_for_steps : A ⊥ → ℕ → A ⊥
run now x for n steps = now x
run later x for zero steps = later x
run later x for suc n steps = run ♭ x for n steps
-- Is the computation done?
isNow : A ⊥ → Bool
isNow (now x) = true
isNow (later x) = false
------------------------------------------------------------------------
-- Kinds
-- The partiality monad comes with two forms of equality (weak and
-- strong) and one ordering. Strong equality is stronger than the
-- ordering, which is stronger than weak equality.
-- The three relations are defined using a single data type, indexed
-- by a "kind".
data OtherKind : Set where
geq weak : OtherKind
data Kind : Set where
strong : Kind
other : (k : OtherKind) → Kind
-- Kind equality is decidable.
infix 4 _≟-Kind_
_≟-Kind_ : DecidableEquality Kind
_≟-Kind_ strong strong = yes ≡.refl
_≟-Kind_ strong (other k) = no λ()
_≟-Kind_ (other k) strong = no λ()
_≟-Kind_ (other geq) (other geq) = yes ≡.refl
_≟-Kind_ (other geq) (other weak) = no λ()
_≟-Kind_ (other weak) (other geq) = no λ()
_≟-Kind_ (other weak) (other weak) = yes ≡.refl
-- A predicate which is satisfied only for equalities. Note that, for
-- concrete inputs, this predicate evaluates to ⊤ or ⊥.
Equality : Kind → Set
Equality k = False (k ≟-Kind other geq)
------------------------------------------------------------------------
-- Equality/ordering
module Equality {A : Set a} -- The "return type".
(_∼_ : A → A → Set ℓ) where
-- The three relations.
data Rel : Kind → A ⊥ → A ⊥ → Set (a ⊔ ℓ) where
now : ∀ {k x y} (x∼y : x ∼ y) → Rel k (now x) (now y)
later : ∀ {k x y} (x∼y : ∞ (Rel k (♭ x) (♭ y))) → Rel k (later x) (later y)
laterʳ : ∀ {x y} (x≈y : Rel (other weak) x (♭ y) ) → Rel (other weak) x (later y)
laterˡ : ∀ {k x y} (x∼y : Rel (other k) (♭ x) y ) → Rel (other k) (later x) y
infix 4 _≅_ _≳_ _≲_ _≈_
_≅_ : A ⊥ → A ⊥ → Set _
_≅_ = Rel strong
_≳_ : A ⊥ → A ⊥ → Set _
_≳_ = Rel (other geq)
_≲_ : A ⊥ → A ⊥ → Set _
_≲_ = flip _≳_
_≈_ : A ⊥ → A ⊥ → Set _
_≈_ = Rel (other weak)
-- x ⇓ y means that x terminates with y.
infix 4 _⇓[_]_ _⇓_
_⇓[_]_ : A ⊥ → Kind → A → Set _
x ⇓[ k ] y = Rel k x (now y)
_⇓_ : A ⊥ → A → Set _
x ⇓ y = x ⇓[ other weak ] y
-- x ⇓ means that x terminates.
infix 4 _⇓
_⇓ : A ⊥ → Set _
x ⇓ = ∃ λ v → x ⇓ v
-- x ⇑ means that x does not terminate.
infix 4 _⇑[_] _⇑
_⇑[_] : A ⊥ → Kind → Set _
x ⇑[ k ] = Rel k x never
_⇑ : A ⊥ → Set _
x ⇑ = x ⇑[ other weak ]
------------------------------------------------------------------------
-- Lemmas relating the three relations
module _ {A : Set a} {_∼_ : A → A → Set ℓ} where
open Equality _∼_ using (Rel; _≅_; _≳_; _≲_; _≈_; _⇓[_]_; _⇑[_])
open Equality.Rel
-- All relations include strong equality.
≅⇒ : ∀ {k} {x y : A ⊥} → x ≅ y → Rel k x y
≅⇒ (now x∼y) = now x∼y
≅⇒ (later x≅y) = later (♯ ≅⇒ (♭ x≅y))
-- The weak equality includes the ordering.
≳⇒ : ∀ {k} {x y : A ⊥} → x ≳ y → Rel (other k) x y
≳⇒ (now x∼y) = now x∼y
≳⇒ (later x≳y) = later (♯ ≳⇒ (♭ x≳y))
≳⇒ (laterˡ x≳y) = laterˡ (≳⇒ x≳y )
-- Weak equality includes the other relations.
⇒≈ : ∀ {k} {x y : A ⊥} → Rel k x y → x ≈ y
⇒≈ {strong} = ≅⇒
⇒≈ {other geq} = ≳⇒
⇒≈ {other weak} = id
-- The relations agree for non-terminating computations.
never⇒never : ∀ {k₁ k₂} {x : A ⊥} →
Rel k₁ x never → Rel k₂ x never
never⇒never (later x∼never) = later (♯ never⇒never (♭ x∼never))
never⇒never (laterʳ x≈never) = never⇒never x≈never
never⇒never (laterˡ x∼never) = later (♯ never⇒never x∼never)
-- The "other" relations agree when the right-hand side is a value.
now⇒now : ∀ {k₁ k₂} {x} {y : A} →
Rel (other k₁) x (now y) → Rel (other k₂) x (now y)
now⇒now (now x∼y) = now x∼y
now⇒now (laterˡ x∼now) = laterˡ (now⇒now x∼now)
------------------------------------------------------------------------
-- Later can be dropped
laterʳ⁻¹ : ∀ {k} {x : A ⊥} {y} →
Rel (other k) x (later y) → Rel (other k) x (♭ y)
laterʳ⁻¹ (later x∼y) = laterˡ (♭ x∼y)
laterʳ⁻¹ (laterʳ x≈y) = x≈y
laterʳ⁻¹ (laterˡ x∼ly) = laterˡ (laterʳ⁻¹ x∼ly)
laterˡ⁻¹ : ∀ {x} {y : A ⊥} → later x ≈ y → ♭ x ≈ y
laterˡ⁻¹ (later x≈y) = laterʳ (♭ x≈y)
laterˡ⁻¹ (laterʳ lx≈y) = laterʳ (laterˡ⁻¹ lx≈y)
laterˡ⁻¹ (laterˡ x≈y) = x≈y
later⁻¹ : ∀ {k} {x y : ∞ (A ⊥)} →
Rel k (later x) (later y) → Rel k (♭ x) (♭ y)
later⁻¹ (later x∼y) = ♭ x∼y
later⁻¹ (laterʳ lx≈y) = laterˡ⁻¹ lx≈y
later⁻¹ (laterˡ x∼ly) = laterʳ⁻¹ x∼ly
------------------------------------------------------------------------
-- The relations are equivalences or partial orders, given suitable
-- assumptions about the underlying relation
module Equivalence where
-- Reflexivity.
refl : Reflexive _∼_ → ∀ {k} → Reflexive (Rel k)
refl refl-∼ {x = now v} = now refl-∼
refl refl-∼ {x = later x} = later (♯ refl refl-∼)
-- Symmetry.
sym : Symmetric _∼_ → ∀ {k} → Equality k → Symmetric (Rel k)
sym sym-∼ eq (now x∼y) = now (sym-∼ x∼y)
sym sym-∼ eq (later x∼y) = later (♯ sym sym-∼ eq (♭ x∼y))
sym sym-∼ eq (laterʳ x≈y) = laterˡ (sym sym-∼ eq x≈y )
sym sym-∼ eq (laterˡ {weak} x≈y) = laterʳ (sym sym-∼ eq x≈y )
-- Transitivity.
private
module Trans (trans-∼ : Transitive _∼_) where
now-trans : ∀ {k x y} {v : A} →
Rel k x y → Rel k y (now v) → Rel k x (now v)
now-trans (now x∼y) (now y∼z) = now (trans-∼ x∼y y∼z)
now-trans (laterˡ x∼y) y∼z = laterˡ (now-trans x∼y y∼z)
now-trans x∼ly (laterˡ y∼z) = now-trans (laterʳ⁻¹ x∼ly) y∼z
mutual
later-trans : ∀ {k} {x y : A ⊥} {z} →
Rel k x y → Rel k y (later z) → Rel k x (later z)
later-trans (later x∼y) ly∼lz = later (♯ trans (♭ x∼y) (later⁻¹ ly∼lz))
later-trans (laterˡ x∼y) y∼lz = later (♯ trans x∼y (laterʳ⁻¹ y∼lz))
later-trans (laterʳ x≈y) ly≈lz = later-trans x≈y (laterˡ⁻¹ ly≈lz)
later-trans x≈y (laterʳ y≈z) = laterʳ ( trans x≈y y≈z )
trans : ∀ {k} {x y z : A ⊥} → Rel k x y → Rel k y z → Rel k x z
trans {z = now v} x∼y y∼v = now-trans x∼y y∼v
trans {z = later z} x∼y y∼lz = later-trans x∼y y∼lz
open Trans public using (trans)
-- All the relations are preorders.
preorder : IsPreorder _≡_ _∼_ → Kind → Preorder _ _ _
preorder pre k = record
{ Carrier = A ⊥
; _≈_ = _≡_
; _≲_ = Rel k
; isPreorder = record
{ isEquivalence = ≡.isEquivalence
; reflexive = refl′
; trans = Equivalence.trans (IsPreorder.trans pre)
}
}
where
refl′ : ∀ {k} {x y : A ⊥} → x ≡ y → Rel k x y
refl′ ≡.refl = Equivalence.refl (IsPreorder.refl pre)
private
preorder′ : IsEquivalence _∼_ → Kind → Preorder _ _ _
preorder′ equiv =
preorder (SetoidProperties.isPreorder (record { isEquivalence = equiv }))
-- The two equalities are equivalence relations.
setoid : IsEquivalence _∼_ →
(k : Kind) {eq : Equality k} → Setoid _ _
setoid equiv k {eq} = record
{ Carrier = A ⊥
; _≈_ = Rel k
; isEquivalence = record
{ refl = Pre.refl
; sym = Equivalence.sym (IsEquivalence.sym equiv) eq
; trans = Pre.trans
}
} where module Pre = Preorder (preorder′ equiv k)
-- The order is a partial order, with strong equality as the
-- underlying equality.
≳-poset : IsEquivalence _∼_ → Poset _ _ _
≳-poset equiv = record
{ Carrier = A ⊥
; _≈_ = _≅_
; _≤_ = _≳_
; isPartialOrder = record
{ antisym = antisym
; isPreorder = record
{ isEquivalence = S.isEquivalence
; reflexive = ≅⇒
; trans = Pre.trans
}
}
}
where
module S = Setoid (setoid equiv strong)
module Pre = Preorder (preorder′ equiv (other geq))
antisym : {x y : A ⊥} → x ≳ y → x ≲ y → x ≅ y
antisym (now x∼y) (now _) = now x∼y
antisym (later x≳y) (later x≲y) = later (♯ antisym (♭ x≳y) (♭ x≲y))
antisym (later x≳y) (laterˡ x≲ly) = later (♯ antisym (♭ x≳y) (laterʳ⁻¹ x≲ly))
antisym (laterˡ x≳ly) (later x≲y) = later (♯ antisym (laterʳ⁻¹ x≳ly) (♭ x≲y))
antisym (laterˡ x≳ly) (laterˡ x≲ly) = later (♯ antisym (laterʳ⁻¹ x≳ly) (laterʳ⁻¹ x≲ly))
-- Equational reasoning.
module Reasoning (isEquivalence : IsEquivalence _∼_) where
private
module Pre {k} = Preorder (preorder′ isEquivalence k)
module S {k eq} = Setoid (setoid isEquivalence k {eq})
infix 3 _∎
infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≈⟨_⟩_
_≡⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≡ y → Rel k y z → Rel k x z
_ ≡⟨ ≡.refl ⟩ y∼z = y∼z
_≅⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≅ y → Rel k y z → Rel k x z
_ ≅⟨ x≅y ⟩ y∼z = Pre.trans (≅⇒ x≅y) y∼z
_≳⟨_⟩_ : ∀ {k} x {y z : A ⊥} →
x ≳ y → Rel (other k) y z → Rel (other k) x z
_ ≳⟨ x≳y ⟩ y∼z = Pre.trans (≳⇒ x≳y) y∼z
_≈⟨_⟩_ : ∀ x {y z : A ⊥} → x ≈ y → y ≈ z → x ≈ z
_ ≈⟨ x≈y ⟩ y≈z = Pre.trans x≈y y≈z
sym : ∀ {k} {eq : Equality k} {x y : A ⊥} →
Rel k x y → Rel k y x
sym {eq = eq} = S.sym {eq = eq}
_∎ : ∀ {k} (x : A ⊥) → Rel k x x
x ∎ = Pre.refl
------------------------------------------------------------------------
-- Lemmas related to now and never
-- Now is not never.
now≉never : ∀ {k} {x : A} → ¬ Rel k (now x) never
now≉never (laterʳ hyp) = now≉never hyp
-- A partial value is either now or never (classically, when the
-- underlying relation is reflexive).
now-or-never : Reflexive _∼_ →
∀ {k} (x : A ⊥) →
¬ ¬ ((∃ λ y → x ⇓[ other k ] y) ⊎ x ⇑[ other k ])
now-or-never refl x = helper <$> ¬¬-excluded-middle
where
open RawMonad ¬¬-Monad
not-now-is-never : (x : A ⊥) → (∄ λ y → x ≳ now y) → x ≳ never
not-now-is-never (now x) hyp with hyp (-, now refl)
... | ()
not-now-is-never (later x) hyp =
later (♯ not-now-is-never (♭ x) (hyp ∘ Prod.map id laterˡ))
helper : Dec (∃ λ y → x ≳ now y) → _
helper (yes ≳now) = inj₁ $ Prod.map id ≳⇒ ≳now
helper (no ≵now) = inj₂ $ ≳⇒ $ not-now-is-never x ≵now
------------------------------------------------------------------------
-- Map-like results
-- Map.
map : ∀ {_∼′_ : A → A → Set a} {k} →
_∼′_ ⇒ _∼_ → Equality.Rel _∼′_ k ⇒ Equality.Rel _∼_ k
map ∼′⇒∼ (now x∼y) = now (∼′⇒∼ x∼y)
map ∼′⇒∼ (later x∼y) = later (♯ map ∼′⇒∼ (♭ x∼y))
map ∼′⇒∼ (laterʳ x≈y) = laterʳ (map ∼′⇒∼ x≈y)
map ∼′⇒∼ (laterˡ x∼y) = laterˡ (map ∼′⇒∼ x∼y)
-- If a statement can be proved using propositional equality as the
-- underlying relation, then it can also be proved for any other
-- reflexive underlying relation.
≡⇒ : Reflexive _∼_ →
∀ {k x y} → Equality.Rel _≡_ k x y → Rel k x y
≡⇒ refl-∼ = map (flip (≡.subst (_∼_ _)) refl-∼)
------------------------------------------------------------------------
-- Steps
-- The number of later constructors (steps) in the terminating
-- computation x.
steps : ∀ {k} {x : A ⊥} {y} → x ⇓[ k ] y → ℕ
steps (now _) = zero
steps .{x = later x} (laterˡ {x = x} x⇓) = suc (steps {x = ♭ x} x⇓)
module Steps {trans-∼ : Transitive _∼_} where
left-identity :
∀ {k x y} {z : A}
(x≅y : x ≅ y) (y⇓z : y ⇓[ k ] z) →
steps (Equivalence.trans trans-∼ (≅⇒ x≅y) y⇓z) ≡ steps y⇓z
left-identity (now _) (now _) = ≡.refl
left-identity (later x≅y) (laterˡ y⇓z) =
≡.cong suc $ left-identity (♭ x≅y) y⇓z
right-identity :
∀ {k x} {y z : A}
(x⇓y : x ⇓[ k ] y) (y≈z : now y ⇓[ k ] z) →
steps (Equivalence.trans trans-∼ x⇓y y≈z) ≡ steps x⇓y
right-identity (now x∼y) (now y∼z) = ≡.refl
right-identity (laterˡ x∼y) (now y∼z) =
≡.cong suc $ right-identity x∼y (now y∼z)
------------------------------------------------------------------------
-- Laws related to bind
-- Never is a left and right "zero" of bind.
left-zero : (f : B → A ⊥) → let open M in
(never >>= f) ≅ never
left-zero f = later (♯ left-zero f)
right-zero : (x : B ⊥) → let open M in
(x >>= λ _ → never) ≅ never
right-zero (later x) = later (♯ right-zero (♭ x))
right-zero (now x) = never≅never
where never≅never : never ≅ never
never≅never = later (♯ never≅never)
-- Now is a left and right identity of bind (for a reflexive
-- underlying relation).
left-identity : Reflexive _∼_ →
(x : B) (f : B → A ⊥) → let open M in
(now x >>= f) ≅ f x
left-identity refl-∼ x f = Equivalence.refl refl-∼
right-identity : Reflexive _∼_ →
(x : A ⊥) → let open M in
(x >>= now) ≅ x
right-identity refl (now x) = now refl
right-identity refl (later x) = later (♯ right-identity refl (♭ x))
-- Bind is associative (for a reflexive underlying relation).
associative : Reflexive _∼_ →
(x : C ⊥) (f : C → B ⊥) (g : B → A ⊥) →
let open M in
(x >>= f >>= g) ≅ (x >>= λ y → f y >>= g)
associative refl-∼ (now x) f g = Equivalence.refl refl-∼
associative refl-∼ (later x) f g =
later (♯ associative refl-∼ (♭ x) f g)
module _ {A B : Set s}
{_∼A_ : A → A → Set ℓ}
{_∼B_ : B → B → Set ℓ} where
open Equality
private
open module EqA = Equality _∼A_ using () renaming (_⇓[_]_ to _⇓[_]A_; _⇑[_] to _⇑[_]A)
open module EqB = Equality _∼B_ using () renaming (_⇓[_]_ to _⇓[_]B_; _⇑[_] to _⇑[_]B)
-- Bind preserves all the relations.
infixl 1 _>>=-cong_
_>>=-cong_ :
∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
Rel _∼A_ k x₁ x₂ →
(∀ {x₁ x₂} → x₁ ∼A x₂ → Rel _∼B_ k (f₁ x₁) (f₂ x₂)) →
Rel _∼B_ k (x₁ >>= f₁) (x₂ >>= f₂)
now x₁∼x₂ >>=-cong f₁∼f₂ = f₁∼f₂ x₁∼x₂
later x₁∼x₂ >>=-cong f₁∼f₂ = later (♯ (♭ x₁∼x₂ >>=-cong f₁∼f₂))
laterʳ x₁≈x₂ >>=-cong f₁≈f₂ = laterʳ (x₁≈x₂ >>=-cong f₁≈f₂)
laterˡ x₁∼x₂ >>=-cong f₁∼f₂ = laterˡ (x₁∼x₂ >>=-cong f₁∼f₂)
-- Inversion lemmas for bind.
>>=-inversion-⇓ :
Reflexive _∼A_ →
∀ {k} x {f : A → B ⊥} {y} → let open M in
(x>>=f⇓ : (x >>= f) ⇓[ k ]B y) →
∃ λ z → ∃₂ λ (x⇓ : x ⇓[ k ]A z) (fz⇓ : f z ⇓[ k ]B y) →
steps x⇓ + steps fz⇓ ≡ steps x>>=f⇓
>>=-inversion-⇓ refl (now x) fx⇓ =
(x , now refl , fx⇓ , ≡.refl)
>>=-inversion-⇓ refl (later x) (laterˡ x>>=f⇓) =
Prod.map id (Prod.map laterˡ (Prod.map id (≡.cong suc))) $
>>=-inversion-⇓ refl (♭ x) x>>=f⇓
>>=-inversion-⇑ : IsEquivalence _∼A_ →
∀ {k} x {f : A → B ⊥} → let open M in
Rel _∼B_ (other k) (x >>= f) never →
¬ ¬ (x ⇑[ other k ]A ⊎
∃ λ y → x ⇓[ other k ]A y × f y ⇑[ other k ]B)
>>=-inversion-⇑ eqA {k} x {f} ∼never =
helper <$> now-or-never IsEqA.refl x
where
open RawMonad ¬¬-Monad using (_<$>_)
open M using (_>>=_)
open Reasoning eqA
module IsEqA = IsEquivalence eqA
k≳ = other geq
is-never : ∀ {x y} →
x ⇓[ k≳ ]A y → (x >>= f) ⇑[ k≳ ]B →
∃ λ z → (y ∼A z) × f z ⇑[ k≳ ]B
is-never (now x∼y) = λ fx⇑ → (_ , IsEqA.sym x∼y , fx⇑)
is-never (laterˡ ≳now) = is-never ≳now ∘ later⁻¹
helper : (∃ λ y → x ⇓[ k≳ ]A y) ⊎ x ⇑[ k≳ ]A →
x ⇑[ other k ]A ⊎
∃ λ y → x ⇓[ other k ]A y × f y ⇑[ other k ]B
helper (inj₂ ≳never) = inj₁ (≳⇒ ≳never)
helper (inj₁ (y , ≳now)) with is-never ≳now (never⇒never ∼never)
... | (z , y∼z , fz⇑) = inj₂ (z , ≳⇒ (x ≳⟨ ≳now ⟩
now y ≅⟨ now y∼z ⟩
now z ∎)
, ≳⇒ fz⇑)
module _ {A B : Set ℓ} {_∼_ : B → B → Set ℓ} where
open Equality
-- A variant of _>>=-cong_.
infixl 1 _≡->>=-cong_
_≡->>=-cong_ :
∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
Rel _≡_ k x₁ x₂ →
(∀ x → Rel _∼_ k (f₁ x) (f₂ x)) →
Rel _∼_ k (x₁ >>= f₁) (x₂ >>= f₂)
_≡->>=-cong_ {k} {f₁ = f₁} {f₂} x₁≈x₂ f₁≈f₂ =
x₁≈x₂ >>=-cong λ {x} x≡x′ →
≡.subst (λ y → Rel _∼_ k (f₁ x) (f₂ y)) x≡x′ (f₁≈f₂ x)
------------------------------------------------------------------------
-- Productivity checker workaround
-- The monad can be awkward to use, due to the limitations of guarded
-- coinduction. The following code provides a (limited) workaround.
module Workaround {a} where
infixl 1 _>>=_
data _⊥P : Set a → Set (Level.suc a) where
now : (x : A) → A ⊥P
later : (x : ∞ (A ⊥P)) → A ⊥P
_>>=_ : (x : A ⊥P) (f : A → B ⊥P) → B ⊥P
private
data _⊥W : Set a → Set (Level.suc a) where
now : (x : A) → A ⊥W
later : (x : A ⊥P) → A ⊥W
mutual
_>>=W_ : A ⊥W → (A → B ⊥P) → B ⊥W
now x >>=W f = whnf (f x)
later x >>=W f = later (x >>= f)
whnf : A ⊥P → A ⊥W
whnf (now x) = now x
whnf (later x) = later (♭ x)
whnf (x >>= f) = whnf x >>=W f
mutual
private
⟦_⟧W : A ⊥W → A ⊥
⟦ now x ⟧W = now x
⟦ later x ⟧W = later (♯ ⟦ x ⟧P)
⟦_⟧P : A ⊥P → A ⊥
⟦ x ⟧P = ⟦ whnf x ⟧W
-- The definitions above make sense. ⟦_⟧P is homomorphic with
-- respect to now, later and _>>=_.
module Correct where
private
open module Eq {A : Set a} = Equality {A = A} _≡_
open module R {A : Set a} = Reasoning (≡.isEquivalence {A = A})
now-hom : (x : A) → ⟦ now x ⟧P ≅ now x
now-hom x = now x ∎
later-hom : (x : ∞ (A ⊥P)) → ⟦ later x ⟧P ≅ later (♯ ⟦ ♭ x ⟧P)
later-hom x = later (♯ (⟦ ♭ x ⟧P ∎))
mutual
private
>>=-homW : (x : B ⊥W) (f : B → A ⊥P) →
⟦ x >>=W f ⟧W ≅ M._>>=_ ⟦ x ⟧W (λ y → ⟦ f y ⟧P)
>>=-homW (now x) f = ⟦ f x ⟧P ∎
>>=-homW (later x) f = later (♯ >>=-hom x f)
>>=-hom : (x : B ⊥P) (f : B → A ⊥P) →
⟦ x >>= f ⟧P ≅ M._>>=_ ⟦ x ⟧P (λ y → ⟦ f y ⟧P)
>>=-hom x f = >>=-homW (whnf x) f
------------------------------------------------------------------------
-- An alternative, but equivalent, formulation of equality/ordering
module AlternativeEquality {a ℓ} where
private
El : Setoid a ℓ → Set _
El = Setoid.Carrier
Eq : ∀ S → B.Rel (El S) _
Eq = Setoid._≈_
open Equality using (Rel)
open Equality.Rel
infix 4 _∣_≅P_ _∣_≳P_ _∣_≈P_
infix 3 _∎
infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≳⟨_⟩≅_ _≳⟨_⟩≈_ _≈⟨_⟩≅_ _≈⟨_⟩≲_
infixl 1 _>>=_
mutual
-- Proof "programs".
_∣_≅P_ : ∀ S → B.Rel (El S ⊥) _
_∣_≅P_ = flip RelP strong
_∣_≳P_ : ∀ S → B.Rel (El S ⊥) _
_∣_≳P_ = flip RelP (other geq)
_∣_≈P_ : ∀ S → B.Rel (El S ⊥) _
_∣_≈P_ = flip RelP (other weak)
data RelP S : Kind → B.Rel (El S ⊥) (Level.suc (a ⊔ ℓ)) where
-- Congruences.
now : ∀ {k x y} (xRy : x ⟨ Eq S ⟩ y) → RelP S k (now x) (now y)
later : ∀ {k x y} (x∼y : ∞ (RelP S k (♭ x) (♭ y))) →
RelP S k (later x) (later y)
_>>=_ : ∀ {S′ : Setoid a ℓ} {k} {x₁ x₂}
{f₁ f₂ : El S′ → El S ⊥} →
let open M in
(x₁∼x₂ : RelP S′ k x₁ x₂)
(f₁∼f₂ : ∀ {x y} → x ⟨ Eq S′ ⟩ y →
RelP S k (f₁ x) (f₂ y)) →
RelP S k (x₁ >>= f₁) (x₂ >>= f₂)
-- Ordering/weak equality.
laterʳ : ∀ {x y} (x≈y : RelP S (other weak) x (♭ y)) → RelP S (other weak) x (later y)
laterˡ : ∀ {k x y} (x∼y : RelP S (other k) (♭ x) y) → RelP S (other k) (later x) y
-- Equational reasoning. Note that including full transitivity
-- for weak equality would make _∣_≈P_ trivial; a similar
-- problem applies to _∣_≳P_ (A ∣ never ≳P now x would be
-- provable). Instead the definition of RelP includes limited
-- notions of transitivity, similar to weak bisimulation up-to
-- various things.
_∎ : ∀ {k} x → RelP S k x x
sym : ∀ {k x y} {eq : Equality k} (x∼y : RelP S k x y) → RelP S k y x
_≡⟨_⟩_ : ∀ {k} x {y z} (x≡y : x ≡ y) (y∼z : RelP S k y z) → RelP S k x z
_≅⟨_⟩_ : ∀ {k} x {y z} (x≅y : S ∣ x ≅P y) (y∼z : RelP S k y z) → RelP S k x z
_≳⟨_⟩_ : let open Equality (Eq S) in
∀ x {y z} (x≳y : x ≳ y) (y≳z : S ∣ y ≳P z) → S ∣ x ≳P z
_≳⟨_⟩≅_ : ∀ x {y z} (x≳y : S ∣ x ≳P y) (y≅z : S ∣ y ≅P z) → S ∣ x ≳P z
_≳⟨_⟩≈_ : ∀ x {y z} (x≳y : S ∣ x ≳P y) (y≈z : S ∣ y ≈P z) → S ∣ x ≈P z
_≈⟨_⟩≅_ : ∀ x {y z} (x≈y : S ∣ x ≈P y) (y≅z : S ∣ y ≅P z) → S ∣ x ≈P z
_≈⟨_⟩≲_ : ∀ x {y z} (x≈y : S ∣ x ≈P y) (y≲z : S ∣ z ≳P y) → S ∣ x ≈P z
-- If any of the following transitivity-like rules were added to
-- RelP, then RelP and Rel would no longer be equivalent:
--
-- x ≳P y → y ≳P z → x ≳P z
-- x ≳P y → y ≳ z → x ≳P z
-- x ≲P y → y ≈P z → x ≈P z
-- x ≈P y → y ≳P z → x ≈P z
-- x ≲ y → y ≈P z → x ≈P z
-- x ≈P y → y ≳ z → x ≈P z
-- x ≈P y → y ≈P z → x ≈P z
-- x ≈P y → y ≈ z → x ≈P z
-- x ≈ y → y ≈P z → x ≈P z
--
-- The reason is that any of these rules would make it possible
-- to derive that never and now x are related.
-- RelP is complete with respect to Rel.
complete : ∀ {S k} {x y : El S ⊥} →
Equality.Rel (Eq S) k x y → RelP S k x y
complete (now xRy) = now xRy
complete (later x∼y) = later (♯ complete (♭ x∼y))
complete (laterʳ x≈y) = laterʳ (complete x≈y)
complete (laterˡ x∼y) = laterˡ (complete x∼y)
-- RelP is sound with respect to Rel.
private
-- Proof WHNFs.
data RelW S : Kind → B.Rel (El S ⊥) (Level.suc (a ⊔ ℓ)) where
now : ∀ {k x y} (xRy : x ⟨ Eq S ⟩ y) → RelW S k (now x) (now y)
later : ∀ {k x y} (x∼y : RelP S k (♭ x) (♭ y)) → RelW S k (later x) (later y)
laterʳ : ∀ {x y} (x≈y : RelW S (other weak) x (♭ y)) → RelW S (other weak) x (later y)
laterˡ : ∀ {k x y} (x∼y : RelW S (other k) (♭ x) y) → RelW S (other k) (later x) y
-- WHNFs can be turned into programs.
program : ∀ {S k x y} → RelW S k x y → RelP S k x y
program (now xRy) = now xRy
program (later x∼y) = later (♯ x∼y)
program (laterˡ x∼y) = laterˡ (program x∼y)
program (laterʳ x≈y) = laterʳ (program x≈y)
-- Lemmas for WHNFs.
_>>=W_ : ∀ {A B k x₁ x₂} {f₁ f₂ : El A → El B ⊥} →
RelW A k x₁ x₂ →
(∀ {x y} → x ⟨ Eq A ⟩ y → RelW B k (f₁ x) (f₂ y)) →
RelW B k (M._>>=_ x₁ f₁) (M._>>=_ x₂ f₂)
now xRy >>=W f₁∼f₂ = f₁∼f₂ xRy
later x∼y >>=W f₁∼f₂ = later (x∼y >>= program ∘ f₁∼f₂)
laterʳ x≈y >>=W f₁≈f₂ = laterʳ (x≈y >>=W f₁≈f₂)
laterˡ x∼y >>=W f₁∼f₂ = laterˡ (x∼y >>=W f₁∼f₂)
reflW : ∀ {S k} x → RelW S k x x
reflW {S} (now x) = now (Setoid.refl S)
reflW (later x) = later (♭ x ∎)
symW : ∀ {S k x y} → Equality k → RelW S k x y → RelW S k y x
symW {S} eq (now xRy) = now (Setoid.sym S xRy)
symW eq (later x≈y) = later (sym {eq = eq} x≈y)
symW eq (laterʳ x≈y) = laterˡ (symW eq x≈y)
symW eq (laterˡ {weak} x≈y) = laterʳ (symW eq x≈y)
trans≅W : ∀ {S x y z} →
RelW S strong x y → RelW S strong y z → RelW S strong x z
trans≅W {S} (now xRy) (now yRz) = now (Setoid.trans S xRy yRz)
trans≅W (later x≅y) (later y≅z) = later (_ ≅⟨ x≅y ⟩ y≅z)
trans≳-W : ∀ {S x y z} → let open Equality (Eq S) in
x ≳ y → RelW S (other geq) y z → RelW S (other geq) x z
trans≳-W {S} (now xRy) (now yRz) = now (Setoid.trans S xRy yRz)
trans≳-W (later x≳y) (later y≳z) = later (_ ≳⟨ ♭ x≳y ⟩ y≳z)
trans≳-W (later x≳y) (laterˡ y≳z) = laterˡ (trans≳-W (♭ x≳y) y≳z)
trans≳-W (laterˡ x≳y) y≳z = laterˡ (trans≳-W x≳y y≳z)
-- Strong equality programs can be turned into WHNFs.
whnf≅ : ∀ {S x y} → S ∣ x ≅P y → RelW S strong x y
whnf≅ (now xRy) = now xRy
whnf≅ (later x≅y) = later (♭ x≅y)
whnf≅ (x₁≅x₂ >>= f₁≅f₂) = whnf≅ x₁≅x₂ >>=W λ xRy → whnf≅ (f₁≅f₂ xRy)
whnf≅ (x ∎) = reflW x
whnf≅ (sym x≅y) = symW _ (whnf≅ x≅y)
whnf≅ (x ≡⟨ ≡.refl ⟩ y≅z) = whnf≅ y≅z
whnf≅ (x ≅⟨ x≅y ⟩ y≅z) = trans≅W (whnf≅ x≅y) (whnf≅ y≅z)
-- More transitivity lemmas.
_⟨_⟩≅_ : ∀ {S k} x {y z} →
RelP S k x y → S ∣ y ≅P z → RelP S k x z
_⟨_⟩≅_ {k = strong} x x≅y y≅z = x ≅⟨ x≅y ⟩ y≅z
_⟨_⟩≅_ {k = other geq} x x≳y y≅z = x ≳⟨ x≳y ⟩≅ y≅z
_⟨_⟩≅_ {k = other weak} x x≈y y≅z = x ≈⟨ x≈y ⟩≅ y≅z
trans∼≅W : ∀ {S k x y z} →
RelW S k x y → RelW S strong y z → RelW S k x z
trans∼≅W {S} (now xRy) (now yRz) = now (Setoid.trans S xRy yRz)
trans∼≅W (later x∼y) (later y≅z) = later (_ ⟨ x∼y ⟩≅ y≅z)
trans∼≅W (laterʳ x≈y) (later y≅z) = laterʳ (trans∼≅W x≈y (whnf≅ y≅z))
trans∼≅W (laterˡ x∼y) y≅z = laterˡ (trans∼≅W x∼y y≅z)
trans≅∼W : ∀ {S k x y z} →
RelW S strong x y → RelW S k y z → RelW S k x z
trans≅∼W {S} (now xRy) (now yRz) = now (Setoid.trans S xRy yRz)
trans≅∼W (later x≅y) (later y∼z) = later (_ ≅⟨ x≅y ⟩ y∼z)
trans≅∼W (later x≅y) (laterˡ y∼z) = laterˡ (trans≅∼W (whnf≅ x≅y) y∼z)
trans≅∼W x≅y (laterʳ ly≈z) = laterʳ (trans≅∼W x≅y ly≈z)
-- Order programs can be turned into WHNFs.
whnf≳ : ∀ {S x y} → S ∣ x ≳P y → RelW S (other geq) x y
whnf≳ (now xRy) = now xRy
whnf≳ (later x∼y) = later (♭ x∼y)
whnf≳ (laterˡ x≲y) = laterˡ (whnf≳ x≲y)
whnf≳ (x₁∼x₂ >>= f₁∼f₂) = whnf≳ x₁∼x₂ >>=W λ xRy → whnf≳ (f₁∼f₂ xRy)
whnf≳ (x ∎) = reflW x
whnf≳ (x ≡⟨ ≡.refl ⟩ y≳z) = whnf≳ y≳z
whnf≳ (x ≅⟨ x≅y ⟩ y≳z) = trans≅∼W (whnf≅ x≅y) (whnf≳ y≳z)
whnf≳ (x ≳⟨ x≳y ⟩ y≳z) = trans≳-W x≳y (whnf≳ y≳z)
whnf≳ (x ≳⟨ x≳y ⟩≅ y≅z) = trans∼≅W (whnf≳ x≳y) (whnf≅ y≅z)
-- Another transitivity lemma.
trans≳≈W : ∀ {S x y z} →
RelW S (other geq) x y → RelW S (other weak) y z →
RelW S (other weak) x z
trans≳≈W {S} (now xRy) (now yRz) = now (Setoid.trans S xRy yRz)
trans≳≈W (later x≳y) (later y≈z) = later (_ ≳⟨ x≳y ⟩≈ y≈z)
trans≳≈W (laterˡ x≳y) y≈z = laterˡ (trans≳≈W x≳y y≈z)
trans≳≈W x≳y (laterʳ y≈z) = laterʳ (trans≳≈W x≳y y≈z)
trans≳≈W (later x≳y) (laterˡ y≈z) = laterˡ (trans≳≈W (whnf≳ x≳y) y≈z)
-- All programs can be turned into WHNFs.
whnf : ∀ {S k x y} → RelP S k x y → RelW S k x y
whnf (now xRy) = now xRy
whnf (later x∼y) = later (♭ x∼y)
whnf (laterʳ x≈y) = laterʳ (whnf x≈y)
whnf (laterˡ x∼y) = laterˡ (whnf x∼y)
whnf (x₁∼x₂ >>= f₁∼f₂) = whnf x₁∼x₂ >>=W λ xRy → whnf (f₁∼f₂ xRy)
whnf (x ∎) = reflW x
whnf (sym {eq = eq} x≈y) = symW eq (whnf x≈y)
whnf (x ≡⟨ ≡.refl ⟩ y∼z) = whnf y∼z
whnf (x ≅⟨ x≅y ⟩ y∼z) = trans≅∼W (whnf x≅y) (whnf y∼z)
whnf (x ≳⟨ x≳y ⟩ y≳z) = trans≳-W x≳y (whnf y≳z)
whnf (x ≳⟨ x≳y ⟩≅ y≅z) = trans∼≅W (whnf x≳y) (whnf y≅z)
whnf (x ≳⟨ x≳y ⟩≈ y≈z) = trans≳≈W (whnf x≳y) (whnf y≈z)
whnf (x ≈⟨ x≈y ⟩≅ y≅z) = trans∼≅W (whnf x≈y) (whnf y≅z)
whnf (x ≈⟨ x≈y ⟩≲ y≲z) = symW _ (trans≳≈W (whnf y≲z) (symW _ (whnf x≈y)))
mutual
-- Soundness.
private
soundW : ∀ {S k x y} → RelW S k x y → Rel (Eq S) k x y
soundW (now xRy) = now xRy
soundW (later x∼y) = later (♯ sound x∼y)
soundW (laterʳ x≈y) = laterʳ (soundW x≈y)
soundW (laterˡ x∼y) = laterˡ (soundW x∼y)
sound : ∀ {S k x y} → RelP S k x y → Rel (Eq S) k x y
sound x∼y = soundW (whnf x∼y)
-- RelP and Rel are equivalent (when the underlying relation is an
-- equivalence).
correct : ∀ {S k x y} → RelP S k x y ⇔ Rel (Eq S) k x y
correct = mk⇔ sound complete
------------------------------------------------------------------------
-- Another lemma
-- Bind is "idempotent".
idempotent :
(B : Setoid ℓ ℓ) →
let open M; open Setoid B using (_≈_; Carrier); open Equality _≈_ in
(x : A ⊥) (f : A → A → Carrier ⊥) →
(x >>= λ y′ → x >>= λ y″ → f y′ y″) ≳ (x >>= λ y′ → f y′ y′)
idempotent {A = A} B x f = sound (idem x)
where
open AlternativeEquality hiding (_>>=_)
open M
open Equality.Rel using (laterˡ)
open Equivalence using (refl)
idem : (x : A ⊥) →
B ∣ (x >>= λ y′ → x >>= λ y″ → f y′ y″) ≳P
(x >>= λ y′ → f y′ y′)
idem (now x) = f x x ∎
idem (later x) = later (♯ (
(♭ x >>= λ y′ → later x >>= λ y″ → f y′ y″) ≳⟨ (refl ≡.refl {x = ♭ x} ≡->>=-cong λ _ →
laterˡ (refl (Setoid.refl B))) ⟩
(♭ x >>= λ y′ → ♭ x >>= λ y″ → f y′ y″) ≳⟨ idem (♭ x) ⟩≅
(♭ x >>= λ y′ → f y′ y′) ∎))