Skip to content

Commit 39e9b0c

Browse files
HeinrichApfelmusHeinrichApfelmus
authored
Merge pull request #412 from HeinrichApfelmus/HeinrichApfelmus/monad-laws
Reorganize Monad laws, prove Applicative laws
2 parents a5cfdb3 + 88f511c commit 39e9b0c

File tree

9 files changed

+308
-100
lines changed

9 files changed

+308
-100
lines changed

‎lib/base/Haskell/Law/Applicative/FromMonad.agda‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
module Haskell.Law.Applicative.FromMonad where
2+
3+
open import Haskell.Prim
4+
5+
open import Haskell.Prim.Applicative
6+
open import Haskell.Prim.Functor
7+
open import Haskell.Prim.Monad
8+
9+
open import Haskell.Law.Applicative.Def
10+
open import Haskell.Law.Monad.Def as Monad
11+
open import Haskell.Law.Equality
12+
open import Haskell.Law.Functor
13+
open import Haskell.Law.Functor.FromMonad
14+
15+
-------------------------------------------------------------------------------
16+
-- Prove the Applicative laws from the Monad laws
17+
18+
--
19+
prop-PreLawfulMonad→IsLawfulApplicative
20+
: ∀ ⦃ _ : Monad m ⦄ ⦃ _ : PreLawfulMonad m ⦄
21+
→ IsLawfulApplicative m
22+
--
23+
prop-PreLawfulMonad→IsLawfulApplicative {m} = record
24+
{ super = prop-PreLawfulMonad→IsLawfulFunctor
25+
; identity = midentity
26+
; composition = mcomposition
27+
; homomorphism = mhomomorphism
28+
; interchange = minterchange
29+
; functor = mfunctor
30+
}
31+
where
32+
midentity : ∀ {a} (ma : m a) → (pure id <*> ma) ≡ ma
33+
midentity {a} ma
34+
rewrite def-pure-return (id {a})
35+
| def-<*>->>= (return id) ma
36+
= begin
37+
return id >>= (λ f → ma >>= (λ x → return (f x)))
38+
≡⟨ Monad.leftIdentity _ _ ⟩
39+
ma >>= (λ x → return (id x))
40+
≡⟨ Monad.rightIdentity _ ⟩
41+
ma
42+
∎
43+
44+
mfunctor : ∀ {a b} (f : a → b) (u : m a) → fmap f u ≡ (pure f <*> u)
45+
mfunctor f u = begin
46+
fmap f u
47+
≡⟨ Monad.def-fmap->>= _ _ ⟩
48+
(do x ← u; return (f x))
49+
≡⟨ sym (Monad.leftIdentity _ _) ⟩
50+
(do f' ← return f; x ← u; return (f' x))
51+
≡⟨ cong (λ o → o >>= _) (sym (def-pure-return _)) ⟩
52+
(do f' ← pure f; x ← u; return (f' x))
53+
≡⟨ sym (def-<*>->>= _ _) ⟩
54+
pure f <*> u
55+
∎
56+
57+
mcomposition
58+
: ∀ {a b c} (u : m (b → c)) (v : m (a → b)) (w : m a)
59+
→ (pure _∘_ <*> u <*> v <*> w) ≡ (u <*> (v <*> w))
60+
mcomposition u v w
61+
= begin
62+
pure _∘_ <*> u <*> v <*> w
63+
≡⟨ cong (λ o → o <*> u <*> v <*> w) (def-pure-return _∘_) ⟩
64+
return _∘_ <*> u <*> v <*> w
65+
≡⟨ cong (λ o → o <*> v <*> w) (def-<*>->>= _ _ ) ⟩
66+
(do comp ← return _∘_; g ← u; return (comp g)) <*> v <*> w
67+
≡⟨ cong (λ o → o <*> v <*> w) (Monad.leftIdentity _ _) ⟩
68+
(do g ← u; return (_∘_ g)) <*> v <*> w
69+
≡⟨ cong (λ o → o <*> w) (def-<*>->>= _ _ ) ⟩
70+
(do g' ← (do g ← u; return (_∘_ g)); f ← v; return (g' f)) <*> w
71+
≡⟨ cong (λ o → o <*> w) (sym (Monad.associativity u _ _)) ⟩
72+
(do g ← u; g' ← return (_∘_ g); f ← v; return (g' f)) <*> w
73+
≡⟨ cong (λ o → o <*> w) (cong-monad u (λ g → Monad.leftIdentity _ _)) ⟩
74+
(do g ← u; f ← v; return (g ∘ f)) <*> w
75+
≡⟨ def-<*>->>= _ _ ⟩
76+
(do gf ← (do g ← u; f ← v; return (g ∘ f)); x ← w; return (gf x))
77+
≡⟨ sym (Monad.associativity u _ _) ⟩
78+
(do g ← u; gf ← (do f ← v; return (g ∘ f)); x ← w; return (gf x))
79+
≡⟨ cong-monad u (λ g → sym (Monad.associativity v _ _)) ⟩
80+
(do g ← u; do f ← v; gf ← return (g ∘ f); x ← w; return (gf x))
81+
≡⟨ cong-monad u (λ g → cong-monad v (λ f → Monad.leftIdentity _ _)) ⟩
82+
(do g ← u; f ← v; x ← w; return (g (f x)))
83+
≡⟨ cong-monad u (λ g → cong-monad v λ f → cong-monad w (λ x → sym (Monad.leftIdentity _ _))) ⟩
84+
(do g ← u; f ← v; x ← w; y ← return (f x); return (g y))
85+
≡⟨ cong-monad u (λ g → cong-monad v λ x → Monad.associativity _ _ _) ⟩
86+
(do g ← u; f ← v; y ← (do x ← w; return (f x)); return (g y))
87+
≡⟨ cong-monad u (λ g → Monad.associativity _ _ _) ⟩
88+
(do g ← u; y ← (do f ← v; x ← w; return (f x)); return (g y))
89+
≡⟨ sym (def-<*>->>= _ _) ⟩
90+
u <*> (do f ← v; x ← w; return (f x))
91+
≡⟨ cong (λ o → u <*> o) (sym (def-<*>->>= _ _)) ⟩
92+
u <*> (v <*> w)
93+
∎
94+
95+
mhomomorphism
96+
: ∀ {a b} (f : a → b) (x : a)
97+
→ (pure {m} f <*> pure x) ≡ pure (f x)
98+
mhomomorphism f x = begin
99+
pure {m} f <*> pure x
100+
≡⟨ cong₂ (_<*>_) (def-pure-return f) (def-pure-return x) ⟩
101+
return {m} f <*> return x
102+
≡⟨ def-<*>->>= _ _ ⟩
103+
(do f' ← return f; x' ← return x; return (f' x'))
104+
≡⟨ Monad.leftIdentity _ _ ⟩
105+
(do x' ← return x; return (f x'))
106+
≡⟨ Monad.leftIdentity _ _ ⟩
107+
return (f x)
108+
≡⟨ sym (def-pure-return _) ⟩
109+
pure (f x)
110+
∎
111+
112+
minterchange
113+
: ∀ {a b} (u : m (a → b)) (y : a)
114+
→ (u <*> pure y) ≡ (pure (_$ y) <*> u)
115+
minterchange u y = begin
116+
u <*> pure y
117+
≡⟨ cong (u <*>_) (def-pure-return _) ⟩
118+
u <*> return y
119+
≡⟨ def-<*>->>= _ _ ⟩
120+
(do f ← u; y' ← return y; return (f y'))
121+
≡⟨ cong-monad u (λ f → Monad.leftIdentity y _) ⟩
122+
(do f ← u; return (f y))
123+
≡⟨ sym (Monad.leftIdentity _ _) ⟩
124+
(do y'' ← return (_$ y); f ← u; return (y'' f))
125+
≡⟨ sym (def-<*>->>= _ _) ⟩
126+
return (_$ y) <*> u
127+
≡⟨ sym (cong (_<*> u) (def-pure-return _)) ⟩
128+
pure (_$ y) <*> u
129+
∎

‎lib/base/Haskell/Law/Extensionality.agda‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module Haskell.Law.Extensionality where
2+
3+
open import Haskell.Prim
4+
5+
-------------------------------------------------------------------------------
6+
-- Axiom: Functions are equal if they agree on all arguments.
7+
--
8+
-- This axiom is sometimes needed for proving properties of higher-order
9+
-- functions, such as 'filter', 'fmap', or '(>>=)'.
10+
11+
postulate
12+
ext : ∀ {f g : a → b} → (∀ x → f x ≡ g x) → f ≡ g

‎lib/base/Haskell/Law/Functor/FromMonad.agda‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
module Haskell.Law.Functor.FromMonad where
2+
3+
open import Haskell.Prim
4+
5+
open import Haskell.Prim.Functor
6+
open import Haskell.Prim.Monad
7+
8+
open import Haskell.Law.Monad.Def as Monad
9+
open import Haskell.Law.Equality
10+
open import Haskell.Law.Functor
11+
12+
-------------------------------------------------------------------------------
13+
-- Prove the Functor laws from the Monad laws
14+
15+
--
16+
prop-PreLawfulMonad→IsLawfulFunctor
17+
: ∀ ⦃ _ : Monad m ⦄ ⦃ _ : PreLawfulMonad m ⦄
18+
→ IsLawfulFunctor m
19+
--
20+
prop-PreLawfulMonad→IsLawfulFunctor .identity fa
21+
rewrite Monad.def-fmap->>= id fa
22+
= Monad.rightIdentity fa
23+
prop-PreLawfulMonad→IsLawfulFunctor .composition fa f g
24+
rewrite Monad.def-fmap->>= g (fmap f fa)
25+
| Monad.def-fmap->>= f fa
26+
| Monad.def-fmap->>= (g ∘ f) fa
27+
= begin
28+
fa >>= (return ∘ g ∘ f)
29+
≡⟨ cong-monad fa (λ x → sym (Monad.leftIdentity (f x) _)) ⟩
30+
fa >>= (λ x → return (f x) >>= (return ∘ g))
31+
≡⟨ Monad.associativity _ _ _ ⟩
32+
(fa >>= (return ∘ f)) >>= (return ∘ g)
33+
∎

‎lib/base/Haskell/Law/Monad/Def.agda‎

Lines changed: 48 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -9,35 +9,64 @@ open import Haskell.Prim.Monoid
99
open import Haskell.Prim.Tuple
1010

1111
open import Haskell.Law.Applicative
12+
open import Haskell.Law.Equality
13+
open import Haskell.Law.Extensionality
1214

13-
record IsLawfulMonad (F : Type → Type) ⦃ iMonadF : Monad F ⦄ : Type₁ where
14-
field
15-
overlap ⦃ super ⦄ : IsLawfulApplicative F
15+
-- Helper function: Substitution in the second argument of '(>>=)'.
16+
cong-monad
17+
: ∀ ⦃ _ : Monad m ⦄ (mx : m a) {f g : a → m b}
18+
→ (∀ x → f x ≡ g x)
19+
→ (do x ← mx; f x) ≡ (do x ← mx; g x)
20+
--
21+
cong-monad mx {f} {g} eq = cong (mx >>=_) (ext eq)
22+
23+
-------------------------------------------------------------------------------
24+
-- Monad laws
25+
--
26+
-- `PreLawfulMonad` contains all laws that we expect a 'Monad' to satisfy,
27+
-- except that we do not yet require that the superclasses are themselves
28+
-- lawful, this is deferred to `IsLawfulMonad`.
29+
-- The lawfulness of the superclasses can be proven from `PreLawfulMonad`.
1630

17-
-- Left identity: return a >>= k = k a
18-
leftIdentity : {a : Type} → (a' : a) (k : a → F b) → ((return a') >>= k) ≡ k a'
31+
record PreLawfulMonad (m : Type → Type) ⦃ _ : Monad m ⦄ : Type₁ where
32+
field
33+
-- The three monad laws
34+
leftIdentity : ∀ {a} (x : a) (k : a → m b)
35+
→ (return x >>= k) ≡ k x
1936

20-
-- Right identity: m >>= return = m
21-
rightIdentity : {a : Type} → (ma : F a) → (ma >>= return) ≡ ma
37+
rightIdentity : ∀ {a} (ma : m a)
38+
→ (ma >>= return) ≡ ma
2239

23-
-- Associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h
24-
associativity : {a b c : Type} → (ma : F a) (f : a → F b) (g : b → F c)
40+
associativity : ∀ {a b c} (ma : m a) (f : a → m b) (g : b → m c)
2541
→ (ma >>= (λ x → f x >>= g)) ≡ ((ma >>= f) >>= g)
2642

27-
-- pure = return
28-
pureIsReturn : (a' : a) → pure a' ≡ (Monad.return iMonadF a')
29-
-- m1 <*> m2 = m1 >>= (\x1 -> m2 >>= (\x2 -> return (x1 x2)))
30-
sequence2bind : {a b : Type} → (mab : F (a → b)) (ma : F a)
31-
→ (mab <*> ma) ≡ (mab >>= (λ x1 → (ma >>= (λ x2 → return (x1 x2)))))
43+
-- Default functions
44+
def->>->>= : ∀ {a b} (ma : m a) (mb : m b)
45+
→ ma >> mb ≡ ma >>= (λ x → mb)
46+
47+
def-pure-return : ∀ {a} (x : a)
48+
→ pure {m} x ≡ return x
49+
50+
-- Superclass functions
51+
def-fmap->>= : ∀ {a b} (f : a → b) (ma : m a)
52+
→ fmap f ma ≡ ma >>= (return ∘ f)
3253

33-
-- fmap f xs = xs >>= return . f
34-
fmap2bind : {a b : Type} → (f : a → b) (ma : F a)
35-
→ fmap f ma ≡ (ma >>= (return ∘ f))
36-
-- (>>) = (*>)
37-
rSequence2rBind : (ma : F a) → (mb : F b) → (ma *> mb) ≡ (ma >> mb)
54+
def-<*>->>= : ∀ {a b} (mab : m (a → b)) (ma : m a)
55+
→ (mab <*> ma) ≡ (mab >>= (λ f → (ma >>= (λ x → return (f x)))))
56+
57+
open PreLawfulMonad ⦃ ... ⦄ public
58+
59+
-- All laws together
60+
record IsLawfulMonad (m : Type → Type) ⦃ _ : Monad m ⦄ : Type₁ where
61+
field
62+
overlap ⦃ applicative ⦄ : IsLawfulApplicative m
63+
overlap ⦃ monad ⦄ : PreLawfulMonad m
3864

3965
open IsLawfulMonad ⦃ ... ⦄ public
4066

67+
-------------------------------------------------------------------------------
68+
-- postulated monad laws, to be proven
69+
4170
instance postulate
4271
iLawfulMonadFun : IsLawfulMonad (λ b → a → b)
4372

‎lib/base/Haskell/Law/Monad/Either.agda‎

Lines changed: 19 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -10,25 +10,22 @@ open import Haskell.Law.Monad.Def
1010
open import Haskell.Law.Applicative.Either
1111

1212
instance
13-
iLawfulMonadEither : IsLawfulMonad (Either a)
14-
iLawfulMonadEither .leftIdentity _ _ = refl
15-
16-
iLawfulMonadEither .rightIdentity = λ { (Left _) → refl; (Right _) → refl }
17-
18-
iLawfulMonadEither .associativity = λ { (Left _) _ _ → refl; (Right _) _ _ → refl }
19-
20-
iLawfulMonadEither .pureIsReturn _ = refl
21-
22-
iLawfulMonadEither .sequence2bind =
23-
λ { (Left _) _ → refl
24-
; (Right _) (Left _) → refl
25-
; (Right _) (Right _) → refl
26-
}
27-
28-
iLawfulMonadEither .fmap2bind = λ { _ (Left _) → refl; _ (Right _) → refl }
29-
30-
iLawfulMonadEither .rSequence2rBind =
31-
λ { (Left _) _ → refl
32-
; (Right _) (Left _) → refl
33-
; (Right _) (Right _) → refl
34-
}
13+
iPreLawfulMonadEither : PreLawfulMonad (Either a)
14+
iPreLawfulMonadEither = λ where
15+
.leftIdentity _ _ → refl
16+
.rightIdentity (Left x) → refl
17+
.rightIdentity (Right x) → refl
18+
.associativity (Left x) _ _ → refl
19+
.associativity (Right x) _ _ → refl
20+
.def->>->>= _ _ → refl
21+
.def-pure-return _ → refl
22+
.def-fmap->>= _ → λ where
23+
(Left x) → refl
24+
(Right x) → refl
25+
.def-<*>->>= → λ where
26+
(Left _) _ → refl
27+
(Right _) (Left _) → refl
28+
(Right _) (Right _) → refl
29+
30+
iIsLawfulMonadEither : IsLawfulMonad (Either a)
31+
iIsLawfulMonadEither = record {}

‎lib/base/Haskell/Law/Monad/IO.agda‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,11 @@ open import Haskell.Prim.Monad
77

88
open import Haskell.Law.Monad.Def
99

10-
open import Haskell.Law.Applicative.IO
10+
open import Haskell.Law.Applicative.IO using (iLawfulApplicativeIO)
1111

12-
instance postulate iLawfulMonadIO : IsLawfulMonad IO
12+
instance
13+
postulate
14+
iPreLawfulMonadIO : PreLawfulMonad IO
15+
16+
iIsLawfulMonadIO : IsLawfulMonad IO
17+
iIsLawfulMonadIO = record { applicative = iLawfulApplicativeIO }

‎lib/base/Haskell/Law/Monad/List.agda‎

Lines changed: 20 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -11,38 +11,33 @@ open import Haskell.Law.List
1111
open import Haskell.Law.Applicative.List
1212

1313
instance
14-
iLawfulMonadList : IsLawfulMonad List
15-
iLawfulMonadList .leftIdentity a k
16-
rewrite ++-[] (k a)
17-
= refl
14+
iPreLawfulMonadList : PreLawfulMonad List
15+
iPreLawfulMonadList .leftIdentity _ _ = ++-[] _
1816

19-
iLawfulMonadList .rightIdentity [] = refl
20-
iLawfulMonadList .rightIdentity (_ ∷ xs)
21-
rewrite rightIdentity xs
17+
iPreLawfulMonadList .rightIdentity [] = refl
18+
iPreLawfulMonadList .rightIdentity (x ∷ xs)
19+
rewrite iPreLawfulMonadList .PreLawfulMonad.rightIdentity xs
2220
= refl
2321

24-
iLawfulMonadList .associativity [] f g = refl
25-
iLawfulMonadList .associativity (x ∷ xs) f g
22+
iPreLawfulMonadList .associativity [] f g = refl
23+
iPreLawfulMonadList .associativity (x ∷ xs) f g
2624
rewrite associativity xs f g
27-
| concatMap-++-distr (f x) (xs >>= f) g
28-
= refl
29-
30-
iLawfulMonadList .pureIsReturn _ = refl
31-
32-
iLawfulMonadList .sequence2bind [] _ = refl
33-
iLawfulMonadList .sequence2bind (f ∷ fs) xs
34-
rewrite sequence2bind fs xs
35-
| map-concatMap f xs
25+
| concatMap-++-distr (f x) (xs >>= f) g
3626
= refl
3727

38-
iLawfulMonadList .fmap2bind f [] = refl
39-
iLawfulMonadList .fmap2bind f (_ ∷ xs)
40-
rewrite fmap2bind f xs
28+
iPreLawfulMonadList .def->>->>= _ _ = refl
29+
iPreLawfulMonadList .def-pure-return _ = refl
30+
31+
iPreLawfulMonadList .def-fmap->>= _ [] = refl
32+
iPreLawfulMonadList .def-fmap->>= f (x ∷ xs)
33+
rewrite iPreLawfulMonadList .PreLawfulMonad.def-fmap->>= f xs
4134
= refl
4235

43-
iLawfulMonadList .rSequence2rBind [] mb = refl
44-
iLawfulMonadList .rSequence2rBind (x ∷ ma) mb
45-
rewrite rSequence2rBind ma mb
46-
| map-id mb
36+
iPreLawfulMonadList .def-<*>->>= [] xs = refl
37+
iPreLawfulMonadList .def-<*>->>= (f ∷ fs) xs
38+
rewrite iPreLawfulMonadList .PreLawfulMonad.def-<*>->>= fs xs
39+
| map-concatMap f xs
4740
= refl
4841

42+
iIsLawfulMonadList : IsLawfulMonad List
43+
iIsLawfulMonadList = record {}

0 commit comments

Comments
 (0)