From dc5972438b06fb8321343315547999aa348dc969 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Mon, 14 Apr 2025 17:31:00 +0100 Subject: [PATCH] Change `Monad` polymorphism --- Class/Applicative/Core.agda | 6 ++-- Class/Bifunctor.agda | 15 ++++----- Class/Core.agda | 30 +++++++++++++---- Class/Foldable/Core.agda | 2 +- Class/Functor/Core.agda | 4 +-- Class/Monad/Core.agda | 2 +- Class/Monad/Instances.agda | 12 +++++++ Class/Traversable/Core.agda | 2 +- Test/Functor.agda | 6 ++++ Test/Monad.agda | 62 +++++++++++++++++++++++++++++++++++ Test/Reflection.agda | 9 +++++ standard-library-classes.agda | 4 ++- 12 files changed, 130 insertions(+), 24 deletions(-) create mode 100644 Test/Monad.agda create mode 100644 Test/Reflection.agda diff --git a/Class/Applicative/Core.agda b/Class/Applicative/Core.agda index 93649ef..49c3042 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 (F : Type↑ ℓ↑) : Typeω 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₀ (F : Type↑ ℓ↑) : Typeω where field overlap ⦃ super ⦄ : Applicative F ε₀ : F A open Applicative₀ ⦃...⦄ public -record Alternative (F : Type↑) : Typeω where +record Alternative (F : Type↑ ℓ↑) : Typeω where infixr 3 _<|>_ field _<|>_ : F A → F A → F A open Alternative ⦃...⦄ public diff --git a/Class/Bifunctor.agda b/Class/Bifunctor.agda index f800b3f..0bfe875 100644 --- a/Class/Bifunctor.agda +++ b/Class/Bifunctor.agda @@ -13,7 +13,7 @@ private variable -- ** indexed/dependent version record BifunctorI - (F : (A : Type a) (B : A → Type b) → Type (a ⊔ b)) : Type (lsuc (a ⊔ b)) where + (F : ∀ {a b} → (A : Type a) (B : A → Type b) → Type (ℓ↑² a b)) : Typeω where field bimap′ : (f : A → A′) → (∀ {x} → B x → C (f x)) → F A B → F A′ C @@ -30,11 +30,11 @@ record BifunctorI open BifunctorI ⦃...⦄ public instance - Bifunctor-Σ : BifunctorI {a}{b} Σ + Bifunctor-Σ : BifunctorI Σ Bifunctor-Σ .bimap′ = ×.map -- ** non-dependent version -record Bifunctor (F : Type a → Type b → Type (a ⊔ b)) : Type (lsuc (a ⊔ b)) where +record Bifunctor (F : Type↑² ℓ↑²) : Typeω where field bimap : ∀ {A A′ : Type a} {B B′ : Type b} → (A → A′) → (B → B′) → F A B → F A′ B′ @@ -50,16 +50,15 @@ record Bifunctor (F : Type a → Type b → Type (a ⊔ b)) : Type (lsuc (a ⊔ open Bifunctor ⦃...⦄ public -map₁₂ : ∀ {F : Type a → Type a → Type a} {A B : Type a} - → ⦃ Bifunctor F ⦄ - → (A → B) → F A A → F B B +map₁₂ : ∀ {F : Type↑² ℓ↑²} ⦃ _ : Bifunctor F ⦄ → + (∀ {a} {A B : Type a} → (A → B) → F A A → F B B) map₁₂ f = bimap f f _<$>₁₂_ = map₁₂ infixl 4 _<$>₁₂_ instance - Bifunctor-× : Bifunctor {a}{b} _×_ + Bifunctor-× : Bifunctor _×_ Bifunctor-× .bimap f g = ×.map f g - Bifunctor-⊎ : Bifunctor {a}{b} _⊎_ + Bifunctor-⊎ : Bifunctor _⊎_ Bifunctor-⊎ .bimap = ⊎.map diff --git a/Class/Core.agda b/Class/Core.agda index fe5b91f..7d0abe1 100644 --- a/Class/Core.agda +++ b/Class/Core.agda @@ -3,13 +3,32 @@ module Class.Core where open import Class.Prelude -Type[_↝_] : ∀ ℓ ℓ′ → Type (lsuc ℓ ⊔ lsuc ℓ′) +-- ** unary type formers + +Type[_↝_] : ∀ ℓ ℓ′ → Type _ Type[ ℓ ↝ ℓ′ ] = Type ℓ → Type ℓ′ -Type↑ : Typeω -Type↑ = ∀ {ℓ} → Type[ ℓ ↝ ℓ ] +Level↑ = Level → Level + +variable ℓ↑ ℓ↑′ : Level↑ + +Type↑ : Level↑ → Typeω +Type↑ ℓ↑ = ∀ {ℓ} → Type[ ℓ ↝ ℓ↑ ℓ ] + +variable M F : Type↑ ℓ↑ + +-- ** binary type formers +Type[_∣_↝_] : ∀ ℓ ℓ′ ℓ″ → Type _ +Type[ ℓ ∣ ℓ′ ↝ ℓ″ ] = Type ℓ → Type ℓ′ → Type ℓ″ -module _ (M : Type↑) where +Level↑² = Level → Level → Level + +Type↑² : Level↑² → Typeω +Type↑² ℓ↑² = ∀ {ℓ ℓ′} → Type[ ℓ ∣ ℓ′ ↝ ℓ↑² ℓ ℓ′ ] + +variable ℓ↑² ℓ↑²′ : Level → Level → Level + +module _ (M : Type↑ ℓ↑) where _¹ : (A → Type ℓ) → Type _ _¹ P = ∀ {x} → M (P x) @@ -18,6 +37,3 @@ module _ (M : Type↑) where _³ : (A → B → C → Type ℓ) → Type _ _³ _~_~_ = ∀ {x y z} → M (x ~ y ~ z) - -variable - M F : Type↑ diff --git a/Class/Foldable/Core.agda b/Class/Foldable/Core.agda index d72fd68..3216990 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 (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where field fold : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A open Foldable ⦃...⦄ public diff --git a/Class/Functor/Core.agda b/Class/Functor/Core.agda index 61a9579..50f7d68 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↑ ℓ↑) : Typeω where infixl 4 _<$>_ _<$_ infixl 1 _<&>_ @@ -20,7 +20,7 @@ record Functor (F : Type↑) : Typeω where _<&>_ = flip _<$>_ open Functor ⦃...⦄ public -record FunctorLaws (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where +record FunctorLaws (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where field -- preserves identity morphisms fmap-id : ∀ {A : Type a} (x : F A) → diff --git a/Class/Monad/Core.agda b/Class/Monad/Core.agda index 31dd04c..c835c22 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 (M : Type↑ ℓ↑) : Typeω where infixl 1 _>>=_ _>>_ _>=>_ infixr 1 _=<<_ _<=<_ diff --git a/Class/Monad/Instances.agda b/Class/Monad/Instances.agda index b3d2d59..b0fe341 100644 --- a/Class/Monad/Instances.agda +++ b/Class/Monad/Instances.agda @@ -19,3 +19,15 @@ instance .return → just ._>>=_ → Maybe._>>=_ where import Data.Maybe as Maybe + + Monad-Sumˡ : Monad (_⊎ A) + Monad-Sumˡ = λ where + .return → inj₁ + ._>>=_ (inj₁ a) f → f a + ._>>=_ (inj₂ b) f → inj₂ b + + Monad-Sumʳ : Monad (A ⊎_) + Monad-Sumʳ = λ where + .return → inj₂ + ._>>=_ (inj₁ a) f → inj₁ a + ._>>=_ (inj₂ b) f → f b diff --git a/Class/Traversable/Core.agda b/Class/Traversable/Core.agda index cb08392..b9ff1c5 100644 --- a/Class/Traversable/Core.agda +++ b/Class/Traversable/Core.agda @@ -6,7 +6,7 @@ open import Class.Core open import Class.Functor.Core open import Class.Monad -record Traversable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where +record Traversable (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where field sequence : ⦃ Monad M ⦄ → F (M A) → M (F A) traverse : ⦃ Monad M ⦄ → (A → M B) → F A → M (F B) diff --git a/Test/Functor.agda b/Test/Functor.agda index 599717a..7d374b7 100644 --- a/Test/Functor.agda +++ b/Test/Functor.agda @@ -30,3 +30,9 @@ _ = map₂′ id (1 , 2 ∷ []) ≡ ((∃ λ n → Vec ℕ n) ∋ (1 , 2 ∷ []) ∋ refl _ = bimap′ suc (2 ∷_) (0 , []) ≡ ((∃ λ n → Vec ℕ n) ∋ (1 , 2 ∷ [])) ∋ refl + +-- ** cross-level mapping +module _ (X : Type) (Y : Type₁) (Z : Type₂) (g : X → Y) (f : Y → Z) (xs : List X) where + _ : fmap (f ∘ g) xs + ≡ (fmap f ∘ fmap g) xs + _ = fmap-∘ xs diff --git a/Test/Monad.agda b/Test/Monad.agda new file mode 100644 index 0000000..a28770c --- /dev/null +++ b/Test/Monad.agda @@ -0,0 +1,62 @@ +{-# OPTIONS --cubical-compatible #-} +module Test.Monad where + +open import Data.List using (length) + +open import Class.Core +open import Class.Prelude +open import Class.Functor +open import Class.Monad + +-- ** maybe monad + +pred? : ℕ → Maybe ℕ +pred? = λ where + 0 → nothing + (suc n) → just n + +getPred : ℕ → Maybe ℕ +getPred = λ n → do + x ← pred? n + return x + +_ = getPred 3 ≡ just 2 + ∋ refl + +-- ** reader monad + +ReaderT : ∀ (M : Type↑ ℓ↑) → Type ℓ → Type ℓ′ → _ +ReaderT M A B = A → M B + +instance + Monad-ReaderT : ⦃ _ : Monad M ⦄ → Monad (ReaderT M A) + Monad-ReaderT = λ where + .return → λ x _ → return x + ._>>=_ m k → λ a → m a >>= λ b → k b a + +Reader : Type ℓ → Type ℓ′ → Type _ +Reader = ReaderT id + +instance + Monad-Id : Monad id + Monad-Id = λ where + .return → id + ._>>=_ m k → k m + {-# INCOHERENT Monad-Id #-} + +ask : Reader A A +ask a = a + +local : (A → B) → Reader B C → Reader A C +local f r = r ∘ f + +runReader : A → Reader A B → B +runReader = flip _$_ + +getLength : List (Maybe ℕ) → ℕ +getLength ys = runReader ys $ local (just 0 ∷_) $ do + xs ← ask + return (length xs) + +_ = getLength (just 1 ∷ nothing ∷ just 2 ∷ []) ≡ 4 + ∋ refl diff --git a/Test/Reflection.agda b/Test/Reflection.agda new file mode 100644 index 0000000..4453fec --- /dev/null +++ b/Test/Reflection.agda @@ -0,0 +1,9 @@ +module Test.Reflection where + +open import Reflection hiding (_>>=_) +open import Data.Nat using (zero) +open import Class.Monad + +-- ** cross-level bind +_ : TC Set +_ = getType (quote zero) >>= unquoteTC diff --git a/standard-library-classes.agda b/standard-library-classes.agda index 0916026..85e59a2 100644 --- a/standard-library-classes.agda +++ b/standard-library-classes.agda @@ -25,11 +25,13 @@ 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.MonotonePredicate public -- ** Tests open import Test.Monoid open import Test.Functor +open import Test.Monad open import Test.DecEq open import Test.Decidable open import Test.Show +open import Test.Reflection