From c150309992d509d44997eb9dc38dc7e19b75cbee Mon Sep 17 00:00:00 2001 From: whatisRT Date: Thu, 28 Nov 2024 15:33:31 +0100 Subject: [PATCH 1/2] Change `Monad` polymorphism Monads don't need to work at all levels anymore, and can have a different level for their result type. --- Class/Applicative/Core.agda | 6 +++--- Class/Applicative/Instances.agda | 25 +++++++++++++------------ Class/Foldable/Core.agda | 2 +- Class/Foldable/Instances.agda | 4 +++- Class/Functor/Core.agda | 6 +++--- Class/Functor/Instances.agda | 24 +++++++++++++----------- Class/Monad/Core.agda | 27 ++++++++++++++++++--------- Class/Monad/Instances.agda | 8 +++++--- Class/Monoid/Core.agda | 4 ++++ Class/Traversable/Core.agda | 4 ++-- Class/Traversable/Instances.agda | 8 +++++--- 11 files changed, 70 insertions(+), 48 deletions(-) diff --git a/Class/Applicative/Core.agda b/Class/Applicative/Core.agda index 93649ef..5740212 100644 --- a/Class/Applicative/Core.agda +++ b/Class/Applicative/Core.agda @@ -5,7 +5,7 @@ open import Class.Prelude open import Class.Core open import Class.Functor.Core -record Applicative (F : Type↑) : Typeω where +record Applicative {a b} (F : Type a → Type b) : Type (lsuc (a ⊔ b)) where infixl 4 _<*>_ _⊛_ _<*_ _<⊛_ _*>_ _⊛>_ infix 4 _⊗_ @@ -34,13 +34,13 @@ record Applicative (F : Type↑) : Typeω where open Applicative ⦃...⦄ public -record Applicative₀ (F : Type↑) : Typeω where +record Applicative₀ {a b} (F : Type a → Type b) : Type (lsuc (a ⊔ b)) where field overlap ⦃ super ⦄ : Applicative F ε₀ : F A open Applicative₀ ⦃...⦄ public -record Alternative (F : Type↑) : Typeω where +record Alternative {a b} (F : Type a → Type b) : Type (lsuc (a ⊔ b)) where infixr 3 _<|>_ field _<|>_ : F A → F A → F A open Alternative ⦃...⦄ public diff --git a/Class/Applicative/Instances.agda b/Class/Applicative/Instances.agda index 365871c..54533bb 100644 --- a/Class/Applicative/Instances.agda +++ b/Class/Applicative/Instances.agda @@ -6,44 +6,45 @@ open import Class.Functor.Core open import Class.Functor.Instances open import Class.Applicative.Core +private variable a : Level + instance - Applicative-Maybe : Applicative Maybe + Applicative-Maybe : Applicative {a} Maybe Applicative-Maybe = λ where .pure → just ._<*>_ → maybe fmap (const nothing) - Applicative₀-Maybe : Applicative₀ Maybe + Applicative₀-Maybe : Applicative₀ {a} Maybe Applicative₀-Maybe .ε₀ = nothing - Alternative-Maybe : Alternative Maybe + Alternative-Maybe : Alternative {a} Maybe Alternative-Maybe ._<|>_ = May._<∣>_ where import Data.Maybe as May - Applicative-List : Applicative List + Applicative-List : Applicative {a} List Applicative-List = λ where .pure → [_] ._<*>_ → flip $ concatMap ∘ _<&>_ - Applicative₀-List : Applicative₀ List + Applicative₀-List : Applicative₀ {a} List Applicative₀-List .ε₀ = [] - Alternative-List : Alternative List + Alternative-List : Alternative {a} List Alternative-List ._<|>_ = _++_ - Applicative-List⁺ : Applicative List⁺ + Applicative-List⁺ : Applicative {a} List⁺ Applicative-List⁺ = λ where .pure → L⁺.[_] ._<*>_ → flip $ L⁺.concatMap ∘ _<&>_ where import Data.List.NonEmpty as L⁺ - Applicative-Vec : ∀ {n} → Applicative (flip Vec n) + Applicative-Vec : ∀ {n} → Applicative {a} (flip Vec n) Applicative-Vec = λ where .pure → V.replicate _ ._<*>_ → V._⊛_ where import Data.Vec as V - - Applicative₀-Vec : Applicative₀ (flip Vec 0) + Applicative₀-Vec : Applicative₀ {a} (flip Vec 0) Applicative₀-Vec .ε₀ = [] -- Applicative-∃Vec : Applicative (∃ ∘ Vec) @@ -55,8 +56,8 @@ instance open import Reflection.TCM.Syntax public open import Reflection.TCM public - Alternative-TC : Alternative TC + Alternative-TC : Alternative {a} TC Alternative-TC = record {M} - Applicative-TC : Applicative TC + Applicative-TC : Applicative {a} TC Applicative-TC = record {M} diff --git a/Class/Foldable/Core.agda b/Class/Foldable/Core.agda index d72fd68..8eff5d6 100644 --- a/Class/Foldable/Core.agda +++ b/Class/Foldable/Core.agda @@ -7,6 +7,6 @@ open import Class.Functor open import Class.Semigroup open import Class.Monoid -record Foldable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where +record Foldable {a b} (F : Type a → Type b) ⦃ _ : Functor F ⦄ : Type (lsuc (a ⊔ b)) where field fold : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A open Foldable ⦃...⦄ public diff --git a/Class/Foldable/Instances.agda b/Class/Foldable/Instances.agda index 16580bf..3664bdf 100644 --- a/Class/Foldable/Instances.agda +++ b/Class/Foldable/Instances.agda @@ -7,8 +7,10 @@ open import Class.Semigroup open import Class.Monoid open import Class.Foldable.Core +private variable a : Level + instance - Foldable-List : Foldable List + Foldable-List : Foldable {a} List Foldable-List .fold = go where go = λ where [] → ε (x ∷ []) → x diff --git a/Class/Functor/Core.agda b/Class/Functor/Core.agda index 61a9579..184869a 100644 --- a/Class/Functor/Core.agda +++ b/Class/Functor/Core.agda @@ -6,7 +6,7 @@ open import Class.Core private variable a b c : Level -record Functor (F : Type↑) : Typeω where +record Functor (F : Type a → Type b) : Type (lsuc (a ⊔ b)) where infixl 4 _<$>_ _<$_ infixl 1 _<&>_ @@ -20,13 +20,13 @@ record Functor (F : Type↑) : Typeω where _<&>_ = flip _<$>_ open Functor ⦃...⦄ public -record FunctorLaws (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where +record FunctorLaws (F : Type a → Type b) ⦃ _ : Functor F ⦄ : Type (lsuc (a ⊔ b)) where field -- preserves identity morphisms fmap-id : ∀ {A : Type a} (x : F A) → fmap id x ≡ x -- preserves composition of morphisms - fmap-∘ : ∀ {A : Type a} {B : Type b} {C : Type c} + fmap-∘ : ∀ {A B C : Type a} {f : B → C} {g : A → B} (x : F A) → fmap (f ∘ g) x ≡ (fmap f ∘ fmap g) x open FunctorLaws ⦃...⦄ public diff --git a/Class/Functor/Instances.agda b/Class/Functor/Instances.agda index 1649192..b25f30c 100644 --- a/Class/Functor/Instances.agda +++ b/Class/Functor/Instances.agda @@ -4,20 +4,22 @@ module Class.Functor.Instances where open import Class.Prelude open import Class.Functor.Core +private variable a : Level + instance - Functor-Maybe : Functor Maybe + Functor-Maybe : Functor {a} Maybe Functor-Maybe = record {M} where import Data.Maybe as M renaming (map to _<$>_) - FunctorLaws-Maybe : FunctorLaws Maybe + FunctorLaws-Maybe : FunctorLaws {a} Maybe FunctorLaws-Maybe = λ where .fmap-id → λ where (just _) → refl; nothing → refl .fmap-∘ → λ where (just _) → refl; nothing → refl - Functor-List : Functor List + Functor-List : Functor {a} List Functor-List ._<$>_ = map - FunctorLaws-List : FunctorLaws List + FunctorLaws-List : FunctorLaws {a} List FunctorLaws-List = record {fmap-id = p; fmap-∘ = q} where p : ∀ {A : Type ℓ} (x : List A) → fmap id x ≡ x @@ -25,31 +27,31 @@ instance [] → refl (x ∷ xs) → cong (x ∷_) (p xs) - q : ∀ {A : Type ℓ} {B : Type ℓ′} {C : Type ℓ″} {f : B → C} {g : A → B} (x : List A) → + q : ∀ {A B C : Type ℓ} {f : B → C} {g : A → B} (x : List A) → fmap (f ∘ g) x ≡ (fmap f ∘ fmap g) x q {f = f}{g} = λ where [] → refl (x ∷ xs) → cong (f (g x) ∷_) (q xs) - Functor-List⁺ : Functor List⁺ + Functor-List⁺ : Functor {a} List⁺ Functor-List⁺ = record {L} where import Data.List.NonEmpty as L renaming (map to _<$>_) - Functor-Vec : ∀ {n} → Functor (flip Vec n) + Functor-Vec : ∀ {n} → Functor {a} (flip Vec n) Functor-Vec = record {V} where import Data.Vec as V renaming (map to _<$>_) - Functor-TC : Functor TC + Functor-TC : Functor {a} TC Functor-TC = record {R} where import Reflection.TCM.Syntax as R - Functor-Abs : Functor Abs + Functor-Abs : Functor {a} Abs Functor-Abs = record {R} where import Reflection.AST.Abstraction as R renaming (map to _<$>_) - Functor-Arg : Functor Arg + Functor-Arg : Functor {a} Arg Functor-Arg = record {R} where import Reflection.AST.Argument as R renaming (map to _<$>_) - Functor-∃Vec : Functor (∃ ∘ Vec) + Functor-∃Vec : Functor {a} (∃ ∘ Vec) Functor-∃Vec ._<$>_ f (_ , xs) = -, (f <$> xs) diff --git a/Class/Monad/Core.agda b/Class/Monad/Core.agda index 31dd04c..e14ebcf 100644 --- a/Class/Monad/Core.agda +++ b/Class/Monad/Core.agda @@ -6,7 +6,7 @@ open import Class.Core open import Class.Functor open import Class.Applicative -record Monad (M : Type↑) : Typeω where +record Monad {a b} (M : Type a → Type b) : Type (lsuc (a ⊔ b)) where infixl 1 _>>=_ _>>_ _>=>_ infixr 1 _=<<_ _<=<_ @@ -26,9 +26,6 @@ record Monad (M : Type↑) : Typeω where _<=<_ : (B → M C) → (A → M B) → (A → M C) g <=< f = f >=> g - join : M (M A) → M A - join m = m >>= id - Functor-M : Functor M Functor-M = λ where ._<$>_ f x → return ∘ f =<< x @@ -48,6 +45,19 @@ record Monad (M : Type↑) : Typeω where concatForM : List A → (A → M (List B)) → M (List B) concatForM xs f = concat <$> forM xs f + traverseM : ⦃ Applicative M ⦄ → ⦃ Monad M ⦄ → (A → M B) → List A → M (List B) + traverseM f = λ where + [] → return [] + (x ∷ xs) → ⦇ f x ∷ traverseM f xs ⦈ + + _<$₂>_,_ : (A → B → C) → M A → M B → M C + f <$₂> x , y = do x ← x; y ← y; return (f x y) +open Monad ⦃...⦄ public + +join : ∀ {a} {M : Type a → Type a} ⦃ _ : Monad M ⦄ {A : Type a} → M (M A) → M A +join m = m >>= id + +module _ {a} {M : Type → Type a} ⦃ _ : Monad M ⦄ {A : Type} where return⊤ void : M A → M ⊤ return⊤ k = k >> return tt void = return⊤ @@ -57,9 +67,8 @@ record Monad (M : Type↑) : Typeω where filterM p (x ∷ xs) = do b ← p x ((if b then [ x ] else []) ++_) <$> filterM p xs + where instance _ = Functor-M - traverseM : ⦃ Applicative M ⦄ → ⦃ Monad M ⦄ → (A → M B) → List A → M (List B) - traverseM f = λ where - [] → return [] - (x ∷ xs) → ⦇ f x ∷ traverseM f xs ⦈ -open Monad ⦃...⦄ public + infix 0 mif_then_ + mif_then_ : Bool → M ⊤ → M ⊤ + mif b then x = if b then x else return _ diff --git a/Class/Monad/Instances.agda b/Class/Monad/Instances.agda index b3d2d59..3f1845f 100644 --- a/Class/Monad/Instances.agda +++ b/Class/Monad/Instances.agda @@ -4,17 +4,19 @@ module Class.Monad.Instances where open import Class.Prelude open import Class.Monad.Core +private variable a : Level + instance - Monad-TC : Monad TC + Monad-TC : Monad {a} TC Monad-TC = record {R} where import Reflection as R renaming (pure to return) - Monad-List : Monad List + Monad-List : Monad {a} List Monad-List = λ where .return → _∷ [] ._>>=_ → flip concatMap - Monad-Maybe : Monad Maybe + Monad-Maybe : Monad {a} Maybe Monad-Maybe = λ where .return → just ._>>=_ → Maybe._>>=_ diff --git a/Class/Monoid/Core.agda b/Class/Monoid/Core.agda index 527fed1..28d12e1 100644 --- a/Class/Monoid/Core.agda +++ b/Class/Monoid/Core.agda @@ -22,3 +22,7 @@ module _ (A : Type ℓ) ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ where open MonoidLaws ⦃...⦄ public renaming ( ε-identity to ε-identity≡ ; ε-identityˡ to ε-identityˡ≡; ε-identityʳ to ε-identityʳ≡ ) + +mconcat : {M : Type ℓ} → ⦃ _ : Semigroup M ⦄ → ⦃ Monoid M ⦄ -> List M -> M +mconcat [] = ε +mconcat (x ∷ l) = x ◇ mconcat l diff --git a/Class/Traversable/Core.agda b/Class/Traversable/Core.agda index cb08392..5cf3f02 100644 --- a/Class/Traversable/Core.agda +++ b/Class/Traversable/Core.agda @@ -6,8 +6,8 @@ open import Class.Core open import Class.Functor.Core open import Class.Monad -record Traversable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where - field sequence : ⦃ Monad M ⦄ → F (M A) → M (F A) +record Traversable {a} (F : Type a → Type a) ⦃ _ : Functor F ⦄ : Type (lsuc a) where + field sequence : {M : Type a → Type a} → ⦃ Monad M ⦄ → F (M A) → M (F A) traverse : ⦃ Monad M ⦄ → (A → M B) → F A → M (F B) traverse f = sequence ∘ fmap f diff --git a/Class/Traversable/Instances.agda b/Class/Traversable/Instances.agda index cb190ac..2ebca3e 100644 --- a/Class/Traversable/Instances.agda +++ b/Class/Traversable/Instances.agda @@ -6,17 +6,19 @@ open import Class.Functor open import Class.Monad open import Class.Traversable.Core +private variable a : Level + instance - Traversable-Maybe : Traversable Maybe + Traversable-Maybe : Traversable {a} Maybe Traversable-Maybe .sequence = λ where nothing → return nothing (just x) → x >>= return ∘ just - Traversable-List : Traversable List + Traversable-List : Traversable {a} List Traversable-List .sequence = go where go = λ where [] → return [] (m ∷ ms) → do x ← m; xs ← go ms; return (x ∷ xs) - Traversable-List⁺ : Traversable List⁺ + Traversable-List⁺ : Traversable {a} List⁺ Traversable-List⁺ .sequence (m ∷ ms) = do x ← m; xs ← sequence ms; return (x ∷ xs) From a5afcf84885c4f76d143ce29722555ba93cb58d2 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Thu, 27 Mar 2025 14:20:28 +0100 Subject: [PATCH 2/2] Add `Monad-Sum` --- Class/Monad/Instances.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Class/Monad/Instances.agda b/Class/Monad/Instances.agda index 3f1845f..b054b6c 100644 --- a/Class/Monad/Instances.agda +++ b/Class/Monad/Instances.agda @@ -21,3 +21,9 @@ instance .return → just ._>>=_ → Maybe._>>=_ where import Data.Maybe as Maybe + + Monad-Sum : Monad {a} (A ⊎_) + Monad-Sum = λ where + .return → inj₂ + ._>>=_ (inj₁ x) f → inj₁ x + ._>>=_ (inj₂ y) f → f y