Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 98:b7f0879e854e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying Monad-laws for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 21 Jan 2015 17:43:53 +0900
parents
children 9c62373bd474
comparison
equal deleted inserted replaced
97:f26a954cd068 98:b7f0879e854e
1 open import Level
2 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning
4
5 open import basic
6 open import delta
7 open import delta.functor
8 open import deltaM
9 open import deltaM.functor
10 open import laws
11
12 module deltaM.monad where
13 open Functor
14 open NaturalTransformation
15 open Monad
16
17
18 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l}
19 {M : {l' : Level} -> Set l' -> Set l'} ->
20 {functorM : {l' : Level} -> Functor {l'} M}
21 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M (functorM ) } ->
22 NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A)
23 {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}}
24 (deltaM-mu {_} {_} {M} {functorM} {monadM})
25
26 headDeltaM-commute : {l : Level} {A B : Set l}
27 {M : {l' : Level} -> Set l' -> Set l'} ->
28 {functorM : {l' : Level} -> Functor {l'} M} ->
29 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M (functorM ) } ->
30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) ->
31 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x)
32 headDeltaM-commute f (deltaM (mono x)) = refl
33 headDeltaM-commute f (deltaM (delta x d)) = refl
34
35
36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l}
37 {M : {l' : Level} -> Set l' -> Set l'} ->
38 {functorM : {l' : Level} -> Functor {l'} M}
39 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM } ->
40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M
41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM
42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM
43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute }
44
45
46
47 deltaM-association-law : {l : Level} {A : Set l}
48 {M : {l' : Level} -> Set l' -> Set l'}
49 (functorM : {l' : Level} -> Functor {l'} M)
50 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM)
51 -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A)))
52 -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d)
53 deltaM-association-law functorM monadM (deltaM x) = {!!}
54 {-
55 begin
56 (deltaM-mu ∙ deltaM-fmap deltaM-mu) d ≡⟨ refl ⟩
57 deltaM-mu (deltaM-fmap deltaM-mu d) ≡⟨ {!!} ⟩
58 deltaM-mu (deltaM-mu d) ≡⟨ refl ⟩
59 (deltaM-mu ∙ deltaM-mu) d
60 ∎
61 -}
62 {-
63 deltaM-association-law functorM monadM (deltaM (mono x)) = begin
64 (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩
65 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
66 deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ refl ⟩
67 deltaM-mu (deltaM (mono (fmap functorM deltaM-mu x))) ≡⟨ refl ⟩
68 deltaM-bind (deltaM (mono (fmap functorM deltaM-mu x))) id ≡⟨ refl ⟩
69 deltaM (mono (bind monadM (fmap functorM deltaM-mu x) (headDeltaM ∙ id))) ≡⟨ refl ⟩
70 deltaM (mono (bind monadM (fmap functorM deltaM-mu x) headDeltaM)) ≡⟨ {!!} ⟩
71 deltaM (mono (bind monadM (bind monadM x headDeltaM) headDeltaM)) ≡⟨ refl ⟩
72 deltaM (mono (bind monadM (bind monadM x (headDeltaM ∙ id)) (headDeltaM ∙ id))) ≡⟨ refl ⟩
73 deltaM-mu (deltaM (mono (bind monadM x (headDeltaM ∙ id)))) ≡⟨ refl ⟩
74 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
75 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎
76 deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!}
77 -}
78
79 {-
80
81 nya : {l : Level} {A B C : Set l} ->
82 {M : {l' : Level} -> Set l' -> Set l'}
83 {functorM : {l' : Level} -> Functor {l'} M }
84 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
85 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M {functorM} {monadM} B)) -> (g : B -> (DeltaM M C)) ->
86 (x : M A) ->
87 (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡
88 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g)
89 nya = {!!}
90
91 deltaM-monad-law-h-3 : {l : Level} {A B C : Set l} ->
92 {M : {l' : Level} -> Set l' -> Set l'}
93 {functorM : {l' : Level} -> Functor {l'} M }
94 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
95 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M B)) -> (g : B -> (DeltaM M C)) ->
96 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡ (deltaM-bind (deltaM-bind m f) g)
97 {-
98 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin
99 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩
100
101 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩
102 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) ≡⟨ refl ⟩
103 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩
104 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) ∎
105 -}
106
107 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin
108 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩
109 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩
110 -- (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡⟨ {!!} ⟩
111 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩
112 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩
113 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩
114 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g)
115 ∎
116 deltaM-monad-law-h-3 (deltaM (delta x d)) f g = {!!}
117 {-
118 begin
119 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡⟨ {!!} ⟩
120 (deltaM-bind (deltaM-bind m f) g)
121 ∎
122 -}
123 -}