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,33 @@ 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↑ → Level↑ → Typeω
+Type↑ ℓ↑ ℓ↑′ = ∀ {ℓ} → Type[ ℓ↑ ℓ ↝ ℓ↑′ ℓ ]
+
+variable M F : Type↑ ℓ↑ ℓ↑′
+
+-- ** binary type formers
 
-module _ (M : Type↑) where
+Type[_∣_↝_] : ∀ ℓ ℓ′ ℓ″ → Type _
+Type[ ℓ ∣ ℓ′ ↝ ℓ″ ] = Type ℓ → Type ℓ′ → Type ℓ″
+
+Level↑² = Level → Level → Level
+
+Type↑² : Level↑ → Level↑ → Level↑² → Typeω
+Type↑² ℓ↑ ℓ↑′ ℓ↑² = ∀ {ℓ ℓ′} → Type[ ℓ↑ ℓ ∣ ℓ↑′ ℓ′ ↝ ℓ↑² ℓ ℓ′ ]
+
+variable ℓ↑² ℓ↑²′ : Level → Level → Level
+
+module _ (M : Type↑ id ℓ↑′) where
   _¹ : (A → Type ℓ) → Type _
   _¹ P = ∀ {x} → M (P x)
 
@@ -18,6 +38,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,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↑ ℓ↑ ℓ↑′) ⦃ _ : Functor (λ {ℓ} → F {ℓ}) ⦄ : Typeω where
   field
     -- preserves identity morphisms
-    fmap-id : ∀ {A : Type a} (x : F A) →
+    fmap-id : ∀ {A : Type (ℓ↑ a)} (x : F {a} A) →
       fmap id x ≡ x
     -- preserves composition of morphisms
-    fmap-∘  : ∀ {A : Type a} {B : Type b} {C : Type c}
-                {f : B → C} {g : A → B} (x : F A) →
-      fmap (f ∘ g) x ≡ (fmap f ∘ fmap g) x
+    fmap-∘  : ∀ {A : Type (ℓ↑ a)} {B : Type (ℓ↑ b)} {C : Type (ℓ↑ c)}
+                {f : B → C} {g : A → B} (x : F {a} A) →
+      fmap (f ∘ g) x ≡ (fmap {F = F} {b}{A = B} {c}{B = C} f ∘ fmap  g) x
 open FunctorLaws ⦃...⦄ public

Class/Functor/Instances.agda

@@ -4,8 +4,10 @@ module Class.Functor.Instances where
 open import Class.Prelude
 open import Class.Functor.Core
 
+private Functor↓ = Functor {id}
+
 instance
-  Functor-Maybe : Functor Maybe
+  Functor-Maybe : Functor↓ Maybe
   Functor-Maybe = record {M}
     where import Data.Maybe as M renaming (map to _<$>_)
 
@@ -14,7 +16,7 @@ instance
     .fmap-id → λ where (just _) → refl; nothing → refl
     .fmap-∘  → λ where (just _) → refl; nothing → refl
 
-  Functor-List : Functor List
+  Functor-List : Functor↓ List
   Functor-List ._<$>_ = map
 
   FunctorLaws-List : FunctorLaws List
@@ -31,25 +33,25 @@ instance
         [] → refl
         (x ∷ xs) → cong (f (g x) ∷_) (q xs)
 
-  Functor-List⁺ : Functor List⁺
+  Functor-List⁺ : Functor↓ 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↓ (flip Vec n)
   Functor-Vec = record {V}
     where import Data.Vec as V renaming (map to _<$>_)
 
-  Functor-TC : Functor TC
+  Functor-TC : Functor↓ TC
   Functor-TC = record {R}
     where import Reflection.TCM.Syntax as R
 
-  Functor-Abs : Functor Abs
+  Functor-Abs : Functor↓ Abs
   Functor-Abs = record {R}
     where import Reflection.AST.Abstraction as R renaming (map to _<$>_)
 
-  Functor-Arg : Functor Arg
+  Functor-Arg : Functor↓ Arg
   Functor-Arg = record {R}
     where import Reflection.AST.Argument as R renaming (map to _<$>_)
 
-  Functor-∃Vec : Functor (∃ ∘ Vec)
+  Functor-∃Vec : Functor↓ (∃ ∘ 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 (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

@@ -3,7 +3,7 @@ module Test.Functor where
 
 open import Class.Prelude
 open import Class.Functor
-open import Class.Bifunctor
+-- open import Class.Bifunctor
 
 _ = fmap suc (just 0) ≡ just 1
   ∋ refl
@@ -16,17 +16,39 @@ _ = fmap suc (Vec ℕ 3 ∋ 0 ∷ 1 ∷ 2 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [])
 _ = fmap suc (∃ (Vec ℕ) ∋ -, 0 ∷ 1 ∷ 2 ∷ []) ≡ (-, 1 ∷ 2 ∷ 3 ∷ [])
   ∋ refl
 
-_ = map₁ suc (0 , (List ℕ ∋ [])) ≡ (1 , [])
-  ∋ refl
-_ = map₂ (2 ∷_) (0 , []) ≡ (0 , [ 2 ])
-  ∋ refl
-_ = bimap suc (2 ∷_) (0 , []) ≡ (1 , [ 2 ])
-  ∋ refl
-_ = map₁₂ suc (0 , 1) ≡ (1 , 2)
-  ∋ refl
-_ = map₁′ suc (0 , (List ℕ ∋ [])) ≡ (1 , [])
-  ∋ refl
-_ = map₂′ id (1 , 2 ∷ []) ≡ ((∃ λ n → Vec ℕ n) ∋ (1 , 2 ∷ []))
-  ∋ refl
-_ = bimap′ suc (2 ∷_) (0 , []) ≡ ((∃ λ n → Vec ℕ n) ∋ (1 , 2 ∷ []))
-  ∋ refl
+-- _ = map₁ suc (0 , (List ℕ ∋ [])) ≡ (1 , [])
+--   ∋ refl
+-- _ = map₂ (2 ∷_) (0 , []) ≡ (0 , [ 2 ])
+--   ∋ refl
+-- _ = bimap suc (2 ∷_) (0 , []) ≡ (1 , [ 2 ])
+--   ∋ refl
+-- _ = map₁₂ suc (0 , 1) ≡ (1 , 2)
+--   ∋ refl
+-- _ = map₁′ suc (0 , (List ℕ ∋ [])) ≡ (1 , [])
+--   ∋ refl
+-- _ = 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
+
+-- ** base level
+
+data newtype (A : Type ℓ) : Type ℓ where
+  mk : A → newtype A
+
+data newtype₀ (A : Type) : Type where
+  mk : A → newtype₀ A
+
+instance
+  _ : Functor {id} newtype
+  _ = λ where ._<$>_ f (mk x) → mk (f x)
+
+  -- ** WORKS even for non-polymorphic newtype₀
+  _ : Functor newtype₀
+  _ = λ where ._<$>_ f (mk x) → mk (f x)

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