Change Monad polymorphism

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

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,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

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/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 _=<<_ _<=<_
 

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

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)

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

@@ -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

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

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