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

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

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}

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

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

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

Class/Functor/Instances.agda

@@ -4,52 +4,54 @@ 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
       p = λ where
         [] → 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)

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 _

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

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

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

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)