Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/monad.agda @ 104:ebd0d6e2772c
Trying redenition Delta with length constraints
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Jan 2015 23:00:05 +0900 |
parents | a271f3ff1922 |
children | 9fe3d0bd1149 |
comparison
equal
deleted
inserted
replaced
103:a271f3ff1922 | 104:ebd0d6e2772c |
---|---|
5 open import basic | 5 open import basic |
6 open import delta | 6 open import delta |
7 open import delta.functor | 7 open import delta.functor |
8 open import deltaM | 8 open import deltaM |
9 open import deltaM.functor | 9 open import deltaM.functor |
10 open import nat | |
10 open import laws | 11 open import laws |
11 | 12 |
12 module deltaM.monad where | 13 module deltaM.monad where |
13 open Functor | 14 open Functor |
14 open NaturalTransformation | 15 open NaturalTransformation |
15 open Monad | 16 open Monad |
16 | 17 |
17 | 18 |
18 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l} | 19 headDeltaM-commute : {l : Level} {A B : Set l} {n : Nat} |
19 {M : {l' : Level} -> Set l' -> Set l'} -> | |
20 {functorM : {l' : Level} -> Functor {l'} M} | |
21 {monadM : {l' : Level} -> Monad {l'} 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'} -> | 20 {M : {l' : Level} -> Set l' -> Set l'} -> |
28 {functorM : {l' : Level} -> Functor {l'} M} -> | 21 {functorM : {l' : Level} -> Functor {l'} M} -> |
29 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } -> | 22 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } -> |
30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) -> | 23 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A n) -> |
31 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x) | 24 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x) |
32 headDeltaM-commute f (deltaM (mono x)) = refl | 25 headDeltaM-commute f (deltaM (mono x)) = refl |
33 headDeltaM-commute f (deltaM (delta x d)) = refl | 26 headDeltaM-commute f (deltaM (delta x d)) = refl |
34 | 27 |
35 | 28 |
36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} | 29 {- |
37 {M : {l' : Level} -> Set l' -> Set l'} -> | 30 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} {n : Nat} |
38 {functorM : {l' : Level} -> Functor {l'} M} | 31 {M : {l' : Level} -> Set l' -> Set l'} -> |
39 {monadM : {l' : Level} -> Monad {l'} M functorM } -> | 32 {functorM : {l' : Level} -> Functor {l'} M} |
40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M | 33 {monadM : {l' : Level} -> Monad {l'} M functorM } -> |
41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM | 34 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A n) M |
42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM | 35 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} |
36 {fmap functorM} headDeltaM | |
37 | |
43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute } | 38 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute } |
39 -} | |
44 | 40 |
45 | 41 |
46 deltaM-right-unity-law : {l : Level} {A : Set l} | 42 deltaM-right-unity-law : {l : Level} {A : Set l} |
47 {M : {l' : Level} -> Set l' -> Set l'} | 43 {M : {l' : Level} -> Set l' -> Set l'} |
48 (functorM : {l' : Level} -> Functor {l'} M) | 44 (functorM : {l' : Level} -> Functor {l'} M) |
49 (monadM : {l' : Level} -> Monad {l'} M functorM) | 45 (monadM : {l' : Level} -> Monad {l'} M functorM) |
50 (d : DeltaM M {functorM} {monadM} A) -> | 46 (d : DeltaM M {functorM} {monadM} A (S O)) -> |
51 (deltaM-mu ∙ deltaM-eta) d ≡ id d | 47 (deltaM-mu ∙ deltaM-eta) d ≡ id d |
52 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin | 48 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin |
53 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ | 49 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ |
54 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ | 50 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ |
55 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩ | 51 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩ |
56 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) ≡⟨ refl ⟩ | 52 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {S O} {M}) (eta monadM (deltaM (mono x)))))) |
57 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) | 53 ≡⟨ cong (\de -> deltaM (mono (mu monadM (de)))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩ |
58 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩ | 54 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {S O} {M} {functorM} {monadM} (deltaM (mono x)))))) |
59 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x)))))) | 55 ≡⟨ refl ⟩ |
60 ≡⟨ refl ⟩ | 56 deltaM (mono (mu monadM (eta monadM x))) |
61 deltaM (mono (mu monadM (eta {l} monadM x))) | 57 ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law monadM x ) )⟩ |
62 ≡⟨ cong (\x -> deltaM (mono x)) (sym (right-unity-law monadM x)) ⟩ | |
63 deltaM (mono x) | 58 deltaM (mono x) |
64 ≡⟨ refl ⟩ | 59 ≡⟨ refl ⟩ |
65 id (deltaM (mono x)) | 60 id (deltaM (mono x)) |
66 ∎ | 61 ∎ |
67 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (delta x d)) = begin | 62 deltaM-right-unity-law functorM monadM (deltaM (delta x ())) |
68 (deltaM-mu ∙ deltaM-eta) (deltaM (delta x d)) ≡⟨ refl ⟩ | 63 -- cannot apply (mu ∙ eta) for over 2 version delta. |
69 deltaM-mu (deltaM-eta (deltaM (delta x d))) ≡⟨ refl ⟩ | 64 |
70 deltaM-mu (deltaM (mono (eta monadM (deltaM (delta x d))))) ≡⟨ refl ⟩ | 65 |
71 deltaM (mono (mu monadM (fmap functorM headDeltaM (eta monadM (deltaM (delta x d)))))) | 66 {- |
72 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (delta x d)))) ⟩ | 67 deltaM-left-unity-law : {l : Level} {A : Set l} |
73 deltaM (mono (mu monadM (eta monadM (headDeltaM (deltaM (delta x d)))))) | 68 {M : {l' : Level} -> Set l' -> Set l'} |
74 ≡⟨ refl ⟩ | 69 (functorM : {l' : Level} -> Functor {l'} M) |
75 deltaM (mono (mu monadM (eta monadM x))) | 70 (monadM : {l' : Level} -> Monad {l'} M functorM) |
76 ≡⟨ {!!} ⟩ | 71 (d : DeltaM M {functorM} {monadM} A (S O)) -> |
77 id (deltaM (delta x d)) | 72 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d |
78 ∎ | 73 deltaM-left-unity-law functorM monadM (deltaM (mono x)) = begin |
74 (deltaM-mu ∙ deltaM-fmap deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ | |
75 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ | |
76 deltaM-mu (deltaM (mono (fmap functorM deltaM-eta x))) ≡⟨ refl ⟩ | |
77 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ | |
78 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ | |
79 | |
80 id (deltaM (mono x)) | |
81 ∎ | |
82 deltaM-left-unity-law functorM monadM (deltaM (delta x ())) | |
83 -} | |
84 | |
85 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} | |
86 {M : {l' : Level} -> Set l' -> Set l'} | |
87 (functorM : {l' : Level} -> Functor {l'} M) | |
88 (monadM : {l' : Level}-> Monad {l'} M functorM) -> | |
89 Monad {l} (\A -> DeltaM M {functorM} {monadM} A n) deltaM-is-functor | |
90 deltaM-is-monad functorM monadM = record | |
91 { mu = deltaM-mu; | |
92 eta = deltaM-eta; | |
93 return = {!!}; | |
94 bind = {!!}; | |
95 association-law = {!!}; | |
96 left-unity-law = {!!}; | |
97 right-unity-law = {!!}; | |
98 eta-is-nt = {!!} | |
99 } | |
100 | |
101 | |
102 | |
103 | |
79 | 104 |
80 | 105 |
81 {- | 106 {- |
82 deltaM-association-law : {l : Level} {A : Set l} | 107 deltaM-association-law : {l : Level} {A : Set l} |
83 {M : {l' : Level} -> Set l' -> Set l'} | 108 {M : {l' : Level} -> Set l' -> Set l'} |