diff --git a/Class/Allable.agda b/Class/Allable.agda index c34d38c..9ecef53 100644 --- a/Class/Allable.agda +++ b/Class/Allable.agda @@ -1,4 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} module Class.Allable where open import Class.Allable.Core public -open import Class.Allable.Instance public +open import Class.Allable.Instances public diff --git a/Class/Allable/Core.agda b/Class/Allable/Core.agda index 04aa514..3af6517 100644 --- a/Class/Allable/Core.agda +++ b/Class/Allable/Core.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible #-} module Class.Allable.Core where open import Class.Prelude diff --git a/Class/Allable/Instance.agda b/Class/Allable/Instances.agda similarity index 56% rename from Class/Allable/Instance.agda rename to Class/Allable/Instances.agda index a1a2946..0bc9fc6 100644 --- a/Class/Allable/Instance.agda +++ b/Class/Allable/Instances.agda @@ -1,4 +1,5 @@ -module Class.Allable.Instance where +{-# OPTIONS --cubical-compatible #-} +module Class.Allable.Instances where open import Class.Prelude open import Class.Allable.Core @@ -18,20 +19,4 @@ instance Allable-Maybe .All = M.All Allable-List⁺ : Allable {ℓ} List⁺ - Allable-List⁺ .All P = All P ∘ toList - -private - open import Class.Decidable - open import Class.HasOrder - - _ : ∀[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0 - _ = auto - - _ : ∀[ x ∈ just 42 ] x > 0 - _ = auto - - _ : ∀[ x ∈ nothing ] x > 0 - _ = auto - - _ : ¬∀[ x ∈ just 0 ] x > 0 - _ = auto + Allable-List⁺ .All P = All P ∘ L⁺.toList diff --git a/Class/Anyable.agda b/Class/Anyable.agda index dadcee3..f02f396 100644 --- a/Class/Anyable.agda +++ b/Class/Anyable.agda @@ -1,4 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} module Class.Anyable where open import Class.Anyable.Core public -open import Class.Anyable.Instance public +open import Class.Anyable.Instances public diff --git a/Class/Anyable/Core.agda b/Class/Anyable/Core.agda index 6a9da9f..68a0f42 100644 --- a/Class/Anyable/Core.agda +++ b/Class/Anyable/Core.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible #-} module Class.Anyable.Core where open import Class.Prelude diff --git a/Class/Anyable/Instance.agda b/Class/Anyable/Instances.agda similarity index 59% rename from Class/Anyable/Instance.agda rename to Class/Anyable/Instances.agda index 2d24932..3a6d085 100644 --- a/Class/Anyable/Instance.agda +++ b/Class/Anyable/Instances.agda @@ -1,4 +1,5 @@ -module Class.Anyable.Instance where +{-# OPTIONS --cubical-compatible #-} +module Class.Anyable.Instances where open import Class.Prelude open import Class.Anyable.Core @@ -18,17 +19,4 @@ instance Anyable-Maybe .Any = M.Any Anyable-List⁺ : Anyable {ℓ} List⁺ - Anyable-List⁺ .Any P = Any P ∘ toList - -private - open import Class.Decidable - open import Class.HasOrder - - _ : ∃[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0 - _ = auto - - _ : ∃[ x ∈ just 42 ] x > 0 - _ = auto - - _ : ∄[ x ∈ nothing ] x > 0 - _ = auto + Anyable-List⁺ .Any P = Any P ∘ L⁺.toList diff --git a/Class/Applicative/Instances.agda b/Class/Applicative/Instances.agda index 365871c..c5292ff 100644 --- a/Class/Applicative/Instances.agda +++ b/Class/Applicative/Instances.agda @@ -49,7 +49,8 @@ instance -- Applicative-∃Vec : Applicative (∃ ∘ Vec) -- Applicative-∃Vec = λ where -- .pure x → 1 , pure x - -- ._<*>_ (n , xs) (m , ys) → {! (n ⊔ m) , zipWith _$_ xs ys -- (+ zipWith-⊔ lemma) !} + -- ._<*>_ (n , xs) (m , ys) → + -- {! (n ⊔ m) , zipWith _$_ xs ys (+ zipWith-⊔ lemma) !} private module M where open import Reflection.TCM.Syntax public diff --git a/Class/Coercions.agda b/Class/Coercions.agda new file mode 100644 index 0000000..7ed386a --- /dev/null +++ b/Class/Coercions.agda @@ -0,0 +1,19 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Coercions where + +open import Class.Prelude + +infix -1 _↝_ +record _↝_ (A : Type ℓ) (B : Type ℓ′) : Typeω where + field to : A → B + syntax to {B = B} = to[ B ] +open _↝_ ⦃...⦄ public + +tos : ⦃ A ↝ B ⦄ → List A ↝ List B +tos .to = map to + +infix -1 _⁇_↝_ +record _⁇_↝_ (A : Type ℓ) (P : Pred A ℓ′) (B : Type ℓ′) : Typeω where + field toBecause : (x : A) .{_ : P x} → B + syntax toBecause x {p} = ⌞ x ⊣ p ⌟ +open _⁇_↝_ ⦃...⦄ public diff --git a/Class/DecEq/Core.agda b/Class/DecEq/Core.agda index 22c1265..163b712 100644 --- a/Class/DecEq/Core.agda +++ b/Class/DecEq/Core.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --without-K #-} +{-# OPTIONS --cubical-compatible #-} module Class.DecEq.Core where open import Class.Prelude @@ -20,3 +20,6 @@ open DecEq ⦃...⦄ public DecEq¹ = DecEq ¹ DecEq² = DecEq ² DecEq³ = DecEq ³ + +Irrelevant⇒DecEq : Irrelevant A → DecEq A +Irrelevant⇒DecEq ∀≡ ._≟_ = yes ∘₂ ∀≡ diff --git a/Class/Decidable.agda b/Class/Decidable.agda index 0160abb..398a9e4 100644 --- a/Class/Decidable.agda +++ b/Class/Decidable.agda @@ -3,3 +3,4 @@ module Class.Decidable where open import Class.Decidable.Core public open import Class.Decidable.Instances public +open import Class.Decidable.WithoutK public diff --git a/Class/Decidable/Core.agda b/Class/Decidable/Core.agda index 2253ac7..6ae7553 100644 --- a/Class/Decidable/Core.agda +++ b/Class/Decidable/Core.agda @@ -1,11 +1,11 @@ -{-# OPTIONS --without-K #-} +{-# OPTIONS --cubical-compatible #-} module Class.Decidable.Core where +open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse) + open import Class.Prelude open import Class.Core -open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse) - record _⁇ (P : Type ℓ) : Type ℓ where constructor ⁇_ field dec : Dec P @@ -24,13 +24,6 @@ open _⁇ ⦃...⦄ public ¿_¿ᵇ : (P : Type ℓ) → ⦃ P ⁇ ⦄ → Bool ¿ P ¿ᵇ = ⌊ ¿ P ¿ ⌋ -infix 0 ifᵈ_then_else_ -ifᵈ_then_else_ : ∀ {X : Type ℓ} (P : Type ℓ′) - → ⦃ P ⁇ ⦄ → ({_ : P} → X) → ({_ : ¬ P} → X) → X -ifᵈ P then t else f with ¿ P ¿ -... | yes p = t {p} -... | no ¬p = f {¬p} - _⁇¹ = _⁇ ¹ _⁇² = _⁇ ² _⁇³ = _⁇ ³ diff --git a/Class/Decidable/Instances.agda b/Class/Decidable/Instances.agda index 567afe8..207e621 100644 --- a/Class/Decidable/Instances.agda +++ b/Class/Decidable/Instances.agda @@ -1,19 +1,14 @@ -{-# OPTIONS --without-K #-} +{-# OPTIONS --cubical-compatible #-} module Class.Decidable.Instances where open import Class.Prelude open import Class.Decidable.Core open import Class.DecEq.Core -private variable - n : ℕ - x : A - P Q : Pred A ℓ - R : Rel A ℓ - instance -- ** deriving from DecEq + DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇² DecEq⇒Dec = ⁇² _≟_ @@ -40,19 +35,6 @@ instance Dec-⊎ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A ⊎ B) ⁇ Dec-⊎ .dec = dec D.⊎-dec dec - import Data.Sum.Relation.Unary.All as ⊎; open ⊎ using (inj₁; inj₂) - open import Relation.Nullary.Decidable using () renaming (map′ to mapDec) - - Dec-⊎All : ⦃ P ⁇¹ ⦄ → ⦃ Q ⁇¹ ⦄ → ⊎.All P Q ⁇¹ - Dec-⊎All {P = P} {Q = Q} {x = inj₁ x} .dec = mapDec inj₁ inj₁˘ ¿ P x ¿ - where inj₁˘ : ⊎.All P Q (inj₁ x) → P x - inj₁˘ (inj₁ x) = x - Dec-⊎All {P = P} {Q = Q} {x = inj₂ y} .dec = mapDec inj₂ inj₂˘ ¿ Q y ¿ - where inj₂˘ : ⊎.All P Q (inj₂ x) → Q x - inj₂˘ (inj₂ x) = x - - import Data.Bool as 𝔹 - Dec-T : T ⁇¹ Dec-T = ⁇¹ 𝔹.T? @@ -70,7 +52,6 @@ instance Dec-AllPairs : ⦃ R ⁇² ⦄ → AP.AllPairs R ⁇¹ Dec-AllPairs = ⁇¹ AP.allPairs? dec² - open import Data.Vec as V open import Data.Vec.Relation.Unary.All as V open import Data.Vec.Relation.Unary.Any as V @@ -80,22 +61,19 @@ instance Dec-VAny : ⦃ P ⁇¹ ⦄ → V.Any P {n} ⁇¹ Dec-VAny = ⁇¹ V.any? dec¹ - import Data.Maybe as M - import Data.Maybe.Relation.Unary.All as M renaming (dec to all?) - import Data.Maybe.Relation.Unary.Any as M renaming (dec to any?) + import Data.Maybe.Relation.Unary.All as Mb renaming (dec to all?) + import Data.Maybe.Relation.Unary.Any as Mb renaming (dec to any?) - Dec-MAll : ⦃ P ⁇¹ ⦄ → M.All P ⁇¹ - Dec-MAll = ⁇¹ M.all? dec¹ + Dec-MAll : ⦃ P ⁇¹ ⦄ → Mb.All P ⁇¹ + Dec-MAll = ⁇¹ Mb.all? dec¹ - Dec-MAny : ⦃ P ⁇¹ ⦄ → M.Any P ⁇¹ - Dec-MAny = ⁇¹ M.any? dec¹ + Dec-MAny : ⦃ P ⁇¹ ⦄ → Mb.Any P ⁇¹ + Dec-MAny = ⁇¹ Mb.any? dec¹ -- ** inequalities - import Data.Nat.Properties as ℕ - - ℕ-Dec-≤ = ⁇² ℕ._≤?_ - ℕ-Dec-< = ⁇² ℕ.__) + Functor-Maybe = record {Mb′} + where module Mb′ = Mb renaming (map to _<$>_) FunctorLaws-Maybe : FunctorLaws Maybe FunctorLaws-Maybe = λ where @@ -32,12 +32,12 @@ instance (x ∷ xs) → cong (f (g x) ∷_) (q xs) Functor-List⁺ : Functor List⁺ - Functor-List⁺ = record {L} - where import Data.List.NonEmpty as L renaming (map to _<$>_) + Functor-List⁺ = record {L⁺′} + where module L⁺′ = L⁺ renaming (map to _<$>_) Functor-Vec : ∀ {n} → Functor (flip Vec n) - Functor-Vec = record {V} - where import Data.Vec as V renaming (map to _<$>_) + Functor-Vec = record {V′} + where module V′ = V renaming (map to _<$>_) Functor-TC : Functor TC Functor-TC = record {R} diff --git a/Class/Group.agda b/Class/Group.agda new file mode 100644 index 0000000..8437c5d --- /dev/null +++ b/Class/Group.agda @@ -0,0 +1,76 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Group where + +open import Class.Prelude +open import Class.Semigroup +open import Class.Monoid +open import Class.Setoid.Core + +record Group (A : Type ℓ) ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ : Type ℓ where + field _⁻¹ : A → A +open Group ⦃...⦄ public + +module _ (A : Type ℓ) ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ ⦃ _ : Group A ⦄ where + + record GroupLaws ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ : Type (ℓ ⊔ relℓ) where + open Alg≈ + field + inverse : Inverse ε _⁻¹ _◇_ + ⁻¹-cong : Congruent₁ _⁻¹ + + GroupLaws≡ : Type ℓ + GroupLaws≡ = GroupLaws + where instance _ = mkISetoid≡; _ = mkSetoidLaws≡ + +open GroupLaws ⦃...⦄ public + +-- ** integers +module _ where + open ℤ + import Data.Integer as ℤ + import Data.Integer.Properties as ℤ + + instance _ = mkISetoid≡; _ = mkSetoidLaws≡ + _ = Semigroup-ℤ-+ + _ = Monoid-ℤ-+ + Group-ℤ-+ = Group ℤ ∋ λ where ._⁻¹ → ℤ.-_ + instance _ = Group-ℤ-+ + GroupLaws-ℤ-+ = GroupLaws≡ ℤ ∋ record {inverse = ℤ.+-inverse ; ⁻¹-cong = cong (ℤ.-_)} + +-- G-sets +module _ (G : Type ℓ) ⦃ _ : Semigroup G ⦄ ⦃ _ : Monoid G ⦄ ⦃ _ : Group G ⦄ where + + module _ (X : Type ℓ′) ⦃ _ : ISetoid X ⦄ where + record Actionˡ : Type (ℓ ⊔ ℓ′ ⊔ relℓ) where + infixr 5 _·_ + field _·_ : G → X → X + identity : ∀ {x : X} → ε · x ≈ x + compatibility : ∀ {g h : G} {x : X} → g · h · x ≈ (g ◇ h) · x + record Actionʳ : Type (ℓ ⊔ ℓ′ ⊔ relℓ) where + infixl 5 _·_ + field _·_ : X → G → X + identity : ∀ {x : X} → x · ε ≈ x + compatibility : ∀ {x : X} {g h : G} → x · g · h ≈ x · (g ◇ h) + open Actionˡ ⦃...⦄ public renaming + (identity to ·-identity; compatibility to ·-compatibility) + + record GSet : Typeω where + field ⦃ action ⦄ : Actionˡ + open GSet ⦃...⦄ public + + record GSet′ : Typeω where + field + {ℓₓ} : Level + X : Type ℓₓ + ⦃ setoidX ⦄ : ISetoid X + action′ : Actionˡ X + open GSet′ public + + module GSet-Morphisms (X Y : Type ℓ′) + ⦃ ix : ISetoid X ⦄ ⦃ iy : ISetoid Y ⦄ + ⦃ _ : GSet X ⦄ ⦃ _ : GSet Y ⦄ where + record _—𝔾→_ : Type (ℓ ⊔ ℓ′ ⊔ relℓ ⦃ iy ⦄) where + field + F : X → Y + equivariant : ∀ {g : G} {x : X} → F (g · x) ≈ g · F x + open _—𝔾→_ public renaming (F to _𝔾⟨$⟩_) diff --git a/Class/HasAdd.agda b/Class/HasAdd.agda index a6681ac..1ca0f16 100644 --- a/Class/HasAdd.agda +++ b/Class/HasAdd.agda @@ -2,4 +2,4 @@ module Class.HasAdd where open import Class.HasAdd.Core public -open import Class.HasAdd.Instance public +open import Class.HasAdd.Instances public diff --git a/Class/HasAdd/Instance.agda b/Class/HasAdd/Instance.agda deleted file mode 100644 index 88c4a1a..0000000 --- a/Class/HasAdd/Instance.agda +++ /dev/null @@ -1,21 +0,0 @@ -{-# OPTIONS --cubical-compatible #-} -module Class.HasAdd.Instance where - -open import Class.HasAdd.Core -open import Data.Integer as ℤ using (ℤ) -open import Data.Nat as ℕ using (ℕ) -open import Data.Rational as ℚ using (ℚ) -open import Data.String as Str - -instance - addInt : HasAdd ℤ - addInt ._+_ = ℤ._+_ - - addNat : HasAdd ℕ - addNat ._+_ = ℕ._+_ - - addRat : HasAdd ℚ - addRat ._+_ = ℚ._+_ - - addString : HasAdd String - addString ._+_ = Str._++_ diff --git a/Class/HasAdd/Instances.agda b/Class/HasAdd/Instances.agda new file mode 100644 index 0000000..cc9a81b --- /dev/null +++ b/Class/HasAdd/Instances.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.HasAdd.Instances where + +open import Class.Prelude +open import Class.HasAdd.Core + +instance + addNat : HasAdd ℕ + addNat ._+_ = Nat._+_ + + addInt : HasAdd ℤ + addInt ._+_ = Int._+_ + + addRat : HasAdd ℚ + addRat ._+_ = Q._+_ + + addString : HasAdd String + addString ._+_ = Str._++_ diff --git a/Class/HasMembership.agda b/Class/HasMembership.agda new file mode 100644 index 0000000..61df8c8 --- /dev/null +++ b/Class/HasMembership.agda @@ -0,0 +1,6 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.HasMembership where + +open import Class.HasMembership.Core public +open import Class.HasMembership.Instances public +open import Class.HasMembership.MapWith public diff --git a/Class/HasMembership/Core.agda b/Class/HasMembership/Core.agda new file mode 100644 index 0000000..388c5c3 --- /dev/null +++ b/Class/HasMembership/Core.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.HasMembership.Core where + +open import Relation.Nullary.Decidable using (¬?) + +open import Class.Prelude +open import Class.Decidable.Core +open import Class.Decidable.Instances + +record HasMembership (F : Type ℓ → Type ℓ) : Type (lsuc $ lsuc ℓ) where + infix 4 _∈_ _∉_ + field _∈_ : A → F A → Type ℓ + + _∉_ : A → F A → Type ℓ + _∉_ = ¬_ ∘₂ _∈_ + + module _ ⦃ _ : _∈_ {A = A} ⁇² ⦄ where + infix 4 _∈?_ _∉?_ _∈ᵇ_ _∉ᵇ_ + + _∈?_ : Decidable² {A = A} _∈_ + _∈?_ = dec² + + _∉?_ : Decidable² {A = A} _∉_ + _∉?_ = dec² + + _∈ᵇ_ _∉ᵇ_ : A → F A → Bool + _∈ᵇ_ = isYes ∘₂ _∈?_ + _∉ᵇ_ = isYes ∘₂ _∉?_ + +open HasMembership ⦃...⦄ public diff --git a/Class/HasMembership/Instances.agda b/Class/HasMembership/Instances.agda new file mode 100644 index 0000000..d5d72e4 --- /dev/null +++ b/Class/HasMembership/Instances.agda @@ -0,0 +1,52 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.HasMembership.Instances where + +open import Class.Prelude +open import Class.HasMembership.Core + +open import Class.DecEq.Core + +open import Class.Decidable.Core +-- open import Class.Decidable.Instances + +instance + + M-List : HasMembership {ℓ} List + M-List = record {LMem} + where import Data.List.Membership.Propositional as LMem + + Dec∈-List : ⦃ _ : DecEq A ⦄ → _∈_ {F = List}{A} ⁇² + Dec∈-List = ⁇² DL._∈?_ + where import Data.List.Membership.DecPropositional _≟_ as DL + + M-Vec : HasMembership {ℓ} (flip Vec n) + M-Vec ._∈_ = λ x → VMem._∈_ x + where import Data.Vec.Membership.Propositional as VMem + + Dec∈-Vec : ⦃ _ : DecEq A ⦄ → _∈_ {F = flip Vec n}{A} ⁇² + Dec∈-Vec = ⁇² λ x → DV._∈?_ x + where import Data.Vec.Membership.DecPropositional _≟_ as DV + + M-List⁺ : HasMembership {ℓ} List⁺ + M-List⁺ ._∈_ x xs = x ∈ L⁺.toList xs + + Dec∈-List⁺ : ⦃ _ : DecEq A ⦄ → _∈_ {F = List⁺}{A} ⁇² + Dec∈-List⁺ .dec = _ ∈? L⁺.toList _ + + import Data.Maybe.Relation.Unary.Any as Mb + + M-Maybe : HasMembership {ℓ} Maybe + M-Maybe ._∈_ x mx = Mb.Any (_≡ x) mx + + Dec∈-Maybe : ⦃ _ : DecEq A ⦄ → _∈_ {F = Maybe}{A} ⁇² + Dec∈-Maybe .dec = Mb.dec (_≟ _) _ + +module _ {A B : Type} (f : A → B) where + + import Data.List.Membership.Propositional.Properties as LMem + + ∈⁺-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ L⁺.map f xs + ∈⁺-map⁺ = LMem.∈-map⁺ f + + ∈⁺-map⁻ : ∀ {y xs} → y ∈ L⁺.map f xs → ∃ λ x → x ∈ xs × y ≡ f x + ∈⁺-map⁻ = LMem.∈-map⁻ f diff --git a/Class/HasMembership/MapWith.agda b/Class/HasMembership/MapWith.agda new file mode 100644 index 0000000..c4063a0 --- /dev/null +++ b/Class/HasMembership/MapWith.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.HasMembership.MapWith where + +open import Class.Prelude +open import Class.HasMembership.Core +open import Class.HasMembership.Instances + +record Functor∈ (F : Type ℓ → Type ℓ) ⦃ _ : HasMembership F ⦄ : Type (lsuc ℓ) where + field mapWith∈ : ∀ {A B : Type ℓ} → (xs : F A) → (∀ {x : A} → x ∈ xs → B) → F B +open Functor∈ ⦃...⦄ public + +instance + F∈-List : Functor∈ {ℓ} List + F∈-List = record {LMem} + where import Data.List.Membership.Propositional as LMem + + F∈-List⁺ : Functor∈ {ℓ} List⁺ + F∈-List⁺ .mapWith∈ (_ ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there) + where open import Data.List.Relation.Unary.Any using (here; there) + + F∈-Vec : Functor∈ {ℓ} (flip Vec n) + F∈-Vec = record {VMem} + where import Data.Vec.Membership.Propositional as VMem + + F∈-Maybe : Functor∈ {ℓ} Maybe + F∈-Maybe .mapWith∈ = λ where + (just _) f → just $ f (Mb.just refl) + nothing f → nothing + where import Data.Maybe.Relation.Unary.Any as Mb diff --git a/Class/HasOrder.agda b/Class/HasOrder.agda index ec519fb..4e3f587 100644 --- a/Class/HasOrder.agda +++ b/Class/HasOrder.agda @@ -1,4 +1,5 @@ +{-# OPTIONS --without-K #-} module Class.HasOrder where open import Class.HasOrder.Core public -open import Class.HasOrder.Instance public +open import Class.HasOrder.Instances public diff --git a/Class/HasOrder/Core.agda b/Class/HasOrder/Core.agda index f5dc1e9..54d3538 100644 --- a/Class/HasOrder/Core.agda +++ b/Class/HasOrder/Core.agda @@ -2,7 +2,7 @@ module Class.HasOrder.Core where open import Class.Prelude -open import Class.Decidable +open import Class.Decidable.Core open import Function.Bundles using (module Equivalence; mk⇔; _⇔_) open import Relation.Binary using ( IsPreorder; IsPartialOrder; IsEquivalence; Total; IsTotalOrder diff --git a/Class/HasOrder/Instance.agda b/Class/HasOrder/Instances.agda similarity index 98% rename from Class/HasOrder/Instance.agda rename to Class/HasOrder/Instances.agda index db7678d..35ccb06 100644 --- a/Class/HasOrder/Instance.agda +++ b/Class/HasOrder/Instances.agda @@ -1,5 +1,5 @@ {-# OPTIONS --without-K #-} -module Class.HasOrder.Instance where +module Class.HasOrder.Instances where open import Class.DecEq open import Class.Decidable diff --git a/Class/Measurable.agda b/Class/Measurable.agda new file mode 100644 index 0000000..61d3a89 --- /dev/null +++ b/Class/Measurable.agda @@ -0,0 +1,74 @@ +{-# OPTIONS --without-K #-} +module Class.Measurable where + +open import Class.Prelude +open Nat using (_+_) + +record Measurable {ℓ} (A : Type ℓ) : Type ℓ where + field ∣_∣ : A → ℕ +open Measurable ⦃...⦄ public + +-- ** instances + +instance + Measurable-ℕ : Measurable ℕ + Measurable-ℕ .∣_∣ x = x + + Measurable-⊎ : ⦃ _ : Measurable A ⦄ ⦃ _ : Measurable B ⦄ → Measurable (A ⊎ B) + Measurable-⊎ .∣_∣ = λ where + (inj₁ x) → ∣ x ∣ + (inj₂ x) → ∣ x ∣ + +-- alternatives for products +Measurable-×ˡ : ⦃ Measurable A ⦄ → Measurable (A × B) +Measurable-×ˡ .∣_∣ (x , _) = ∣ x ∣ + +Measurable-×ʳ : ⦃ Measurable B ⦄ → Measurable (A × B) +Measurable-×ʳ .∣_∣ (_ , x) = ∣ x ∣ + +Measurable-×ˡʳ : ⦃ Measurable A ⦄ → ⦃ Measurable B ⦄ → Measurable (A × B) +Measurable-×ˡʳ .∣_∣ (x , y) = ∣ x ∣ + ∣ y ∣ + +-- alternatives for lists +Measurable-List₀ : Measurable (List A) +Measurable-List₀ .∣_∣ = length + +Measurable-List₁ : ⦃ _ : Measurable A ⦄ → Measurable (List A) +Measurable-List₁ {A = A} .∣_∣ = go where go = λ where + [] → 1 + (x ∷ xs) → ∣ x ∣ + go xs + +-- ** well-founded recursion + +module _ ⦃ _ : Measurable A ⦄ where + + import Relation.Binary.Construct.On as On + open import Induction using (Recursor) + open import Induction.WellFounded using (WellFounded; WfRec; module All) + open import Data.Nat.Induction using (<-wellFounded) + open Nat using (_<_) + open Fun using (_on_) + + _≺_ : Rel A 0ℓ + _≺_ = _<_ on ∣_∣ + + ≺-wf : WellFounded _≺_ + ≺-wf = On.wellFounded ∣_∣ <-wellFounded + + ≺-rec : Recursor (WfRec _≺_) + ≺-rec = All.wfRec ≺-wf 0ℓ + +-- ** working with *heterogeneous* well-founded relations + +∃Measurable : Type₁ +∃Measurable = ∃ λ (A : Type) → Measurable A × A + +toMeasure : ∀ {A : Type} ⦃ _ : Measurable A ⦄ → A → ∃Measurable +toMeasure ⦃ mx ⦄ x = _ , mx , x + +instance + Measurable∃ : Measurable ∃Measurable + Measurable∃ .∣_∣ (_ , record {∣_∣ = f} , x) = f x + +_≺ᵐ_ : ∀ {A B : Type} ⦃ _ : Measurable A ⦄ ⦃ _ : Measurable B ⦄ → A → B → Type +x ≺ᵐ y = toMeasure x ≺ toMeasure y diff --git a/Class/Monad/Core.agda b/Class/Monad/Core.agda index 31dd04c..bf95d4b 100644 --- a/Class/Monad/Core.agda +++ b/Class/Monad/Core.agda @@ -11,6 +11,7 @@ record Monad (M : Type↑) : Typeω where infixr 1 _=<<_ _<=<_ field + overlap ⦃ super ⦄ : Applicative M return : A → M A _>>=_ : M A → (A → M B) → M B @@ -20,6 +21,8 @@ record Monad (M : Type↑) : Typeω where _=<<_ : (A → M B) → M A → M B f =<< c = c >>= f + _≫=_ = _>>=_; _≫_ = _>>_; _=≪_ = _=<<_ + _>=>_ : (A → M B) → (B → M C) → (A → M C) f >=> g = _=<<_ g ∘ f @@ -32,24 +35,25 @@ record Monad (M : Type↑) : Typeω where Functor-M : Functor M Functor-M = λ where ._<$>_ f x → return ∘ f =<< x - instance _ = Functor-M +open Monad ⦃...⦄ public +module _ ⦃ _ : Monad M ⦄ where mapM : (A → M B) → List A → M (List B) mapM f [] = return [] - mapM f (x ∷ xs) = do y ← f x; y ∷_ <$> mapM f xs + mapM f (x ∷ xs) = ⦇ f x ∷ mapM f xs ⦈ concatMapM : (A → M (List B)) → List A → M (List B) concatMapM f xs = concat <$> mapM f xs forM : List A → (A → M B) → M (List B) forM [] _ = return [] - forM (x ∷ xs) f = do y ← f x; y ∷_ <$> forM xs f + forM (x ∷ xs) f = ⦇ f x ∷ forM xs f ⦈ concatForM : List A → (A → M (List B)) → M (List B) concatForM xs f = concat <$> forM xs f return⊤ void : M A → M ⊤ - return⊤ k = k >> return tt + return⊤ k = k ≫ return tt void = return⊤ filterM : (A → M Bool) → List A → M (List A) @@ -58,8 +62,36 @@ record Monad (M : Type↑) : Typeω where b ← p x ((if b then [ x ] else []) ++_) <$> filterM p xs - traverseM : ⦃ Applicative M ⦄ → ⦃ Monad M ⦄ → (A → M B) → List A → M (List B) + traverseM : (A → M B) → List A → M (List B) traverseM f = λ where [] → return [] (x ∷ xs) → ⦇ f x ∷ traverseM f xs ⦈ -open Monad ⦃...⦄ public + +record MonadLaws (M : Type↑) ⦃ _ : Monad M ⦄ : Typeω where + field + >>=-identityˡ : ∀ {A : Type ℓ} {B : Type ℓ′} → + ∀ {a : A} {h : A → M B} → + (return a >>= h) ≡ h a + >>=-identityʳ : ∀ {A : Type ℓ} → + ∀ (m : M A) → + (m >>= return) ≡ m + >>=-assoc : ∀ {A : Type ℓ} {B : Type ℓ′} {C : Type ℓ″} → + ∀ (m : M A) {g : A → M B} {h : B → M C} → + ((m >>= g) >>= h) ≡ (m >>= (λ x → g x >>= h)) +open MonadLaws ⦃...⦄ public + +record Monad₀ (M : Type↑) : Typeω where + field ⦃ isMonad ⦄ : Monad M + ⦃ isApplicative₀ ⦄ : Applicative₀ M +open Monad₀ ⦃...⦄ using () public +instance + mkMonad₀ : ⦃ Monad M ⦄ → ⦃ Applicative₀ M ⦄ → Monad₀ M + mkMonad₀ = record {} + +record Monad⁺ (M : Type↑) : Typeω where + field ⦃ isMonad ⦄ : Monad M + ⦃ isAlternative ⦄ : Alternative M +open Monad⁺ ⦃...⦄ using () public +instance + mkMonad⁺ : ⦃ Monad M ⦄ → ⦃ Alternative M ⦄ → Monad⁺ M + mkMonad⁺ = record {} diff --git a/Class/Monad/Id.agda b/Class/Monad/Id.agda new file mode 100644 index 0000000..ba272f6 --- /dev/null +++ b/Class/Monad/Id.agda @@ -0,0 +1,29 @@ +-- ** Id monad. +-- Provides us with forward composition as _>=>_, +-- but might break instance-resolution/typeclass-inference + +{-# OPTIONS --cubical-compatible #-} +module Class.Monad.Id where + +open import Class.Prelude +open import Class.Functor.Core +open import Class.Applicative.Core +open import Class.Monad.Core + +Id : Type ℓ → Type ℓ +Id = id + +instance + Functor-Id : Functor Id + Functor-Id ._<$>_ = _$_ + {-# OVERLAPPABLE Functor-Id #-} + + Applicative-Id : Applicative Id + Applicative-Id .pure = id + Applicative-Id ._<*>_ = _$_ + {-# OVERLAPPABLE Applicative-Id #-} + + Monad-Id : Monad Id + Monad-Id .return = id + Monad-Id ._>>=_ = _|>_ + {-# OVERLAPPABLE Monad-Id #-} diff --git a/Class/Monad/Instances.agda b/Class/Monad/Instances.agda index b3d2d59..ef9cc21 100644 --- a/Class/Monad/Instances.agda +++ b/Class/Monad/Instances.agda @@ -2,7 +2,10 @@ module Class.Monad.Instances where open import Class.Prelude +open import Class.Functor.Core +open import Class.Applicative open import Class.Monad.Core +open import Class.Monad.Id instance Monad-TC : Monad TC @@ -19,3 +22,13 @@ instance .return → just ._>>=_ → Maybe._>>=_ where import Data.Maybe as Maybe + + MonadLaws-Maybe : MonadLaws Maybe + MonadLaws-Maybe = λ where + .>>=-identityˡ → refl + .>>=-identityʳ → λ where + (just _) → refl + nothing → refl + .>>=-assoc → λ where + (just _) → refl + nothing → refl diff --git a/Class/Monoid/Core.agda b/Class/Monoid/Core.agda index 527fed1..9f83756 100644 --- a/Class/Monoid/Core.agda +++ b/Class/Monoid/Core.agda @@ -3,22 +3,28 @@ module Class.Monoid.Core where open import Class.Prelude open import Class.Semigroup +open import Class.Setoid.Core record Monoid (A : Type ℓ) ⦃ _ : Semigroup A ⦄ : Type ℓ where field ε : A open Monoid ⦃...⦄ public module _ (A : Type ℓ) ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ where - record MonoidLaws (_≈_ : Rel A ℓ′) : Type (ℓ ⊔ ℓ′) where + + record MonoidLaws ⦃ _ : ISetoid A ⦄ : Type (ℓ ⊔ relℓ) where open Alg _≈_ field ε-identity : Identity ε _◇_ ε-identityˡ = LeftIdentity ε _◇_ ∋ ε-identity .proj₁ ε-identityʳ = RightIdentity ε _◇_ ∋ ε-identity .proj₂ - open MonoidLaws ⦃...⦄ public - MonoidLaws≡ : Type ℓ - MonoidLaws≡ = MonoidLaws _≡_ + MonoidLaws≡ : Type _ + MonoidLaws≡ = MonoidLaws + where instance _ = mkISetoid≡; _ = mkSetoidLaws≡ open MonoidLaws ⦃...⦄ public - renaming ( ε-identity to ε-identity≡ - ; ε-identityˡ to ε-identityˡ≡; ε-identityʳ to ε-identityʳ≡ ) + +module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ ⦃ _ : MonoidLaws≡ A ⦄ where + instance _ = mkISetoid≡; _ = mkSetoidLaws≡ + open MonoidLaws it public + renaming ( ε-identity to ε-identity≡ + ; ε-identityˡ to ε-identityˡ≡; ε-identityʳ to ε-identityʳ≡ ) diff --git a/Class/Monoid/Instances.agda b/Class/Monoid/Instances.agda index a293b75..7e28d84 100644 --- a/Class/Monoid/Instances.agda +++ b/Class/Monoid/Instances.agda @@ -2,6 +2,7 @@ module Class.Monoid.Instances where open import Class.Prelude +open import Class.Setoid.Core open import Class.Semigroup open import Class.Monoid.Core @@ -29,6 +30,23 @@ module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ where instance p = LeftIdentity ε _◇_ ∋ λ _ → refl q = RightIdentity ε _◇_ ∋ λ where (just _) → refl; nothing → refl +module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Semigroup B ⦄ where instance + Monoid-× : ⦃ Monoid A ⦄ → ⦃ Monoid B ⦄ → Monoid (A × B) + Monoid-× .ε = ε , ε + + MonoidLaws-× : ⦃ _ : Monoid A ⦄ ⦃ _ : Monoid B ⦄ + → ⦃ MonoidLaws≡ A ⦄ → ⦃ MonoidLaws≡ B ⦄ + → MonoidLaws≡ (A × B) + MonoidLaws-× = record {ε-identity = p , q} + where + open Alg≡ + + p : LeftIdentity (A × B ∋ ε) _◇_ + p (a , b) rewrite ε-identityˡ≡ a | ε-identityˡ≡ b = refl + + q : RightIdentity (A × B ∋ ε) _◇_ + q (a , b) rewrite ε-identityʳ≡ a | ε-identityʳ≡ b = refl + -- ** natural numbers module _ where open import Data.Nat.Properties @@ -68,7 +86,7 @@ module _ where MonoidLaws-ℤ-* = MonoidLaws≡ ℤ ∋ record {ε-identity = *-identityˡ , *-identityʳ} -- ** maybes -module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ ⦃ _ : MonoidLaws≡ A ⦄ (x : A) where +module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ ⦃ _ : ISetoid A ⦄ ⦃ _ : MonoidLaws≡ A ⦄ (x : A) where just-◇ˡ : ∀ (mx : Maybe A) → just x ◇ mx ≡ just (x ◇ fromMaybe ε mx) just-◇ˡ = λ where diff --git a/Class/MonotonePredicate.agda b/Class/MonotonePredicate.agda index ec4fb56..3c894d9 100644 --- a/Class/MonotonePredicate.agda +++ b/Class/MonotonePredicate.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --without-K #-} module Class.MonotonePredicate where -open import Class.MonotonePredicate.Core public +open import Class.MonotonePredicate.Core public diff --git a/Class/MonotonePredicate/Core.agda b/Class/MonotonePredicate/Core.agda index 34ef508..52117f8 100644 --- a/Class/MonotonePredicate/Core.agda +++ b/Class/MonotonePredicate/Core.agda @@ -1,7 +1,7 @@ +{-# OPTIONS --without-K #-} +module Class.MonotonePredicate.Core where -module Class.MonotonePredicate.Core where - -open import Class.Prelude +open import Class.Prelude hiding (trans) open import Class.HasOrder open import Relation.Unary @@ -13,9 +13,9 @@ open import Level -- relation, etc...) lives at the same level. Otherwise we couldn't -- express the (co)monadic structure of the possiblity and necessity -- modalities. -module _ {A : Type ℓ} +module _ {A : Type ℓ} ⦃ _ : HasPreorder {A = A} {_≈_ = _≡_} {ℓ} {ℓ} ⦄ where - + open IsPreorder {ℓ} ≤-isPreorder record Monotone {ℓ′} (P : Pred A ℓ′) : Type (ℓ ⊔ ℓ′ ⊔ ℓ) where @@ -30,58 +30,57 @@ module _ {A : Type ℓ} open Antitone ⦃...⦄ -- The posibility modality. One way to think about posibility is as a unary - -- version of separating conjunction. + -- version of separating conjunction. record ◇ (P : Pred A ℓ) (a : A) : Set ℓ where - constructor ◇⟨_,_⟩ + constructor ◇⟨_,_⟩ field {a′} : A ι : a′ ≤ a - px : P a′ - - open ◇ public - + px : P a′ + + open ◇ public + -- The necessity modality. In a similar spirit, we can view necessity as a unary -- version of separating implication. record □ (P : Pred A ℓ) (a : A) : Set ℓ where - constructor necessary + constructor necessary field □⟨_⟩_ : ∀ {a′} → (ι : a ≤ a′) → P a′ - - open □ public - module Operations where + open □ public - -- □ is a comonad over the category of monotone predicates over `A` + module Operations where + + -- □ is a comonad over the category of monotone predicates over `A` extract : ∀ {P} → ∀[ □ P ⇒ P ] extract px = □⟨ px ⟩ reflexive _≡_.refl - + duplicate : ∀ {P} → ∀[ □ P ⇒ □ (□ P) ] - duplicate px = necessary λ ι → necessary λ ι′ → □⟨ px ⟩ trans ι ι′ - - + duplicate px = necessary λ ι → necessary λ ι′ → □⟨ px ⟩ trans ι ι′ + + -- ◇ is a monad over the category of monotone predicates over `A`. return : ∀ {P} → ∀[ P ⇒ ◇ P ] return px = ◇⟨ reflexive _≡_.refl , px ⟩ - + join : ∀ {P} → ∀[ ◇ (◇ P) ⇒ ◇ P ] join ◇⟨ ι₁ , ◇⟨ ι₂ , px ⟩ ⟩ = ◇⟨ (trans ι₂ ι₁) , px ⟩ - + -- □ is right-adjoint to ◇ curry : ∀ {P Q} → ∀[ ◇ P ⇒ Q ] → ∀[ P ⇒ □ Q ] curry f px = necessary (λ ι → f ◇⟨ ι , px ⟩) - + uncurry : ∀ {P Q} → ∀[ P ⇒ □ Q ] → ∀[ ◇ P ⇒ Q ] uncurry f ◇⟨ ι , px ⟩ = □⟨ f px ⟩ ι - - + + -- The "Kripke exponent" (or, Kripke function space) between two predicates is -- defined as the necessity of their implication. - _⇛_ : ∀ (P Q : Pred A ℓ) → Pred A ℓ - P ⇛ Q = □ (P ⇒ Q) - - kripke-curry : {P Q R : Pred A ℓ} → ⦃ Monotone P ⦄ → ∀[ (P ∩ Q) ⇒ R ] → ∀[ P ⇒ (Q ⇛ R) ] + _⇛_ : ∀ (P Q : Pred A ℓ) → Pred A ℓ + P ⇛ Q = □ (P ⇒ Q) + + kripke-curry : {P Q R : Pred A ℓ} → ⦃ Monotone P ⦄ → ∀[ (P ∩ Q) ⇒ R ] → ∀[ P ⇒ (Q ⇛ R) ] kripke-curry f px₁ = necessary (λ i px₂ → f (weaken i px₁ , px₂)) - - kripke-uncurry : {P Q R : Pred A ℓ} → ∀[ P ⇒ (Q ⇛ R) ] → ∀[ (P ∩ Q) ⇒ R ] + + kripke-uncurry : {P Q R : Pred A ℓ} → ∀[ P ⇒ (Q ⇛ R) ] → ∀[ (P ∩ Q) ⇒ R ] kripke-uncurry f (px₁ , px₂) = □⟨ f px₁ ⟩ reflexive _≡_.refl $ px₂ - diff --git a/Class/Newtype.agda b/Class/Newtype.agda new file mode 100644 index 0000000..a7df424 --- /dev/null +++ b/Class/Newtype.agda @@ -0,0 +1,53 @@ +---------------------------------------- +-- Emulating Haskell's newtype feature. +---------------------------------------- + +{-# OPTIONS --without-K #-} +module Class.Newtype where + +open import Function.Bundles using (_↔_; mk↔) + +open import Class.Prelude +open import Class.Functor + +record newtype (A : Type ℓ) : Type ℓ where + constructor mk + field unmk : A +open newtype public + +instance + Functor-newtype : Functor newtype + Functor-newtype ._<$>_ f = mk ∘ f ∘ unmk + + mkNewtype : ⦃ A ⦄ → newtype A + mkNewtype = mk it + +mk-injective : ∀ (x y : A) → mk x ≡ mk y → x ≡ y +mk-injective _ _ refl = refl + +newtype¹ : Pred A ℓ → Pred A ℓ +newtype¹ P x = newtype (P x) + +newtype² : Rel A ℓ → Rel A ℓ +newtype² _~_ x y = newtype (x ~ y) + +newtype↔ : newtype A ↔ A +newtype↔ = mk↔ {to = unmk} $ (λ where refl → refl) , (λ where refl → refl) + +mk? : Dec A → Dec (newtype A) +mk? = mapDec mk unmk + +unmk? : Dec (newtype A) → Dec A +unmk? = mapDec unmk mk + +mk?¹ : Decidable¹ P → Decidable¹ (newtype¹ P) +mk?¹ P? x = mk? (P? x) + +unmk?¹ : Decidable¹ (newtype¹ P) → Decidable¹ P +unmk?¹ P? x = unmk? (P? x) + +mk?² : Decidable² R → Decidable² (newtype² R) +mk?² R? x y = mk? (R? x y) + +unmk?² : Decidable² (newtype² R) → Decidable² R +unmk?² R? x y = unmk? (R? x y) diff --git a/Class/Null.agda b/Class/Null.agda new file mode 100644 index 0000000..dc97046 --- /dev/null +++ b/Class/Null.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Null where + +open import Class.Prelude +open import Class.Semigroup +open import Class.Monoid +open import Class.Decidable.Core +open import Class.Decidable.Instances + +record Nullable (A : Type ℓ) {ℓ′ : Level} : Type (ℓ ⊔ lsuc ℓ′) where + field Null : Pred A ℓ′ + + ¬Null : Pred A ℓ′ + ¬Null = ¬_ ∘ Null + + module _ ⦃ _ : Null ⁇¹ ⦄ where + Null? = Decidable¹ Null ∋ dec¹; Nullᵇ = isYes ∘ Null? + ¬Null? = Decidable¹ ¬Null ∋ dec¹; ¬Nullᵇ = isYes ∘ ¬Null? +open Nullable ⦃...⦄ public + +Monoid⇒Nullable : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → Nullable A +Monoid⇒Nullable = λ where .Null → _≡ ε + +instance + Nullable-List : Nullable (List A) + Nullable-List = Monoid⇒Nullable + + Nullable-Vec : Nullable (∃ (Vec A)) + Nullable-Vec = Monoid⇒Nullable + + Nullable-String : Nullable String + Nullable-String = Monoid⇒Nullable + + Nullable-Maybe : Nullable (Maybe A) + Nullable-Maybe .Null = Mb.Is-nothing diff --git a/Class/PartialMonoid.agda b/Class/PartialMonoid.agda new file mode 100644 index 0000000..bab1505 --- /dev/null +++ b/Class/PartialMonoid.agda @@ -0,0 +1,4 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.PartialMonoid where + +open import Class.PartialMonoid.Core public diff --git a/Class/PartialMonoid/Core.agda b/Class/PartialMonoid/Core.agda new file mode 100644 index 0000000..1bc30c8 --- /dev/null +++ b/Class/PartialMonoid/Core.agda @@ -0,0 +1,49 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.PartialMonoid.Core where + +open import Class.Prelude +open import Class.Core +open import Class.Setoid.Core +open import Class.Setoid.Instances +open import Class.PartialSemigroup + +record PartialMonoid (A : Type ℓ) ⦃ _ : PartialSemigroup A ⦄ : Type ℓ where + field ε◆ : A +open PartialMonoid ⦃...⦄ public + +record PartialMonoidLaws + (A : Type ℓ) + ⦃ _ : PartialSemigroup A ⦄ + ⦃ _ : PartialMonoid A ⦄ + ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ + : Type (ℓ ⊔ relℓ {A = A}) + where + field ε◆-identity : ∀ (x : A) → (ε◆ ◆ x ≈ just x) × (x ◆ ε◆ ≈ just x) + + ε◆-identityˡ : ∀ (x : A) → ε◆ ◆ x ≈ just x + ε◆-identityˡ = proj₁ ∘ ε◆-identity + + ε◆-identityʳ : ∀ (x : A) → x ◆ ε◆ ≈ just x + ε◆-identityʳ = proj₂ ∘ ε◆-identity +open PartialMonoidLaws ⦃...⦄ public + +PartialMonoidLaws≡ : (A : Type ℓ) ⦃ _ : PartialSemigroup A ⦄ + → ⦃ PartialMonoid A ⦄ → Type ℓ +PartialMonoidLaws≡ A = PartialMonoidLaws A + where instance _ = mkISetoid≡; _ = mkSetoidLaws≡ + +open import Class.Semigroup +open import Class.Monoid + +module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ where + instance _ = Semigroup⇒Partial + Monoid⇒Partial : PartialMonoid A + Monoid⇒Partial .ε◆ = ε + instance _ = Monoid⇒Partial + + MonoidLaws⇒Partial + : ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ + → ⦃ _ : PartialSemigroupLaws A ⦄ + → ⦃ _ : MonoidLaws A ⦄ + → PartialMonoidLaws A + MonoidLaws⇒Partial .ε◆-identity _ = ε-identityˡ _ , ε-identityʳ _ diff --git a/Class/PartialSemigroup.agda b/Class/PartialSemigroup.agda new file mode 100644 index 0000000..aafc4b5 --- /dev/null +++ b/Class/PartialSemigroup.agda @@ -0,0 +1,4 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.PartialSemigroup where + +open import Class.PartialSemigroup.Core public diff --git a/Class/PartialSemigroup/Core.agda b/Class/PartialSemigroup/Core.agda new file mode 100644 index 0000000..e8ab05c --- /dev/null +++ b/Class/PartialSemigroup/Core.agda @@ -0,0 +1,53 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.PartialSemigroup.Core where + +open import Class.Prelude +open import Class.Core +open import Class.Monad +open import Class.Setoid.Core +open import Class.Setoid.Instances + +_⇀_ : Type ℓ → Type ℓ′ → Type _ +A ⇀ B = A → Maybe B + +record PartialSemigroup (A : Type ℓ) : Type ℓ where + infixr 5 _◆_ + field _◆_ : A → A ⇀ A + + infix 4 _≫◆_ _◆≪_ + _≫◆_ : Maybe A → A ⇀ A + m ≫◆ y = m >>= (_◆ y) + + _◆≪_ : A → Maybe A ⇀ A + x ◆≪ m = (x ◆_) =<< m +open PartialSemigroup ⦃...⦄ public + +record PartialSemigroupLaws + (A : Type ℓ) + ⦃ _ : PartialSemigroup A ⦄ + -- ⦃ _ : LawfulSetoid A ⦄ + ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ + : Type (ℓ ⊔ relℓ {A = A}) + where + field ◆-comm : ∀ (x y : A) → x ◆ y ≈ y ◆ x + ◆-assocʳ : ∀ (x y z : A) → (x ◆ y ≫◆ z) ≈ (x ◆≪ y ◆ z) + ◆-assocˡ : ∀ (x y z : A) → (x ◆≪ y ◆ z) ≈ (x ◆ y ≫◆ z) + ◆-assocˡ x y z = ≈-sym {x = _ ◆ _ ≫◆ _} $ ◆-assocʳ x y z +open PartialSemigroupLaws ⦃...⦄ public + +PartialSemigroupLaws≡ : (A : Type ℓ) ⦃ _ : PartialSemigroup A ⦄ → Type ℓ +PartialSemigroupLaws≡ A = PartialSemigroupLaws A + where instance _ = mkISetoid≡; _ = mkSetoidLaws≡ + +open import Class.Semigroup + +module _ ⦃ _ : Semigroup A ⦄ where + Semigroup⇒Partial : PartialSemigroup A + Semigroup⇒Partial ._◆_ = just ∘₂ _◇_ + instance _ = Semigroup⇒Partial + + SemigroupLaws⇒Partial + : ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ + → ⦃ _ : SemigroupLaws A ⦄ + → PartialSemigroupLaws A + SemigroupLaws⇒Partial = λ where .◆-comm → ◇-comm; .◆-assocʳ → ◇-assocʳ diff --git a/Class/Pointed.agda b/Class/Pointed.agda new file mode 100644 index 0000000..d33912d --- /dev/null +++ b/Class/Pointed.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Pointed where + +open import Class.Pointed.Core public +open import Class.Pointed.Instances public diff --git a/Class/Pointed/Core.agda b/Class/Pointed/Core.agda new file mode 100644 index 0000000..e513194 --- /dev/null +++ b/Class/Pointed/Core.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Pointed.Core where + +open import Class.Prelude +open import Class.Core +open import Class.Applicative.Core +open import Class.Monad.Core + +record Pointed (F : Type↑) : Typeω where + field point : ∀ {A : Type ℓ} → A → F A +open Pointed ⦃...⦄ public + +Applicative⇒Pointed : ⦃ Applicative F ⦄ → Pointed F +Applicative⇒Pointed .point = pure + +Monad⇒Pointed : ⦃ Monad F ⦄ → Pointed F +Monad⇒Pointed .point = return diff --git a/Class/Pointed/Instances.agda b/Class/Pointed/Instances.agda new file mode 100644 index 0000000..40d26c0 --- /dev/null +++ b/Class/Pointed/Instances.agda @@ -0,0 +1,13 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Pointed.Instances where + +open import Class.Prelude +open import Class.Pointed.Core +open import Class.Applicative.Instances + +instance + P-Maybe = Applicative⇒Pointed {F = Maybe} + P-List = Applicative⇒Pointed {F = List} + P-List⁺ = Applicative⇒Pointed {F = List⁺} + P-TC = Applicative⇒Pointed {F = TC} + P-Vec = λ {n} → Applicative⇒Pointed {F = flip Vec n} diff --git a/Class/Prelude.agda b/Class/Prelude.agda index c84ff05..02069ef 100644 --- a/Class/Prelude.agda +++ b/Class/Prelude.agda @@ -4,56 +4,87 @@ module Class.Prelude where open import Agda.Primitive public using () renaming (Set to Type; Setω to Typeω) open import Level public - using (Level; _⊔_) renaming (suc to lsuc) -open import Function.Base public - using (id; _∘_; _∋_; _$_; const; constᵣ; flip; it; case_of_) + using (Level; _⊔_; Lift; lift; 0ℓ) renaming (suc to lsuc) +module Fun where open import Function.Base public +open Fun public + using (id; _∘_; _∘₂_; _∋_; _$_; const; constᵣ; flip; it; case_of_; _|>_) open import Data.Empty public using (⊥; ⊥-elim) open import Data.Unit public using (⊤; tt) -open import Data.Product public +open import Data.These public + using (These; this; that; these) +open import Data.Refinement public + using (Refinement; _,_; value) +module Prod where open import Data.Product public +open Prod public using (_×_; _,_; proj₁; proj₂; Σ; ∃; ∃-syntax; -,_) -open import Data.Sum public +module Sum where open import Data.Sum public +open Sum public using (_⊎_; inj₁; inj₂) -open import Data.Bool public +module 𝔹 where open import Data.Bool public +open 𝔹 public using (Bool; true; false; not; if_then_else_; T) -open import Data.Nat public +module Nat where open import Data.Nat public; open import Data.Nat.Properties public +open Nat public using (ℕ; zero; suc) -open import Data.Fin as Fin public +module Bin where open import Data.Nat.Binary public +open Bin public + using (ℕᵇ) +module Fi where open import Data.Fin public +open Fi public using (Fin; zero; suc) -open import Data.Integer public - using (ℤ; 0ℤ; 1ℤ) -open import Data.Rational public +module Int where open import Data.Integer public +open Int public + using (ℤ; 0ℤ; 1ℤ; -_) +module Q where open import Data.Rational public +open Q public using (ℚ) -open import Data.Float public +module Fl where open import Data.Float public +open Fl public using (Float) -open import Data.Char public +module Ch where open import Data.Char public +open Ch public using (Char) -open import Data.String public +module Str where open import Data.String public +open Str public using (String) -open import Data.Maybe public +module Word where open import Data.Word64 public +open Word public + using (Word64) +module Mb where open import Data.Maybe public +open Mb public using (Maybe; just; nothing; maybe; fromMaybe) -open import Data.List public - using (List; []; _∷_; [_]; map; _++_; foldr; concat; concatMap) -open import Data.List.NonEmpty public - using (List⁺; _∷_; _⁺++⁺_; foldr₁; toList) -open import Data.Vec public +module L where open import Data.List public +open L public + using (List; []; _∷_; [_]; map; _++_; foldr; concat; concatMap; length) +module L⁺ where open import Data.List.NonEmpty public +open L⁺ public + using (List⁺; _∷_; _⁺++⁺_; foldr₁) +module V where open import Data.Vec public +open V public using (Vec; []; _∷_) -open import Data.These public - using (These; this; that; these) -open import Data.Refinement public - using (Refinement; _,_; value) + +module Meta where + open import Reflection public + open import Reflection.AST public + open import Reflection.TCM public +open Meta public + using (TC; Arg; Abs) open import Relation.Nullary public - using (¬_; Dec; yes; no; contradiction) + using (¬_; Dec; yes; no; contradiction; Irrelevant) open import Relation.Nullary.Decidable public using (⌊_⌋; dec-yes; isYes) + renaming (map′ to mapDec) open import Relation.Unary public using (Pred) renaming (Decidable to Decidable¹) open import Relation.Binary public - using (REL; Rel; DecidableEquality) + using ( REL; Rel; DecidableEquality + ; IsEquivalence; Setoid + ) renaming (Decidable to Decidable²) module _ {a b c} where 3REL : (A : Type a) (B : Type b) (C : Type c) (ℓ : Level) → Type _ @@ -62,15 +93,19 @@ module _ {a b c} where Decidable³ : ∀ {A B C ℓ} → 3REL A B C ℓ → Type _ Decidable³ _~_~_ = ∀ x y z → Dec (x ~ y ~ z) open import Relation.Binary.PropositionalEquality public - using (_≡_; refl; sym; cong; subst) - -open import Reflection public - using (TC; Arg; Abs) + using (_≡_; refl; sym; cong; subst; trans) variable ℓ ℓ′ ℓ″ ℓ‴ : Level A B C : Type ℓ + x y : A + P Q : Pred A ℓ + R R′ : Rel A ℓ + n m : ℕ module Alg (_~_ : Rel A ℓ) where open import Algebra.Definitions _~_ public module Alg≡ {ℓ} {A : Type ℓ} = Alg (_≡_ {A = A}) + +itω : ∀ {A : Typeω} → ⦃ A ⦄ → A +itω ⦃ x ⦄ = x diff --git a/Class/Semigroup/Core.agda b/Class/Semigroup/Core.agda index 6f0f8f2..0c8bcd8 100644 --- a/Class/Semigroup/Core.agda +++ b/Class/Semigroup/Core.agda @@ -2,6 +2,7 @@ module Class.Semigroup.Core where open import Class.Prelude +open import Class.Setoid.Core record Semigroup (A : Type ℓ) : Type ℓ where infixr 5 _◇_ _<>_ @@ -10,15 +11,24 @@ record Semigroup (A : Type ℓ) : Type ℓ where open Semigroup ⦃...⦄ public module _ (A : Type ℓ) ⦃ _ : Semigroup A ⦄ where - record SemigroupLaws (_≈_ : Rel A ℓ′) : Type (ℓ ⊔ ℓ′) where + record SemigroupLaws ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ : Type (ℓ ⊔ relℓ) where open Alg _≈_ field ◇-comm : Commutative _◇_ ◇-assocʳ : Associative _◇_ - open SemigroupLaws ⦃...⦄ public + + ◇-assocˡ : ∀ (x y z : A) → (x ◇ (y ◇ z)) ≈ ((x ◇ y) ◇ z) + ◇-assocˡ x y z = ≈-sym (◇-assocʳ x y z) + + instance _ = mkISetoid≡; _ = mkSetoidLaws≡ SemigroupLaws≡ : Type ℓ - SemigroupLaws≡ = SemigroupLaws _≡_ + SemigroupLaws≡ = SemigroupLaws + +open SemigroupLaws ⦃...⦄ public + +module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : SemigroupLaws≡ A ⦄ where + + instance _ = mkISetoid≡; _ = mkSetoidLaws≡ -module _ {A : Type ℓ} ⦃ _ : Semigroup A ⦄ ⦃ _ : SemigroupLaws≡ A ⦄ where - ◇-assocˡ : ∀ (x y z : A) → (x ◇ (y ◇ z)) ≡ ((x ◇ y) ◇ z) - ◇-assocˡ x y z = sym (◇-assocʳ x y z) + open SemigroupLaws it public + renaming (◇-comm to ◇-comm≡; ◇-assocʳ to ◇-assocʳ≡; ◇-assocˡ to ◇-assocˡ≡) diff --git a/Class/Semigroup/Instances.agda b/Class/Semigroup/Instances.agda index b7cf787..6322e0e 100644 --- a/Class/Semigroup/Instances.agda +++ b/Class/Semigroup/Instances.agda @@ -3,6 +3,8 @@ module Class.Semigroup.Instances where open import Class.Prelude open import Class.Semigroup.Core +open import Class.Setoid.Core +open import Class.Setoid.Instances instance Semigroup-List : Semigroup (List A) @@ -19,27 +21,60 @@ instance Semigroup-String ._◇_ = Str._++_ where import Data.String as Str - Semigroup-Maybe : ⦃ Semigroup A ⦄ → Semigroup (Maybe A) +module _ ⦃ _ : Semigroup A ⦄ where instance + Semigroup-Maybe : Semigroup (Maybe A) Semigroup-Maybe ._◇_ = λ where (just x) (just y) → just (x ◇ y) (just x) nothing → just x nothing m → m - SemigroupLaws-Maybe : ⦃ _ : Semigroup A ⦄ → ⦃ SemigroupLaws≡ A ⦄ - → SemigroupLaws≡ (Maybe A) - SemigroupLaws-Maybe {A = A} = λ where - .◇-assocʳ → λ where - (just _) (just _) (just _) → cong just (◇-assocʳ _ _ _) - (just _) (just _) nothing → refl - (just _) nothing _ → refl - nothing (just _) _ → refl - nothing nothing _ → refl - .◇-comm → λ where - (just x) (just y) → cong just (◇-comm x y) - (just _) nothing → refl - nothing (just _) → refl - nothing nothing → refl - where open Alg≡ + module _ ⦃ _ : SemigroupLaws≡ A ⦄ where instance + SemigroupLaws≡-Maybe : SemigroupLaws≡ (Maybe A) + SemigroupLaws≡-Maybe = record + { ◇-assocʳ = λ where + (just x) (just y) (just z) → cong just $ ◇-assocʳ≡ x y z + (just x) (just y) nothing → refl + (just x) nothing z → refl + nothing (just y) z → refl + nothing nothing z → refl + ; ◇-comm = λ where + (just x) (just y) → cong just $ ◇-comm≡ x y + (just x) nothing → refl + nothing (just y) → refl + nothing nothing → it + } + + module _ ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ ⦃ _ : SemigroupLaws A ⦄ where instance + SemigroupLaws-Maybe : SemigroupLaws (Maybe A) + SemigroupLaws-Maybe = record + { ◇-assocʳ = λ where + (just x) (just y) (just z) → ◇-assocʳ x y z + (just x) (just y) nothing → ≈-refl {x = x ◇ y} + (just x) nothing z → ≈-refl {x = just x ◇ z} + nothing (just y) z → ≈-refl {x = just y ◇ z} + nothing nothing z → ≈-refl {x = z} + ; ◇-comm = λ where + (just x) (just y) → ◇-comm x y + (just x) nothing → ≈-refl {x = x} + nothing (just y) → ≈-refl {x = y} + nothing nothing → lift tt + } + +module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : Semigroup B ⦄ where instance + Semigroup-× : Semigroup (A × B) + Semigroup-× ._◇_ (a , b) (a′ , b′) = (a ◇ a′ , b ◇ b′) + + SemigroupLaws-× : ⦃ SemigroupLaws≡ A ⦄ → ⦃ SemigroupLaws≡ B ⦄ + → SemigroupLaws≡ (A × B) + SemigroupLaws-× = record {◇-assocʳ = p; ◇-comm = q} + where + open Alg≡ + + p : Associative (_◇_ {A = A × B}) + p (a , b) (c , d) (e , f) rewrite ◇-assocʳ≡ a c e | ◇-assocʳ≡ b d f = refl + + q : Commutative (_◇_ {A = A × B}) + q (a , b) (c , d) rewrite ◇-comm≡ a c | ◇-comm≡ b d = refl -- ** natural numbers module _ where @@ -47,12 +82,12 @@ module _ where open import Data.Nat.Properties Semigroup-ℕ-+ = Semigroup ℕ ∋ λ where ._◇_ → _+_ - SemigroupLaws-ℕ-+ = SemigroupLaws ℕ _≡_ ∋ + SemigroupLaws-ℕ-+ = SemigroupLaws≡ ℕ ∋ record {◇-assocʳ = +-assoc; ◇-comm = +-comm} where instance _ = Semigroup-ℕ-+ Semigroup-ℕ-* = Semigroup ℕ ∋ λ where ._◇_ → _*_ - SemigroupLaws-ℕ-* = SemigroupLaws ℕ _≡_ ∋ + SemigroupLaws-ℕ-* = SemigroupLaws≡ ℕ ∋ record {◇-assocʳ = *-assoc; ◇-comm = *-comm} where instance _ = Semigroup-ℕ-* @@ -62,7 +97,7 @@ module _ where open import Data.Nat.Binary.Properties Semigroup-ℕᵇ-+ = Semigroup ℕᵇ ∋ λ where ._◇_ → _+_ - SemigroupLaws-ℕᵇ-+ = SemigroupLaws ℕᵇ _≡_ ∋ + SemigroupLaws-ℕᵇ-+ = SemigroupLaws≡ ℕᵇ ∋ record {◇-assocʳ = +-assoc; ◇-comm = +-comm} where instance _ = Semigroup-ℕᵇ-+ @@ -72,11 +107,11 @@ module _ where open import Data.Integer.Properties Semigroup-ℤ-+ = Semigroup ℤ ∋ λ where ._◇_ → _+_ - SemigroupLaws-ℤ-+ = SemigroupLaws ℤ _≡_ ∋ + SemigroupLaws-ℤ-+ = SemigroupLaws≡ ℤ ∋ record {◇-assocʳ = +-assoc; ◇-comm = +-comm} where instance _ = Semigroup-ℤ-+ Semigroup-ℤ-* = Semigroup ℤ ∋ λ where ._◇_ → _*_ - SemigroupLaws-ℤ-* = SemigroupLaws ℤ _≡_ ∋ + SemigroupLaws-ℤ-* = SemigroupLaws≡ ℤ ∋ record {◇-assocʳ = *-assoc; ◇-comm = *-comm} where instance _ = Semigroup-ℤ-* diff --git a/Class/SeparationAlgebra.agda b/Class/SeparationAlgebra.agda new file mode 100644 index 0000000..9175147 --- /dev/null +++ b/Class/SeparationAlgebra.agda @@ -0,0 +1,53 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.SeparationAlgebra where + +open import Function.Definitions using (Injective) +open import Data.Maybe using (Is-just) +open import Relation.Unary renaming (Irrelevant to Irrelevant¹) + +open import Class.Prelude +open import Class.Core + +open import Class.Setoid.Core +open import Class.Setoid.Instances +open import Class.PartialSemigroup +open import Class.PartialMonoid + +-- A separation algebra is a cancellative, partial commutative monoid (Σ, •, ε). +record SeparationAlgebra + (Σ : Type ℓ) ⦃ _ : ISetoid Σ ⦄ ⦃ _ : SetoidLaws Σ ⦄ : Type (ℓ ⊔ relℓ {A = Σ}) where + field + ⦃ ps ⦄ : PartialSemigroup Σ + ⦃ ps-laws ⦄ : PartialSemigroupLaws Σ + ⦃ pm ⦄ : PartialMonoid Σ + ⦃ pm-laws ⦄ : PartialMonoidLaws Σ + cancellative : ∀ (x : Σ) → Injective _≈_ _≈_ (x ◆_) + + -- ** induced relations + + -- "separateness" + _#_ : Rel Σ _ + x # y = Is-just (x ◆ y ) + + -- "substate" + _≼_ : Rel Σ _ + x ≼ z = ∃ λ y → (x ◆ y) ≈ just z + + -- ** predicates over Σ + ℙ : Type _ + ℙ = Pred Σ _ + + emp : ℙ + emp = _≈ ε◆ + + _∗_ : ℙ → ℙ → Pred Σ _ + (p ∗ q) σ = ∃ λ (σ₀ : Σ) → ∃ λ (σ₁ : Σ) + → (σ₀ # σ₁) + × (σ₀ ∈ p) + × (σ₁ ∈ q) + + -- ** precise predicates + Prec : Pred ℙ _ + Prec p = ∀ σ → Irrelevant¹ (λ σₚ → (σₚ ∈ p) × (σₚ ≼ σ)) + +open SeparationAlgebra ⦃...⦄ public diff --git a/Class/Setoid.agda b/Class/Setoid.agda new file mode 100644 index 0000000..c471f0f --- /dev/null +++ b/Class/Setoid.agda @@ -0,0 +1,6 @@ +{-# OPTIONS --without-K #-} +module Class.Setoid where + +open import Class.Setoid.Core public +open import Class.Setoid.Instances public +open import Class.Setoid.Dec public diff --git a/Class/Setoid/Core.agda b/Class/Setoid/Core.agda new file mode 100644 index 0000000..d3a91d5 --- /dev/null +++ b/Class/Setoid/Core.agda @@ -0,0 +1,46 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Setoid.Core where + +open import Class.Core +open import Class.Prelude + +record ISetoid (A : Type ℓ) : Typeω where + infix 4 _≈_ _≉_ + field + {relℓ} : Level + _≈_ : Rel A relℓ + + _≉_ : Rel A relℓ + x ≉ y = ¬ (x ≈ y) + + module Alg≈ = Alg _≈_ +open ISetoid ⦃...⦄ public + +record SetoidLaws (A : Type ℓ) ⦃ _ : ISetoid A ⦄ : Typeω where + field isEquivalence : IsEquivalence _≈_ + + open IsEquivalence isEquivalence public + renaming (refl to ≈-refl; sym to ≈-sym; trans to ≈-trans; reflexive to ≈-reflexive) + + mkSetoid : Setoid ℓ relℓ + mkSetoid = record {Carrier = A; _≈_ = _≈_; isEquivalence = isEquivalence} + + import Relation.Binary.Reasoning.Setoid as BinSetoid + module ≈-Reasoning = BinSetoid mkSetoid +open SetoidLaws ⦃...⦄ public + +_⟶_ : (A : Type ℓ) (B : Type ℓ′) + → ⦃ _ : ISetoid A ⦄ → ⦃ SetoidLaws A ⦄ + → ⦃ _ : ISetoid B ⦄ → ⦃ SetoidLaws B ⦄ + → Type _ +A ⟶ B = Func (mkSetoid {A = A}) (mkSetoid {A = B}) + where open import Function.Bundles + +mkISetoid≡ : ISetoid A +mkISetoid≡ = λ where + .relℓ → _ + ._≈_ → _≡_ + +mkSetoidLaws≡ : SetoidLaws A ⦃ mkISetoid≡ ⦄ +mkSetoidLaws≡ .isEquivalence = PropEq.isEquivalence + where import Relation.Binary.PropositionalEquality as PropEq diff --git a/Class/Setoid/Dec.agda b/Class/Setoid/Dec.agda new file mode 100644 index 0000000..22f64be --- /dev/null +++ b/Class/Setoid/Dec.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --without-K #-} +module Class.Setoid.Dec where + +open import Class.Prelude +open import Class.Decidable +open import Class.Setoid.Core + +DecSetoid : ∀ (A : Type ℓ) ⦃ _ : ISetoid A ⦄ → Type (ℓ ⊔ relℓ) +DecSetoid A = _≈_ {A = A} ⁇² + +module _ {A : Type ℓ} ⦃ _ : ISetoid A ⦄ ⦃ _ : DecSetoid A ⦄ where + infix 4 _≈?_ _≉?_ + _≈?_ : Decidable² _≈_ + _≈?_ = dec² + _≉?_ : Decidable² _≉_ + _≉?_ = dec² diff --git a/Class/Setoid/Instances.agda b/Class/Setoid/Instances.agda new file mode 100644 index 0000000..1f6474c --- /dev/null +++ b/Class/Setoid/Instances.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.Setoid.Instances where + +open import Class.Prelude +open import Class.Setoid.Core + +instance + Setoid-Maybe : ⦃ ISetoid A ⦄ → ISetoid (Maybe A) + Setoid-Maybe .relℓ = _ + Setoid-Maybe ._≈_ = λ where + nothing nothing → Lift _ ⊤ + nothing (just _) → Lift _ ⊥ + (just _) nothing → Lift _ ⊥ + (just x) (just y) → x ≈ y + + SetoidLaws-Maybe : ⦃ _ : ISetoid A ⦄ → ⦃ SetoidLaws A ⦄ → SetoidLaws (Maybe A) + SetoidLaws-Maybe .isEquivalence = record + { refl = λ where + {just x} → ≈-refl {x = x} + {nothing} → lift tt + ; sym = λ where + {just x} {just y} → ≈-sym {x = x}{y} + {just _} {nothing} → id + {nothing} {just _} → id + {nothing} {nothing} → id + ; trans = λ where + {just x} {just y} {just z} p q → ≈-trans {i = x}{y}{z} p q + {nothing} {nothing} {nothing} p _ → p + } diff --git a/Class/ToBool.agda b/Class/ToBool.agda index 3363cf4..b7e2bf4 100644 --- a/Class/ToBool.agda +++ b/Class/ToBool.agda @@ -5,14 +5,11 @@ open import Class.Prelude hiding (if_then_else_; ⊤; tt) open import Data.Unit.Polymorphic using (⊤; tt) open import Class.Decidable.Core -private variable - X : Type ℓ; P : X → Type ℓ - record ToBool′ (A : Type ℓ) (P 𝕋 𝔽 : A → Type ℓ′) : Type (ℓ ⊔ ℓ′) where field decide : (a : A) → ⦃ P a ⦄ → 𝕋 a ⊎ 𝔽 a infix -10 if_then_else_ - if_then_else_ : (a : A) ⦃ _ : P a ⦄ → ({𝕋 a} → X) → ({𝔽 a} → X) → X + if_then_else_ : (a : A) ⦃ _ : P a ⦄ → ({𝕋 a} → B) → ({𝔽 a} → B) → B if a then t else f = case decide a of λ where (inj₁ 𝕥) → t {𝕥} @@ -31,12 +28,12 @@ instance true → inj₁ refl false → inj₂ refl - ToBool-Dec : ToBool (Dec X) (const X) (const $ ¬ X) + ToBool-Dec : ToBool (Dec B) (const B) (const $ ¬ B) ToBool-Dec .decide = λ where (yes x) → inj₁ x (no ¬x) → inj₂ ¬x - ToBool-Maybe : ToBool (Maybe X) (const X) (const ⊤) + ToBool-Maybe : ToBool (Maybe B) (const B) (const ⊤) ToBool-Maybe .decide = λ where (just x) → inj₁ x nothing → inj₂ tt diff --git a/Class/ToList.agda b/Class/ToList.agda new file mode 100644 index 0000000..7d46e9d --- /dev/null +++ b/Class/ToList.agda @@ -0,0 +1,22 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.ToList where + +open import Class.Prelude + +record ToList (A : Type ℓ) (B : Type ℓ′) : Type (ℓ ⊔ ℓ′) where + field toList : A → List B + _∙toList = toList +open ToList ⦃...⦄ public + +instance + ToList-List : ToList (List A) A + ToList-List .toList = id + + ToList-List⁺ : ToList (List⁺ A) A + ToList-List⁺ .toList = L⁺.toList + + ToList-Str : ToList String Char + ToList-Str .toList = Str.toList + + ToList-Vec : ∀ {n} → ToList (Vec A n) A + ToList-Vec .toList = V.toList diff --git a/Class/ToN.agda b/Class/ToN.agda new file mode 100644 index 0000000..d92ee94 --- /dev/null +++ b/Class/ToN.agda @@ -0,0 +1,31 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.ToN where + +open import Class.Prelude + +record Toℕ (A : Type ℓ) : Type ℓ where + field toℕ : A → ℕ +open Toℕ ⦃...⦄ public + +open import Reflection.AST.Meta as Meta using (Meta) + +instance + Toℕ-ℕ = Toℕ ℕ ∋ λ where .toℕ → id + Toℕ-Char = Toℕ Char ∋ λ where .toℕ → Ch.toℕ + Toℕ-Word = Toℕ Word64 ∋ λ where .toℕ → Word.toℕ + Toℕ-Meta = Toℕ Meta ∋ λ where .toℕ → Meta.toℕ + + Toℕ-Fin : ∀ {n} → Toℕ (Fin n) + Toℕ-Fin .toℕ = Fi.toℕ + + import Data.List.Membership.Propositional as LMem + import Data.List.Relation.Unary.Any as LAny + + Toℕ-List∈ : ∀ {x}{xs : List A} → Toℕ (x LMem.∈ xs) + Toℕ-List∈ .toℕ = toℕ ∘ LAny.index + + import Data.Vec.Membership.Propositional as VMem + import Data.Vec.Relation.Unary.Any as VAny + + Toℕ-Vec∈ : ∀ {x}{xs : Vec A n} → Toℕ (x VMem.∈ xs) + Toℕ-Vec∈ .toℕ = toℕ ∘ VAny.index diff --git a/Class/ToZ.agda b/Class/ToZ.agda new file mode 100644 index 0000000..79b457d --- /dev/null +++ b/Class/ToZ.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.ToZ where + +open import Class.Prelude +open import Class.ToN + +record Toℤ (A : Type ℓ) : Type ℓ where + field toℤ : A → ℤ +open Toℤ ⦃...⦄ public + +instance + Toℤ-ℤ = Toℤ ℤ ∋ λ where .toℤ → id + + Toℕ⇒Toℤ : ∀ {A : Type ℓ} → ⦃ Toℕ A ⦄ → Toℤ A + Toℕ⇒Toℤ .toℤ = Int.+_ ∘ toℕ diff --git a/Class/Traversable/Core.agda b/Class/Traversable/Core.agda index cb08392..975e199 100644 --- a/Class/Traversable/Core.agda +++ b/Class/Traversable/Core.agda @@ -4,7 +4,15 @@ module Class.Traversable.Core where open import Class.Prelude open import Class.Core open import Class.Functor.Core -open import Class.Monad +open import Class.Applicative.Core +open import Class.Monad.Core + +record TraversableA (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where + field sequenceA : ⦃ Applicative M ⦄ → F (M A) → M (F A) + + traverseA : ⦃ Applicative M ⦄ → (A → M B) → F A → M (F B) + traverseA f = sequenceA ∘ fmap f +open TraversableA ⦃...⦄ public record Traversable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where field sequence : ⦃ Monad M ⦄ → F (M A) → M (F A) diff --git a/Class/Traversable/Instances.agda b/Class/Traversable/Instances.agda index cb190ac..16117da 100644 --- a/Class/Traversable/Instances.agda +++ b/Class/Traversable/Instances.agda @@ -3,20 +3,29 @@ module Class.Traversable.Instances where open import Class.Prelude open import Class.Functor +open import Class.Applicative open import Class.Monad open import Class.Traversable.Core instance - Traversable-Maybe : Traversable Maybe - Traversable-Maybe .sequence = λ where - nothing → return nothing - (just x) → x >>= return ∘ just + TraversableA-Maybe : TraversableA Maybe + TraversableA-Maybe .sequenceA = λ where + nothing → ⦇ nothing ⦈ + (just x) → ⦇ just x ⦈ - Traversable-List : Traversable List - Traversable-List .sequence = go - where go = λ where - [] → return [] - (m ∷ ms) → do x ← m; xs ← go ms; return (x ∷ xs) + TraversableM-Maybe : Traversable Maybe + TraversableM-Maybe .sequence = sequenceA - Traversable-List⁺ : Traversable List⁺ - Traversable-List⁺ .sequence (m ∷ ms) = do x ← m; xs ← sequence ms; return (x ∷ xs) + TraversableA-List : TraversableA List + TraversableA-List .sequenceA = go where go = λ where + [] → ⦇ [] ⦈ + (m ∷ ms) → ⦇ m ∷ go ms ⦈ + + TraversableM-List : Traversable List + TraversableM-List .sequence = sequenceA + + TraversableA-List⁺ : TraversableA List⁺ + TraversableA-List⁺ .sequenceA (m ∷ ms) = ⦇ m ∷ sequenceA ms ⦈ + + TraversableM-List⁺ : Traversable List⁺ + TraversableM-List⁺ .sequence = sequenceA diff --git a/Class/View.agda b/Class/View.agda new file mode 100644 index 0000000..2f2fb62 --- /dev/null +++ b/Class/View.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --cubical-compatible #-} +module Class.View where + +open import Class.Prelude + +record _▷_ (A : Type ℓ) (B : Type ℓ′) : Type (ℓ ⊔ ℓ′) where + field + view : A → B + unview : B → A + unview∘view : ∀ x → unview (view x) ≡ x + view∘unview : ∀ y → view (unview y) ≡ y + +open _▷_ ⦃...⦄ public + +view_as_ : A → (B : Type ℓ′) ⦃ _ : A ▷ B ⦄ → B +view x as B = view {B = B} x diff --git a/Test/Allable.agda b/Test/Allable.agda new file mode 100644 index 0000000..8f91e45 --- /dev/null +++ b/Test/Allable.agda @@ -0,0 +1,18 @@ +module Test.Allable where + +open import Class.Prelude +open import Class.Allable +open import Class.Decidable +open import Class.HasOrder + +_ : ∀[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0 +_ = auto + +_ : ∀[ x ∈ just 42 ] x > 0 +_ = auto + +_ : ∀[ x ∈ nothing ] x > 0 +_ = auto + +_ : ¬∀[ x ∈ just 0 ] x > 0 +_ = auto diff --git a/Test/Anyable.agda b/Test/Anyable.agda new file mode 100644 index 0000000..4e33da0 --- /dev/null +++ b/Test/Anyable.agda @@ -0,0 +1,15 @@ +module Test.Anyable where + +open import Class.Prelude +open import Class.Anyable +open import Class.Decidable +open import Class.HasOrder + +_ : ∃[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0 +_ = auto + +_ : ∃[ x ∈ just 42 ] x > 0 +_ = auto + +_ : ∄[ x ∈ nothing ] x > 0 +_ = auto diff --git a/Test/Coercions.agda b/Test/Coercions.agda new file mode 100644 index 0000000..76ff9ab --- /dev/null +++ b/Test/Coercions.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --cubical-compatible #-} +module Test.Coercions where + +open import Class.Prelude +open import Class.Coercions + +𝟚 = ⊤ ⊎ ⊤ +pattern 𝕃 = inj₁ tt; pattern ℝ = inj₂ tt + +instance + ↝Bool : 𝟚 ↝ Bool + ↝Bool .to = λ where + 𝕃 → true + ℝ → false + + Bool↝ : Bool ↝ 𝟚 + Bool↝ .to = λ where + true → 𝕃 + false → ℝ + +_ : Bool +_ = to 𝕃 + +_ : 𝟚 +_ = to true + +_ : Bool → Bool +_ = not ∘ to[ Bool ] ∘ to[ 𝟚 ] diff --git a/Test/Decidable.agda b/Test/Decidable.agda index cad1203..68204a3 100644 --- a/Test/Decidable.agda +++ b/Test/Decidable.agda @@ -1,9 +1,10 @@ -{-# OPTIONS --without-K #-} +{-# OPTIONS --with-K #-} module Test.Decidable where open import Class.Prelude open import Class.Decidable open import Class.DecEq +open import Class.DecEq.WithK module _ {ℓ} {A : Type ℓ} where open import Data.Maybe @@ -22,9 +23,61 @@ open import Data.List.Membership.Propositional using (_∈_; _∉_) 0⋯2 = List ℕ ∋ 0 ∷ 1 ∷ 2 ∷ [] +open import Data.Nat using (_∸_) +open import Class.Anyable + _ = 1 ∈ 0⋯2 ∋ auto _ = 3 ∉ 0⋯2 ∋ auto f = (3 ∈ 0⋯2 → 2 ≡ 3) ∋ contradict + +_ = (¬ ¬ ((true , true) ≡ (true , true))) + × (8 ≡ 18 ∸ 10) + ∋ auto + +_ = ¬ ( (¬ ¬ ((true , true) ≡ (true , true))) + × (8 ≡ 17 ∸ 10) ) + ∋ auto + +_ : ∀ {A : Type ℓ} + → ⦃ DecEq A ⦄ + → {m : Maybe (List A)} {x₁ x₂ : A} + → Dec $ Any (λ xs → (xs ≡ (x₁ ∷ x₂ ∷ [])) ⊎ Any (const ⊤) xs) m +_ = dec + +module NonDependentRecords where + record Valid : Type where + constructor _,_ + field p₁ : ¬ ( (¬ ¬ (true ≡ true)) + × (8 ≡ 17 ∸ 10) ) + p₂ : (¬ ¬ (true ≡ true)) + × (8 ≡ 18 ∸ 10) + open Valid + + t : Valid ⁇ + t .dec + with dec + ... | no ¬p₁ = no (¬p₁ ∘ p₁) + ... | yes p₁ + with dec + ... | no ¬p₂ = no (¬p₂ ∘ p₂) + ... | yes p₂ = yes (p₁ , p₂) + +module SimpleDependentRecords where + record Valid : Type where + constructor _,_ + field p₁ : ⊤ + p₂ : ¬ ( (¬ ¬ (tt ≡ p₁)) + × (8 ≡ 17 ∸ 10) ) + open Valid + + t : Valid ⁇ + t .dec + with dec + ... | no ¬p₁ = no (¬p₁ ∘ p₁) + ... | yes p₁ + with dec + ... | no ¬p₂ = no λ where (p₁ , p₂) → ¬p₂ p₂ + ... | yes p₂ = yes (p₁ , p₂) diff --git a/Test/HasMembership.agda b/Test/HasMembership.agda new file mode 100644 index 0000000..012eb17 --- /dev/null +++ b/Test/HasMembership.agda @@ -0,0 +1,13 @@ +{-# OPTIONS --cubical-compatible #-} +module Test.HasMembership where + +open import Class.Prelude +open import Class.HasMembership +open import Class.ToN + +_ = mapWith∈ (List ℕ ∋ 10 ∷ 20 ∷ 30 ∷ []) toℕ + ≡ (0 ∷ 1 ∷ 2 ∷ []) + ∋ refl +_ = mapWith∈ (Vec ℕ 3 ∋ 10 ∷ 20 ∷ 30 ∷ []) toℕ + ≡ (0 ∷ 1 ∷ 2 ∷ []) + ∋ refl diff --git a/Test/Measurable.agda b/Test/Measurable.agda new file mode 100644 index 0000000..feb113e --- /dev/null +++ b/Test/Measurable.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --without-K #-} +module Test.Measurable where + +open import Class.Prelude +open Nat +open import Class.Measurable + +instance _ = Measurable-List₁ + +-- ** make sure we can differentiate between ∣ [] ∣ and ∣ [ [] ] ∣ + +∣xs∣>0 : ∀ ⦃ _ : Measurable A ⦄ (xs : List A) → + ∣ xs ∣ > 0 +∣xs∣>0 [] = s≤s z≤n +∣xs∣>0 (x ∷ xs) with ∣ x ∣ +... | 0 = ∣xs∣>0 xs +... | suc _ = s≤s z≤n + +≺ᵐ-∷ : ⦃ _ : Measurable A ⦄ (x : A) (xs : List A) → + x ≺ᵐ (x ∷ xs) +≺ᵐ-∷ x xs = Nat.m0 xs) + +-- ** example well-founded recursion on naturals +-- +-- NB: termination fails if the recursive argument is not structurally smaller, e.g. +-- +-- binSearch : ℕ → ℕ +-- binSearch 0 = 0 +-- binSearch n = f ⌊ n /2⌋ + +binSearch : ℕ → ℕ +binSearch = ≺-rec _ λ where + zero _ → 0 + (suc n) r → r (s≤s $ /2-less n) + where + /2-less : ∀ n → ⌊ n /2⌋ ≤ n + /2-less = λ where + zero → z≤n + (suc zero) → z≤n + (suc (suc n)) → s≤s $ ≤-trans (/2-less n) (n≤1+n _) diff --git a/Test/Monad.agda b/Test/Monad.agda new file mode 100644 index 0000000..363cc1a --- /dev/null +++ b/Test/Monad.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --cubical-compatible #-} +module Test.Monad where + +open import Class.Prelude +open import Class.Core +open import Class.Monad +-- open import Class.Monad.Id -- breaks instance resolution + +_ = (return 5 >>= just) ≡ just 5 + ∋ refl +_ = (return 5 >>= just) ≡ just 5 + ∋ >>=-identityʳ _ + +_ : Monad Maybe +_ = itω + +_ : MonadLaws Maybe +_ = itω + +_ : ⦃ _ : Monad M ⦄ → (ℕ → M ℕ) +_ = return diff --git a/Test/Newtype.agda b/Test/Newtype.agda new file mode 100644 index 0000000..24fc830 --- /dev/null +++ b/Test/Newtype.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --without-K #-} +module Test.Newtype where + +open import Class.Prelude +open import Class.Newtype +open import Class.Functor + +ℕ˘ = newtype ℕ + +_+˘_ : ℕ˘ → ℕ˘ → ℕ˘ +n +˘ m = case unmk m of λ where + 0 → n + (suc m′) → suc <$> (n +˘ mk m′) + ++˘-identityˡ : ∀ x → mk 0 +˘ x ≡ x ++˘-identityˡ (mk 0) = refl ++˘-identityˡ (mk (suc n)) rewrite +˘-identityˡ (mk n) = refl + +H˘ : ∀ {n : ℕ˘} → n +˘ mk 0 ≡ n +H˘ = refl + +H˘′ : ∀ {n : ℕ} → mk n +˘ mk 0 ≡ mk n +H˘′ = H˘ + +open Nat using (_+_) + ++↔+˘ : ∀ (x y : ℕ) → x + y ≡ (mk x +˘ mk y) .unmk ++↔+˘ zero y rewrite +˘-identityˡ (mk y) = refl ++↔+˘ (suc x) zero = cong suc $ Nat.+-identityʳ x ++↔+˘ (suc x) (suc y) = cong suc $ trans (Nat.+-suc x y) (+↔+˘ (suc x) y) + +_ : ∀ {n : ℕ} → n + 0 ≡ n +_ = trans (+↔+˘ _ 0) (cong unmk H˘′) + +-- T0D0: tactic to automate "newtype" transports diff --git a/Test/View.agda b/Test/View.agda new file mode 100644 index 0000000..42286cd --- /dev/null +++ b/Test/View.agda @@ -0,0 +1,51 @@ +{-# OPTIONS --with-K #-} +module Test.View where + +open import Class.Prelude +open import Class.View + +data SnocList (A : Type ℓ) : Type ℓ where + [] : SnocList A + _∷_ : SnocList A → A → SnocList A + +_∷ˡ_ : A → SnocList A → SnocList A +x ∷ˡ [] = [] ∷ x +x ∷ˡ (xs ∷ y) = (x ∷ˡ xs) ∷ y + +snocView : List A → SnocList A +snocView = λ where + [] → [] + (x ∷ xs) → x ∷ˡ snocView xs + +snocUnview : SnocList A → List A +snocUnview = λ where + [] → [] + (xs ∷ x) → snocUnview xs L.∷ʳ x + +snocUnview-∷ˡ : ∀ (x : A) xs → snocUnview (x ∷ˡ xs) ≡ x ∷ snocUnview xs +snocUnview-∷ˡ _ [] = refl +snocUnview-∷ˡ x (xs ∷ _) rewrite snocUnview-∷ˡ x xs = refl + +snocView-∷ʳ : ∀ (x : A) xs → snocView (xs L.∷ʳ x) ≡ snocView xs ∷ x +snocView-∷ʳ _ [] = refl +snocView-∷ʳ x (_ ∷ xs) rewrite snocView-∷ʳ x xs = refl + +instance + SnocView : List A ▷ SnocList A + SnocView .view = snocView + SnocView .unview = snocUnview + SnocView .unview∘view [] = refl + SnocView .unview∘view (x ∷ xs) + rewrite snocUnview-∷ˡ x (view xs) + | unview∘view xs + = refl + SnocView .view∘unview [] = refl + SnocView .view∘unview (xs ∷ x) + rewrite snocView-∷ʳ x (unview xs) + | view∘unview xs + = refl + +last : List A → Maybe A +last xs with view xs as SnocList _ +... | [] = nothing +... | _ ∷ x = just x diff --git a/standard-library-classes.agda b/standard-library-classes.agda index 0916026..5370942 100644 --- a/standard-library-classes.agda +++ b/standard-library-classes.agda @@ -1,35 +1,52 @@ {-# OPTIONS --with-K #-} module standard-library-classes where +open import Class.Prelude +open import Class.Newtype; import Test.Newtype + -- ** Algebraic structures +open import Class.Setoid public open import Class.Semigroup public -open import Class.Monoid public +open import Class.Monoid public; import Test.Monoid open import Class.CommutativeMonoid public -open import Class.Functor public +open import Class.Functor public; import Test.Functor open import Class.Bifunctor public open import Class.Applicative public -open import Class.Monad public +open import Class.Monad public; import Class.Monad.Id; import Test.Monad open import Class.Foldable public open import Class.Traversable public +open import Class.Pointed public +open import Class.Group public +open import Class.PartialSemigroup public +open import Class.PartialMonoid public +open import Class.SeparationAlgebra public -- ** Decidability -open import Class.DecEq public +open import Class.DecEq public; import Test.DecEq open import Class.DecEq.WithK public -open import Class.Decidable public +open import Class.Decidable public; import Test.Decidable --- ** Others -open import Class.Allable public -open import Class.Anyable public -open import Class.Default public +-- ** Conversions +open import Class.ToBool public +open import Class.ToList public +open import Class.FromList public +open import Class.ToN public +open import Class.FromN public +open import Class.ToZ public +open import Class.Coercions public; import Test.Coercions + +-- ** Overloading notation +open import Class.Allable public; import Test.Allable +open import Class.Anyable public; import Test.Anyable open import Class.HasAdd public open import Class.HasOrder public -open import Class.Show public -open import Class.ToBool public -open import Class.MonotonePredicate public +open import Class.HasMembership public; import Test.HasMembership --- ** Tests -open import Test.Monoid -open import Test.Functor -open import Test.DecEq -open import Test.Decidable -open import Test.Show +-- ** Others +open import Class.Default public +open import Class.Show public; import Test.Show +open import Class.MonotonePredicate public +open import Class.Default public +open import Class.Measurable public; import Test.Measurable +open import Class.Null public +open import Class.View public; import Test.View