Mercurial > hg > Members > atton > delta_monad
diff 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 |
line wrap: on
line diff
--- a/agda/deltaM/monad.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/deltaM/monad.agda Mon Jan 26 23:00:05 2015 +0900 @@ -7,6 +7,7 @@ open import delta.functor open import deltaM open import deltaM.functor +open import nat open import laws module deltaM.monad where @@ -15,67 +16,91 @@ open Monad -postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} -> - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M (functorM ) } -> - NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A) - {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}} - (deltaM-mu {_} {_} {M} {functorM} {monadM}) - -headDeltaM-commute : {l : Level} {A B : Set l} +headDeltaM-commute : {l : Level} {A B : Set l} {n : Nat} {M : {l' : Level} -> Set l' -> Set l'} -> {functorM : {l' : Level} -> Functor {l'} M} -> {monadM : {l' : Level} -> Monad {l'} M (functorM ) } -> - (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) -> + (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A n) -> headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x) headDeltaM-commute f (deltaM (mono x)) = refl headDeltaM-commute f (deltaM (delta x d)) = refl -headDeltaM-is-natural-transformation : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} -> - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM } -> - NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M - {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM --- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM +{- +headDeltaM-is-natural-transformation : {l : Level} {A : Set l} {n : Nat} + {M : {l' : Level} -> Set l' -> Set l'} -> + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM } -> + NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A n) M + {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} + {fmap functorM} headDeltaM + headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute } +-} -deltaM-right-unity-law : {l : Level} {A : Set l} +deltaM-right-unity-law : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'} (functorM : {l' : Level} -> Functor {l'} M) (monadM : {l' : Level} -> Monad {l'} M functorM) - (d : DeltaM M {functorM} {monadM} A) -> + (d : DeltaM M {functorM} {monadM} A (S O)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d -deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin +deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩ - deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) ≡⟨ refl ⟩ - deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) - ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩ - deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x)))))) - ≡⟨ refl ⟩ - deltaM (mono (mu monadM (eta {l} monadM x))) - ≡⟨ cong (\x -> deltaM (mono x)) (sym (right-unity-law monadM x)) ⟩ + deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {S O} {M}) (eta monadM (deltaM (mono x)))))) + ≡⟨ cong (\de -> deltaM (mono (mu monadM (de)))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩ + deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {S O} {M} {functorM} {monadM} (deltaM (mono x)))))) + ≡⟨ refl ⟩ + deltaM (mono (mu monadM (eta monadM x))) + ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law monadM x ) )⟩ deltaM (mono x) ≡⟨ refl ⟩ id (deltaM (mono x)) ∎ -deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (delta x d)) = begin - (deltaM-mu ∙ deltaM-eta) (deltaM (delta x d)) ≡⟨ refl ⟩ - deltaM-mu (deltaM-eta (deltaM (delta x d))) ≡⟨ refl ⟩ - deltaM-mu (deltaM (mono (eta monadM (deltaM (delta x d))))) ≡⟨ refl ⟩ - deltaM (mono (mu monadM (fmap functorM headDeltaM (eta monadM (deltaM (delta x d)))))) - ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (delta x d)))) ⟩ - deltaM (mono (mu monadM (eta monadM (headDeltaM (deltaM (delta x d)))))) - ≡⟨ refl ⟩ - deltaM (mono (mu monadM (eta monadM x))) - ≡⟨ {!!} ⟩ - id (deltaM (delta x d)) - ∎ +deltaM-right-unity-law functorM monadM (deltaM (delta x ())) +-- cannot apply (mu ∙ eta) for over 2 version delta. + + +{- +deltaM-left-unity-law : {l : Level} {A : Set l} + {M : {l' : Level} -> Set l' -> Set l'} + (functorM : {l' : Level} -> Functor {l'} M) + (monadM : {l' : Level} -> Monad {l'} M functorM) + (d : DeltaM M {functorM} {monadM} A (S O)) -> + (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d +deltaM-left-unity-law functorM monadM (deltaM (mono x)) = begin + (deltaM-mu ∙ deltaM-fmap deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ + deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap functorM deltaM-eta x))) ≡⟨ refl ⟩ + deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ + deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ + + id (deltaM (mono x)) + ∎ +deltaM-left-unity-law functorM monadM (deltaM (delta x ())) +-} + +deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} + {M : {l' : Level} -> Set l' -> Set l'} + (functorM : {l' : Level} -> Functor {l'} M) + (monadM : {l' : Level}-> Monad {l'} M functorM) -> + Monad {l} (\A -> DeltaM M {functorM} {monadM} A n) deltaM-is-functor +deltaM-is-monad functorM monadM = record + { mu = deltaM-mu; + eta = deltaM-eta; + return = {!!}; + bind = {!!}; + association-law = {!!}; + left-unity-law = {!!}; + right-unity-law = {!!}; + eta-is-nt = {!!} + } + + + + {-