Change Monad polymorphism

.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

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

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

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↑

Class/Foldable/Core.agda

@@ -7,15 +7,15 @@ 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
   foldMap f = fold ∘ fmap f
 
 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

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) →

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

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,15 +84,31 @@ 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
 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

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)

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
 

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)

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

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