Skip to content

Commit 9464f57

Browse files
omelkonianomelkonian
committed
Change Monad polymorphism
1 parent e732956 commit 9464f57

12 files changed

Lines changed: 148 additions & 37 deletions

File tree

‎Class/Applicative/Core.agda‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ open import Class.Prelude
55
open import Class.Core
66
open import Class.Functor.Core
77

8-
record Applicative (F : Type↑) : Typeω where
8+
record Applicative (F : Type↑ ℓ↑) : Typeω where
9+
constructor mkApplicative
910
infixl 4 _<*>_ _⊛_ _<*_ _<⊛_ _*>_ _⊛>_
1011
infix 4 _⊗_
1112

@@ -34,13 +35,24 @@ record Applicative (F : Type↑) : Typeω where
3435

3536
open Applicative ⦃...⦄ public
3637

37-
record Applicative₀ (F : Type↑) : Typeω where
38+
module MkApplicative
39+
(pure : ∀ {ℓ} {A : Type ℓ} → A → F A)
40+
(_<*>_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → F (A → B) → F A → F B)
41+
where instance
42+
43+
⇒Functor : Functor F
44+
⇒Functor ._<$>_ f mx = pure f <*> mx
45+
46+
⇒Applicative : Applicative F
47+
⇒Applicative = mkApplicative pure _<*>_
48+
49+
record Applicative₀ (F : Type↑ ℓ↑) : Typeω where
3850
field
3951
overlap ⦃ super ⦄ : Applicative F
4052
ε₀ : F A
4153
open Applicative₀ ⦃...⦄ public
4254

43-
record Alternative (F : Type↑) : Typeω where
55+
record Alternative (F : Type↑ ℓ↑) : Typeω where
4456
infixr 3 _<|>_
4557
field _<|>_ : F A → F A → F A
4658
open Alternative ⦃...⦄ public

‎Class/Bifunctor.agda‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ private variable
1313

1414
-- ** indexed/dependent version
1515
record BifunctorI
16-
(F : (A : Type a) (B : A → Type b) → Type (a ⊔ b)) : Type (lsuc (a ⊔ b)) where
16+
(F : ∀ {a b} → (A : Type a) (B : A → Type b) → Type (ℓ↑² a b)) : Typeω where
1717
field
1818
bimap′ : (f : A → A′) → (∀ {x} → B x → C (f x)) → F A B → F A′ C
1919

@@ -30,11 +30,11 @@ record BifunctorI
3030
open BifunctorI ⦃...⦄ public
3131

3232
instance
33-
Bifunctor-Σ : BifunctorI {a}{b} Σ
33+
Bifunctor-Σ : BifunctorI Σ
3434
Bifunctor-Σ .bimap′ = ×.map
3535

3636
-- ** non-dependent version
37-
record Bifunctor (F : Type a → Type b → Type (a ⊔ b)) : Type (lsuc (a ⊔ b)) where
37+
record Bifunctor (F : Type↑² ℓ↑²) : Typeω where
3838
field
3939
bimap : ∀ {A A′ : Type a} {B B′ : Type b} → (A → A′) → (B → B′) → F A B → F A′ B′
4040

@@ -50,16 +50,15 @@ record Bifunctor (F : Type a → Type b → Type (a ⊔ b)) : Type (lsuc (a ⊔
5050

5151
open Bifunctor ⦃...⦄ public
5252

53-
map₁₂ : ∀ {F : Type a → Type a → Type a} {A B : Type a}
54-
→ ⦃ Bifunctor F ⦄
55-
→ (A → B) → F A A → F B B
53+
map₁₂ : ∀ {F : Type↑² ℓ↑²} ⦃ _ : Bifunctor F ⦄ →
54+
(∀ {a} {A B : Type a} → (A → B) → F A A → F B B)
5655
map₁₂ f = bimap f f
5756
_<$>₁₂_ = map₁₂
5857
infixl 4 _<$>₁₂_
5958

6059
instance
61-
Bifunctor-× : Bifunctor {a}{b} _×_
60+
Bifunctor-× : Bifunctor _×_
6261
Bifunctor-× .bimap f g = ×.map f g
6362

64-
Bifunctor-⊎ : Bifunctor {a}{b} _⊎_
63+
Bifunctor-⊎ : Bifunctor _⊎_
6564
Bifunctor-⊎ .bimap = ⊎.map

‎Class/Core.agda‎

Lines changed: 23 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,32 @@ module Class.Core where
33

44
open import Class.Prelude
55

6-
Type[_↝_] : ∀ ℓ ℓ′ → Type (lsuc ℓ ⊔ lsuc ℓ′)
6+
-- ** unary type formers
7+
8+
Type[_↝_] : ∀ ℓ ℓ′ → Type _
79
Type[ ℓ ↝ ℓ′ ] = Type ℓ → Type ℓ′
810

9-
Type↑ : Typeω
10-
Type↑ = ∀ {ℓ} → Type[ ℓ ↝ ℓ ]
11+
Level↑ = Level → Level
12+
13+
variable ℓ↑ ℓ↑′ : Level↑
14+
15+
Type↑ : Level↑ → Typeω
16+
Type↑ ℓ↑ = ∀ {ℓ} → Type[ ℓ ↝ ℓ↑ ℓ ]
17+
18+
variable M F : Type↑ ℓ↑
19+
20+
-- ** binary type formers
21+
Type[_∣_↝_] : ∀ ℓ ℓ′ ℓ″ → Type _
22+
Type[ ℓ ∣ ℓ′ ↝ ℓ″ ] = Type ℓ → Type ℓ′ → Type ℓ″
1123

12-
module _ (M : Type↑) where
24+
Level↑² = Level → Level → Level
25+
26+
Type↑² : Level↑² → Typeω
27+
Type↑² ℓ↑² = ∀ {ℓ ℓ′} → Type[ ℓ ∣ ℓ′ ↝ ℓ↑² ℓ ℓ′ ]
28+
29+
variable ℓ↑² ℓ↑²′ : Level → Level → Level
30+
31+
module _ (M : Type↑ ℓ↑) where
1332
_¹ : (A → Type ℓ) → Type _
1433
_¹ P = ∀ {x} → M (P x)
1534

@@ -18,6 +37,3 @@ module _ (M : Type↑) where
1837

1938
_³ : (A → B → C → Type ℓ) → Type _
2039
_³ _~_~_ = ∀ {x y z} → M (x ~ y ~ z)
21-
22-
variable
23-
M F : Type↑

‎Class/Foldable/Core.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,15 @@ open import Class.Functor
77
open import Class.Semigroup
88
open import Class.Monoid
99

10-
record Foldable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
10+
record Foldable (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where
1111
field fold : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A
1212

1313
foldMap : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B
1414
foldMap f = fold ∘ fmap f
1515

1616
open Foldable ⦃...⦄ public
1717

18-
record Foldable′ (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
18+
record Foldable′ (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where
1919
field foldMap′ : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B
2020

2121
fold′ : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A

‎Class/Functor/Core.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ open import Class.Core
66

77
private variable a b c : Level
88

9-
record Functor (F : Type↑) : Typeω where
9+
record Functor (F : Type↑ ℓ↑) : Typeω where
1010
infixl 4 _<$>_ _<$_
1111
infixl 1 _<&>_
1212

@@ -20,7 +20,7 @@ record Functor (F : Type↑) : Typeω where
2020
_<&>_ = flip _<$>_
2121
open Functor ⦃...⦄ public
2222

23-
record FunctorLaws (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
23+
record FunctorLaws (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where
2424
field
2525
-- preserves identity morphisms
2626
fmap-id : ∀ {A : Type a} (x : F A) →

‎Class/Monad.agda‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,6 @@ module Class.Monad where
33

44
open import Class.Monad.Core public
55
open import Class.Monad.Instances public
6+
7+
-- ** do not export: breaks instance resolution in general
8+
-- open import Class.Monad.Id public

‎Class/Monad/Core.agda‎

Lines changed: 29 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,11 @@ module Class.Monad.Core where
33

44
open import Class.Prelude
55
open import Class.Core
6-
open import Class.Functor
7-
open import Class.Applicative
6+
open import Class.Functor.Core
7+
open import Class.Applicative.Core
88

9-
record Monad (M : Type↑) : Typeω where
9+
record Monad (M : Type↑ ℓ↑) : Typeω where
10+
constructor mkMonad
1011
infixl 1 _>>=_ _>>_ _>=>_
1112
infixr 1 _=<<_ _<=<_
1213

@@ -32,9 +33,6 @@ record Monad (M : Type↑) : Typeω where
3233
join : M (M A) → M A
3334
join m = m >>= id
3435

35-
Functor-M : Functor M
36-
Functor-M = λ where ._<$>_ f x → return ∘ f =<< x
37-
3836
open Monad ⦃...⦄ public
3937

4038
module _ ⦃ _ : Monad M ⦄ where
@@ -67,7 +65,13 @@ module _ ⦃ _ : Monad M ⦄ where
6765
[] → return []
6866
(x ∷ xs) → ⦇ f x ∷ traverseM f xs ⦈
6967

70-
record MonadLaws (M : Type↑) ⦃ _ : Monad M ⦄ : Typeω where
68+
whenM : Bool -> M ⊤ -> M ⊤
69+
whenM cond act =
70+
if cond
71+
then act >> return _
72+
else return _
73+
74+
record MonadLaws (M : Type↑ ℓ↑) ⦃ _ : Monad M ⦄ : Typeω where
7175
field
7276
>>=-identityˡ : ∀ {A : Type ℓ} {B : Type ℓ′} →
7377
∀ {a : A} {h : A → M B} →
@@ -80,15 +84,31 @@ record MonadLaws (M : Type↑) ⦃ _ : Monad M ⦄ : Typeω where
8084
((m >>= g) >>= h) ≡ (m >>= (λ x → g x >>= h))
8185
open MonadLaws ⦃...⦄ public
8286

83-
record Monad₀ (M : Type↑) : Typeω where
87+
module MkMonad
88+
(return : ∀ {ℓ} {A : Type ℓ} → A → M A)
89+
(_>>=_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → M A → (A → M B) → M B)
90+
where instance
91+
92+
⇒Functor : Functor M
93+
⇒Functor ._<$>_ f mx = mx >>= (return ∘ f)
94+
95+
⇒Applicative : Applicative M
96+
⇒Applicative = λ where
97+
.pure → return
98+
._<*>_ mf mx → mf >>= (_<$> mx)
99+
100+
⇒Monad : Monad M
101+
⇒Monad = mkMonad return _>>=_
102+
103+
record Monad₀ (M : Type↑ ℓ↑) : Typeω where
84104
field ⦃ isMonad ⦄ : Monad M
85105
⦃ isApplicative₀ ⦄ : Applicative₀ M
86106
open Monad₀ ⦃...⦄ using () public
87107
instance
88108
mkMonad₀ : ⦃ Monad M ⦄ → ⦃ Applicative₀ M ⦄ → Monad₀ M
89109
mkMonad₀ = record {}
90110

91-
record Monad⁺ (M : Type↑) : Typeω where
111+
record Monad⁺ (M : Type↑ ℓ↑) : Typeω where
92112
field ⦃ isMonad ⦄ : Monad M
93113
⦃ isAlternative ⦄ : Alternative M
94114
open Monad⁺ ⦃...⦄ using () public

‎Class/Monad/Instances.agda‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,8 @@
22
module Class.Monad.Instances where
33

44
open import Class.Prelude
5-
open import Class.Functor.Core
65
open import Class.Applicative
76
open import Class.Monad.Core
8-
open import Class.Monad.Id
97

108
instance
119
Monad-TC : Monad TC
@@ -32,3 +30,9 @@ instance
3230
.>>=-assoc → λ where
3331
(just _) → refl
3432
nothing → refl
33+
34+
module _ {X : Type ℓ} where
35+
module Monad-Sumˡ = MkMonad {M = X ⊎_}
36+
inj₂ (λ where (inj₁ a) f → inj₁ a; (inj₂ b) f → f b)
37+
module Monad-Sumʳ = MkMonad {M = _⊎ X}
38+
inj₁ (λ where (inj₁ a) f → f a; (inj₂ b) f → inj₂ b)

‎Class/Pointed/Core.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ open import Class.Core
66
open import Class.Applicative.Core
77
open import Class.Monad.Core
88

9-
record Pointed (F : Type↑) : Typeω where
9+
record Pointed (F : Type↑ ℓ↑) : Typeω where
1010
field point : ∀ {A : Type ℓ} → A → F A
1111
open Pointed ⦃...⦄ public
1212

‎Class/Traversable/Core.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,14 @@ open import Class.Functor.Core
77
open import Class.Applicative.Core
88
open import Class.Monad.Core
99

10-
record TraversableA (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
10+
record TraversableA (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where
1111
field sequenceA : ⦃ Applicative M ⦄ → F (M A) → M (F A)
1212

1313
traverseA : ⦃ Applicative M ⦄ → (A → M B) → F A → M (F B)
1414
traverseA f = sequenceA ∘ fmap f
1515
open TraversableA ⦃...⦄ public
1616

17-
record Traversable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
17+
record Traversable (F : Type↑ ℓ↑) ⦃ _ : Functor F ⦄ : Typeω where
1818
field sequence : ⦃ Monad M ⦄ → F (M A) → M (F A)
1919

2020
traverse : ⦃ Monad M ⦄ → (A → M B) → F A → M (F B)

0 commit comments

Comments
 (0)