Mercurial > hg > Members > atton > delta_monad
changeset 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 | e6499a50ccbd |
| files | agda/delta.agda agda/delta/functor.agda agda/delta/monad.agda agda/deltaM.agda agda/deltaM/functor.agda agda/deltaM/monad.agda agda/revision.agda |
| diffstat | 7 files changed, 197 insertions(+), 134 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/delta.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/delta.agda Mon Jan 26 23:00:05 2015 +0900 @@ -1,6 +1,7 @@ open import list open import basic open import nat +open import revision open import laws open import Level @@ -9,59 +10,56 @@ module delta where +data Delta {l : Level} (A : Set l) : (Rev -> (Set l)) where + mono : A -> Delta A init + delta : {v : Rev} -> A -> Delta A v -> Delta A (commit v) -data Delta {l : Level} (A : Set l) : (Set l) where - mono : A -> Delta A - delta : A -> Delta A -> Delta A - -deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A +deltaAppend : {l : Level} {A : Set l} {n m : Rev} -> Delta A n -> Delta A m -> Delta A (merge n m) deltaAppend (mono x) d = delta x d deltaAppend (delta x d) ds = delta x (deltaAppend d ds) -headDelta : {l : Level} {A : Set l} -> Delta A -> A +headDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A n -> A headDelta (mono x) = x headDelta (delta x _) = x -tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A -tailDelta (mono x) = mono x +tailDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A (commit n) -> Delta A n tailDelta (delta _ d) = d -n-tail : {l : Level} {A : Set l} -> Nat -> ((Delta A) -> (Delta A)) -n-tail O = id -n-tail (S n) = tailDelta ∙ (n-tail n) -- Functor -delta-fmap : {l : Level} {A B : Set l} -> (A -> B) -> (Delta A) -> (Delta B) +delta-fmap : {l : Level} {A B : Set l} {n : Rev} -> (A -> B) -> (Delta A n) -> (Delta B n) delta-fmap f (mono x) = mono (f x) delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) -- Monad (Category) -delta-eta : {l : Level} {A : Set l} -> A -> Delta A -delta-eta x = mono x +delta-eta : {l : Level} {A : Set l} {v : Rev} -> A -> Delta A v +delta-eta {v = init} x = mono x +delta-eta {v = commit v} x = delta x (delta-eta {v = v} x) -delta-bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B -delta-bind (mono x) f = f x -delta-bind (delta x d) f = delta (headDelta (f x)) (delta-bind d (tailDelta ∙ f)) +delta-bind : {l : Level} {A B : Set l} {n : Rev} -> (Delta A n) -> (A -> Delta B n) -> Delta B n +delta-bind (mono x) f = f x +delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x)) -delta-mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A +delta-mu : {l : Level} {A : Set l} {n : Rev} -> (Delta (Delta A n) n) -> Delta A n delta-mu d = delta-bind d id +{- -- Monad (Haskell) -delta-return : {l : Level} {A : Set l} -> A -> Delta A +delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O) delta-return = delta-eta -_>>=_ : {l : Level} {A B : Set l} -> - (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) -(mono x) >>= f = f x -(delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f)) +_>>=_ : {l : Level} {A B : Set l} {n : Nat} -> + (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n) +d >>= f = delta-bind d f +-} - +{- -- proofs -- sub-proofs @@ -122,3 +120,4 @@ delta-fmap f (n-tail n d) ≡⟨ refl ⟩ delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩ delta-fmap f (n-tail (S n) (delta x d)) ∎ +-}
--- a/agda/delta/functor.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/delta/functor.agda Mon Jan 26 23:00:05 2015 +0900 @@ -1,28 +1,32 @@ -open import delta -open import basic -open import laws - open import Level open import Relation.Binary.PropositionalEquality +open import basic +open import delta +open import laws +open import nat +open import revision + + + module delta.functor where -- Functor-laws -- Functor-law-1 : T(id) = id' -functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (delta-fmap id) d ≡ id d +functor-law-1 : {l : Level} {A : Set l} {n : Rev} -> (d : Delta A n) -> (delta-fmap id) d ≡ id d functor-law-1 (mono x) = refl functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d) -- Functor-law-2 : T(f . g) = T(f) . T(g) -functor-law-2 : {l : Level} {A B C : Set l} -> - (f : B -> C) -> (g : A -> B) -> (d : Delta A) -> +functor-law-2 : {l : Level} {n : Rev} {A B C : Set l} -> + (f : B -> C) -> (g : A -> B) -> (d : Delta A n) -> (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d functor-law-2 f g (mono x) = refl functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) -delta-is-functor : {l : Level} -> Functor {l} Delta +delta-is-functor : {l : Level} {n : Rev} -> Functor {l} (\A -> Delta A n) delta-is-functor = record { fmap = delta-fmap ; preserve-id = functor-law-1; covariant = \f g -> functor-law-2 g f}
--- a/agda/delta/monad.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/delta/monad.agda Mon Jan 26 23:00:05 2015 +0900 @@ -3,6 +3,7 @@ open import delta.functor open import nat open import laws +open import revision open import Level @@ -13,6 +14,7 @@ -- Monad-laws (Category) +{- monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) -> n-tail n (delta-bind ds (n-tail m)) ≡ delta-bind (n-tail n ds) (n-tail (m + n)) @@ -322,14 +324,25 @@ delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩ (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎ -delta-is-monad : {l : Level} -> Monad {l} Delta delta-is-functor +-} +-- monad-law-1 : join . delta-fmap join = join . join +monad-law-1 : {l : Level} {A : Set l} {a : Rev} -> (d : Delta (Delta (Delta A a) a) a) -> + ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) +monad-law-1 (mono d) = refl +monad-law-1 (delta d ds) = {!!} + +delta-is-monad : {l : Level} {v : Rev} -> Monad {l} (\A -> Delta A v) delta-is-functor + + delta-is-monad = record { eta = delta-eta; mu = delta-mu; return = delta-eta; bind = delta-bind; - association-law = monad-law-1; - left-unity-law = monad-law-2; - right-unity-law = monad-law-2' } + association-law = monad-law-1 } +-- left-unity-law = monad-law-2; +-- right-unity-law = monad-law-2' } + +
--- a/agda/deltaM.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/deltaM.agda Mon Jan 26 23:00:05 2015 +0900 @@ -4,6 +4,7 @@ open import delta open import delta.functor open import nat +open import revision open import laws module deltaM where @@ -15,83 +16,76 @@ {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM} (A : Set l) - : Set l where - deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A + : (Rev -> Set l) where + deltaM : {v : Rev} -> Delta (M A) v -> DeltaM M {functorM} {monadM} A v -- DeltaM utils -headDeltaM : {l : Level} {A : Set l} +headDeltaM : {l : Level} {A : Set l} {v : Rev} {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> DeltaM M {functorM} {monadM} A -> M A + -> DeltaM M {functorM} {monadM} A v -> M A headDeltaM (deltaM d) = headDelta d -tailDeltaM : {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} - -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -tailDeltaM (deltaM d) = deltaM (tailDelta d) - - -appendDeltaM : {l : Level} {A : Set l} +tailDeltaM : {l : Level} {A : Set l} {v : Rev} {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) + -> DeltaM {l} M {functorM} {monadM} A (commit v) -> DeltaM M {functorM} {monadM} A v +tailDeltaM {_} {n} (deltaM d) = deltaM (tailDelta d) -checkOut : {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} - -> Nat -> DeltaM M {functorM} {monadM} A -> M A -checkOut O (deltaM (mono x)) = x -checkOut O (deltaM (delta x _)) = x -checkOut (S n) (deltaM (mono x)) = x -checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d) +appendDeltaM : {l : Level} {A : Set l} {n m : Rev} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} + -> DeltaM M {functorM} {monadM} A n -> DeltaM M {functorM} {monadM} A m -> DeltaM M {functorM} {monadM} A (merge n m) +appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) + -- functor definitions open Functor -deltaM-fmap : {l : Level} {A B : Set l} +deltaM-fmap : {l : Level} {A B : Set l} {n : Rev} {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B -deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) + -> (A -> B) -> DeltaM M {functorM} {monadM} A n -> DeltaM M {functorM} {monadM} B n +deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) + + + -- monad definitions open Monad -deltaM-eta : {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} - -> A -> (DeltaM M {functorM} {monadM} A) -deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta monadM x)) -deltaM-mu : {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} - -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) = deltaM (mono (mu monadM (fmap functorM headDeltaM x))) -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx))) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM))) - (deltaM-mu (deltaM (mono xx))) -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} monadM x headDeltaM))) - (deltaM-mu (deltaM d)) --- original deltaM-mu definitions. but it's cannot termination checking. --- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu. -{- -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM))) - (deltaM-mu (deltaM (tailDelta d))) --} +deltaM-eta : {l : Level} {A : Set l} {v : Rev} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} + -> A -> (DeltaM M {functorM} {monadM} A v) +deltaM-eta {v = init} {monadM = mm} x = deltaM (mono (eta mm x)) +deltaM-eta {v = (commit v)} {monadM = mm} x = appendDeltaM (deltaM (mono (eta mm x))) + (deltaM-eta {v = v} x) -deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'} + +deltaM-bind : {l : Level} {A B : Set l} {v : Rev} + {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B -deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d f = deltaM-mu (deltaM-fmap f d) + -> (DeltaM M {functorM} {monadM} A v) -> (A -> DeltaM M {functorM} {monadM} B v) -> DeltaM M {functorM} {monadM} B v +deltaM-bind {v = init} {monadM = mm} (deltaM (mono x)) f = deltaM (mono (bind mm x (headDeltaM ∙ f))) +deltaM-bind {v = commit v} {monadM = mm} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind mm x (headDeltaM ∙ f)))) + (deltaM-bind (deltaM d) (tailDeltaM ∙ f)) + + +deltaM-mu : {l : Level} {A : Set l} {v : Rev} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} + -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A v) v) -> DeltaM M {functorM} {monadM} A v +deltaM-mu d = deltaM-bind d id
--- a/agda/deltaM/functor.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/deltaM/functor.agda Mon Jan 26 23:00:05 2015 +0900 @@ -6,17 +6,19 @@ open import delta open import delta.functor open import deltaM +open import nat +open import revision open import laws open Functor module deltaM.functor where -deltaM-preserve-id : {l : Level} {A : Set l} +deltaM-preserve-id : {l : Level} {A : Set l} {n : Rev} {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) -> deltaM-fmap id d ≡ id d + -> (d : DeltaM M {functorM} {monadM} A n) -> deltaM-fmap id d ≡ id d deltaM-preserve-id functorM (deltaM (mono x)) = begin deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ @@ -42,11 +44,11 @@ ∎ -deltaM-covariant : {l : Level} {A B C : Set l} -> +deltaM-covariant : {l : Level} {A B C : Set l} {n : Rev} -> {M : {l' : Level} -> Set l' -> Set l'} (functorM : {l' : Level} -> Functor {l'} M) {monadM : {l' : Level} -> Monad {l'} M functorM} - (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) -> + (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A n) -> (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d deltaM-covariant functorM f g (deltaM (mono x)) = begin deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ @@ -79,10 +81,11 @@ ∎ -deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'} +deltaM-is-functor : {l : Level} {n : Rev} + {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M } {monadM : {l' : Level} -> Monad {l'} M functorM} - -> Functor {l} (DeltaM M {functorM} {monadM}) -deltaM-is-functor {_} {_} {functorM} = record { fmap = deltaM-fmap ; - preserve-id = deltaM-preserve-id functorM ; - covariant = (\f g -> deltaM-covariant functorM g f)} \ No newline at end of file + -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A n) +deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; + preserve-id = deltaM-preserve-id functorM ; + covariant = (\f g -> deltaM-covariant functorM g f)}
--- 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 = {!!} + } + + + + {-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/revision.agda Mon Jan 26 23:00:05 2015 +0900 @@ -0,0 +1,25 @@ +open import Relation.Binary.PropositionalEquality +module revision where + +data Rev : Set where + init : Rev + commit : Rev -> Rev + +merge : Rev -> Rev -> Rev +merge init b = commit b +merge (commit a) b = commit (merge a b) + +tip : Rev -> Rev -> Rev +tip init init = init +tip init (commit b) = commit b +tip (commit a) init = commit a +tip (commit a) (commit b) = commit (tip a b) + +open ≡-Reasoning + +same-tip : (a : Rev) -> tip a a ≡ a +same-tip init = refl +same-tip (commit v) = begin + tip (commit v) (commit v) ≡⟨ refl ⟩ + commit (tip v v) ≡⟨ cong commit (same-tip v) ⟩ + commit v ∎