From 9464f571aa5b97cb7f54edb0c2381dcdebd476d0 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Wed, 3 Jun 2026 08:51:29 +0100 Subject: [PATCH 1/2] Change `Monad` polymorphism --- Class/Applicative/Core.agda | 18 ++++++++++--- Class/Bifunctor.agda | 15 +++++------ Class/Core.agda | 30 ++++++++++++++++----- Class/Foldable/Core.agda | 4 +-- Class/Functor/Core.agda | 4 +-- Class/Monad.agda | 3 +++ Class/Monad/Core.agda | 38 +++++++++++++++++++------- Class/Monad/Instances.agda | 8 ++++-- Class/Pointed/Core.agda | 2 +- Class/Traversable/Core.agda | 4 +-- Test/Functor.agda | 6 +++++ Test/Monad.agda | 53 ++++++++++++++++++++++++++++++++++++- 12 files changed, 148 insertions(+), 37 deletions(-) diff --git a/Class/Applicative/Core.agda b/Class/Applicative/Core.agda index 93649ef..8b80ecd 100644 --- a/Class/Applicative/Core.agda +++ b/Class/Applicative/Core.agda @@ -5,7 +5,8 @@ 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 + constructor mkApplicative infixl 4 _<*>_ _⊛_ _<*_ _<⊛_ _*>_ _⊛>_ infix 4 _⊗_ @@ -34,13 +35,24 @@ record Applicative (F : Type↑) : Typeω where open Applicative ⦃...⦄ public -record Applicative₀ (F : Type↑) : Typeω where +module MkApplicative + (pure : ∀ {ℓ} {A : Type ℓ} → A → F A) + (_<*>_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → F (A → B) → F A → F B) + where instance + + ⇒Functor : Functor F + ⇒Functor ._<$>_ f mx = pure f <*> mx + + ⇒Applicative : Applicative F + ⇒Applicative = mkApplicative pure _<*>_ + +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 a3e24ee..c7f4b4f 100644 --- a/Class/Foldable/Core.agda +++ b/Class/Foldable/Core.agda @@ -7,7 +7,7 @@ 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 foldMap : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B @@ -15,7 +15,7 @@ record Foldable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where open Foldable ⦃...⦄ public -record Foldable′ (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where +record Foldable′ (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where field foldMap′ : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B fold′ : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A 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.agda b/Class/Monad.agda index 9e896d1..12fd4c7 100644 --- a/Class/Monad.agda +++ b/Class/Monad.agda @@ -3,3 +3,6 @@ module Class.Monad where open import Class.Monad.Core public open import Class.Monad.Instances public + +-- ** do not export: breaks instance resolution in general +-- open import Class.Monad.Id public diff --git a/Class/Monad/Core.agda b/Class/Monad/Core.agda index bf95d4b..d96c7ba 100644 --- a/Class/Monad/Core.agda +++ b/Class/Monad/Core.agda @@ -3,10 +3,11 @@ module Class.Monad.Core where open import Class.Prelude open import Class.Core -open import Class.Functor -open import Class.Applicative +open import Class.Functor.Core +open import Class.Applicative.Core -record Monad (M : Type↑) : Typeω where +record Monad (M : Type↑ ℓ↑) : Typeω where + constructor mkMonad infixl 1 _>>=_ _>>_ _>=>_ infixr 1 _=<<_ _<=<_ @@ -32,9 +33,6 @@ record Monad (M : Type↑) : Typeω where join : M (M A) → M A join m = m >>= id - Functor-M : Functor M - Functor-M = λ where ._<$>_ f x → return ∘ f =<< x - open Monad ⦃...⦄ public module _ ⦃ _ : Monad M ⦄ where @@ -67,7 +65,13 @@ module _ ⦃ _ : Monad M ⦄ where [] → return [] (x ∷ xs) → ⦇ f x ∷ traverseM f xs ⦈ -record MonadLaws (M : Type↑) ⦃ _ : Monad M ⦄ : Typeω where + whenM : Bool -> M ⊤ -> M ⊤ + whenM cond act = + if cond + then act >> return _ + else return _ + +record MonadLaws (M : Type↑ ℓ↑) ⦃ _ : Monad M ⦄ : Typeω where field >>=-identityˡ : ∀ {A : Type ℓ} {B : Type ℓ′} → ∀ {a : A} {h : A → M B} → @@ -80,7 +84,23 @@ record MonadLaws (M : Type↑) ⦃ _ : Monad M ⦄ : Typeω where ((m >>= g) >>= h) ≡ (m >>= (λ x → g x >>= h)) open MonadLaws ⦃...⦄ public -record Monad₀ (M : Type↑) : Typeω where +module MkMonad + (return : ∀ {ℓ} {A : Type ℓ} → A → M A) + (_>>=_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → M A → (A → M B) → M B) + where instance + + ⇒Functor : Functor M + ⇒Functor ._<$>_ f mx = mx >>= (return ∘ f) + + ⇒Applicative : Applicative M + ⇒Applicative = λ where + .pure → return + ._<*>_ mf mx → mf >>= (_<$> mx) + + ⇒Monad : Monad M + ⇒Monad = mkMonad return _>>=_ + +record Monad₀ (M : Type↑ ℓ↑) : Typeω where field ⦃ isMonad ⦄ : Monad M ⦃ isApplicative₀ ⦄ : Applicative₀ M open Monad₀ ⦃...⦄ using () public @@ -88,7 +108,7 @@ instance mkMonad₀ : ⦃ Monad M ⦄ → ⦃ Applicative₀ M ⦄ → Monad₀ M mkMonad₀ = record {} -record Monad⁺ (M : Type↑) : Typeω where +record Monad⁺ (M : Type↑ ℓ↑) : Typeω where field ⦃ isMonad ⦄ : Monad M ⦃ isAlternative ⦄ : Alternative M open Monad⁺ ⦃...⦄ using () public diff --git a/Class/Monad/Instances.agda b/Class/Monad/Instances.agda index ef9cc21..e0b9eba 100644 --- a/Class/Monad/Instances.agda +++ b/Class/Monad/Instances.agda @@ -2,10 +2,8 @@ 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 @@ -32,3 +30,9 @@ instance .>>=-assoc → λ where (just _) → refl nothing → refl + +module _ {X : Type ℓ} where + module Monad-Sumˡ = MkMonad {M = X ⊎_} + inj₂ (λ where (inj₁ a) f → inj₁ a; (inj₂ b) f → f b) + module Monad-Sumʳ = MkMonad {M = _⊎ X} + inj₁ (λ where (inj₁ a) f → f a; (inj₂ b) f → inj₂ b) diff --git a/Class/Pointed/Core.agda b/Class/Pointed/Core.agda index e513194..22ba491 100644 --- a/Class/Pointed/Core.agda +++ b/Class/Pointed/Core.agda @@ -6,7 +6,7 @@ open import Class.Core open import Class.Applicative.Core open import Class.Monad.Core -record Pointed (F : Type↑) : Typeω where +record Pointed (F : Type↑ ℓ↑) : Typeω where field point : ∀ {A : Type ℓ} → A → F A open Pointed ⦃...⦄ public diff --git a/Class/Traversable/Core.agda b/Class/Traversable/Core.agda index 975e199..a8a4304 100644 --- a/Class/Traversable/Core.agda +++ b/Class/Traversable/Core.agda @@ -7,14 +7,14 @@ open import Class.Functor.Core open import Class.Applicative.Core open import Class.Monad.Core -record TraversableA (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where +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 +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 index 363cc1a..a1bacc7 100644 --- a/Test/Monad.agda +++ b/Test/Monad.agda @@ -4,7 +4,6 @@ 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 @@ -19,3 +18,55 @@ _ = itω _ : ⦃ _ : Monad M ⦄ → (ℕ → M ℕ) _ = return + +-- ** 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 + +-- ** cross-level bind + +_ : TC Set +_ = getType (quote Nat.zero) >>= unquoteTC + where open import Reflection using (getType; unquoteTC) + +-- ** reader monad + +ReaderT : ∀ (M : Type↑ ℓ↑) → Type ℓ → Type ℓ′ → _ +ReaderT M A B = A → M B + +module _ ⦃ _ : Monad M ⦄ {A : Type ℓ} where + module Monad-ReaderT = MkMonad {M = ReaderT M A} + (λ x _ → return x) + (λ m k a → m a >>= λ b → k b a) + +Reader : Type ℓ → Type ℓ′ → Type _ +Reader = ReaderT 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) + where open import Class.Monad.Id + +_ = getLength (just 1 ∷ nothing ∷ just 2 ∷ []) ≡ 4 + ∋ refl From 9ce3fead9cb2211bd501c84f5311fc4a19962b18 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Wed, 3 Jun 2026 08:58:23 +0100 Subject: [PATCH 2/2] CI: bump setup-agda --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 17c1caf..e2f9eb7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,7 +13,7 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 - - uses: omelkonian/setup-agda@v2.3 + - uses: omelkonian/setup-agda@main with: agda-version: 2.8.0 stdlib-version: 2.3