Mercurial > hg > Members > atton > delta_monad
changeset 143:f241d521bf65
Merge
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Feb 2015 14:36:02 +0900 |
| parents | 861e35665469 (diff) 3bbb68f0a1e3 (current diff) |
| children | 575de2e38385 |
| files | haskell/Delta.hs |
| diffstat | 7 files changed, 199 insertions(+), 134 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgignore Sun Feb 15 17:34:52 2015 +0900 +++ b/.hgignore Wed Feb 25 14:36:02 2015 +0900 @@ -1,5 +1,7 @@ syntax: glob +.DS_Store + *.swp *.*~ *.agdai
--- a/agda/delta.agda Sun Feb 15 17:34:52 2015 +0900 +++ b/agda/delta.agda Wed Feb 25 14:36:02 2015 +0900 @@ -54,4 +54,4 @@ (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n) d >>= f = delta-bind d f --} \ No newline at end of file +-}
--- a/agda/delta/monad.agda Sun Feb 15 17:34:52 2015 +0900 +++ b/agda/delta/monad.agda Wed Feb 25 14:36:02 2015 +0900 @@ -10,11 +10,6 @@ module delta.monad where -tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} - (f : A -> B) -> (d : Delta A (S (S n))) -> - (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d -tailDelta-is-nt f (delta x d) = refl - tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat) (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) -> @@ -40,7 +35,6 @@ delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) delta-eta-is-nt {n = O} f x = refl -delta-eta-is-nt {n = S O} f x = refl delta-eta-is-nt {n = S n} f x = begin (delta-eta ∙ f) x ≡⟨ refl ⟩ delta-eta (f x) ≡⟨ refl ⟩ @@ -75,10 +69,10 @@ (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ∎ -delta-fmap-mu-to-tail (S n) (S n₁) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin +delta-fmap-mu-to-tail (S n) (S m) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) (delta-fmap tailDelta (delta-fmap delta-mu dds)) - ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S n₁) dds) ⟩ + ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S m) dds) ⟩ delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds))) ∎ @@ -89,7 +83,7 @@ -- association-law : join . delta-fmap join = join . join delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) -delta-association-law {n = O} (mono d) = refl +delta-association-law {n = O} (mono d) = refl delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
--- a/haskell/Delta.hs Sun Feb 15 17:34:52 2015 +0900 +++ b/haskell/Delta.hs Wed Feb 25 14:36:02 2015 +0900 @@ -1,6 +1,7 @@ +module Delta ( Delta(..) , deltaAppend , headDelta , tailDelta , deltaFromList) where + import Control.Applicative -import Control.Monad.Writer -import Data.Numbers.Primes -- $ cabal install primes + -- Delta definition @@ -51,127 +52,5 @@ -- utils -returnDD :: (Show s) => s -> s -> Delta s -returnDD x y = (return x) `deltaAppend` (return y) - deltaFromList :: [a] -> Delta a deltaFromList = (foldl1 deltaAppend) . (fmap return) - - --- samples - -generator :: Int -> Delta [Int] -generator x = let intList = [1..x] in - return intList - -primeFilter :: [Int] -> Delta [Int] -primeFilter xs = let primeList = filter isPrime xs - refactorList = filter even xs in - returnDD primeList refactorList - -count :: [Int] -> Delta Int -count xs = let primeCount = length xs in - return primeCount - -primeCount :: Int -> Delta Int -primeCount x = generator x >>= primeFilter >>= count - -bubbleSort :: [Int] -> Delta [Int] -bubbleSort [] = return [] -bubbleSort xs = bubbleSort remainValue >>= (\xs -> returnDD (sortedValueL : xs) - (sortedValueR ++ xs)) - where - maximumValue = maximum xs - sortedValueL = maximumValue - sortedValueR = replicate (length $ filter (== maximumValue) xs) maximumValue - remainValue = filter (/= maximumValue) xs - - - --- DeltaM definition (Delta with Monad) - -data DeltaM m a = DeltaM (Delta (m a)) deriving (Show) - - --- DeltaM utils - -unDeltaM :: DeltaM m a -> Delta (m a) -unDeltaM (DeltaM d) = d - -headDeltaM :: DeltaM m a -> m a -headDeltaM (DeltaM d) = headDelta d - -tailDeltaM :: DeltaM m a -> DeltaM m a -tailDeltaM (DeltaM d) = DeltaM $ tailDelta d - -appendDeltaM :: DeltaM m a -> DeltaM m a -> DeltaM m a -appendDeltaM (DeltaM d) (DeltaM dd) = DeltaM (deltaAppend d dd) - -checkOut :: Int -> DeltaM m a -> m a -checkOut 0 (DeltaM (Mono x)) = x -checkOut 0 (DeltaM (Delta x _)) = x -checkOut n (DeltaM (Mono x)) = x -checkOut n (DeltaM (Delta _ d)) = checkOut (n-1) (DeltaM d) - - --- DeltaM instance definitions - -instance (Functor m) => Functor (DeltaM m) where - fmap f (DeltaM d) = DeltaM $ fmap (fmap f) d - -instance (Applicative m) => Applicative (DeltaM m) where - pure f = DeltaM $ Mono $ pure f - (DeltaM (Mono f)) <*> (DeltaM (Mono x)) = DeltaM $ Mono $ f <*> x - df@(DeltaM (Mono f)) <*> (DeltaM (Delta x d)) = appendDeltaM (DeltaM $ Mono $ f <*> x) (df <*> (DeltaM d)) - (DeltaM (Delta f df)) <*> dx@(DeltaM (Mono x)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> dx) - (DeltaM (Delta f df)) <*> (DeltaM (Delta x dx)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> (DeltaM dx)) - - -mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a -mu' d@(DeltaM (Mono _)) = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d -mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d) - (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d)))) - -instance (Functor m, Monad m) => Monad (DeltaM m) where - return x = DeltaM $ Mono $ return x - d >>= f = mu' $ fmap f d - - - --- DeltaM examples - --- DeltaM example utils -type DeltaLog = Writer [String] -type DeltaWithLog = DeltaM DeltaLog - -returnW :: (Show a) => a -> DeltaLog a -returnW x = do tell $ [show x] - return x - -dmap :: (m a -> b) -> DeltaM m a -> Delta b -dmap f (DeltaM d) = fmap f d - -deltaWithLogFromList :: (Show a) => [a] -> DeltaWithLog a -deltaWithLogFromList xs = DeltaM $ deltaFromList $ fmap returnW xs - - --- example : prime filter --- usage : runWriter $ checkOut 0 $ primeCountM 30 -- run specific version --- : dmap runWriter $ primeCountM 30 -- run all version - -generatorM :: Int -> DeltaWithLog [Int] -generatorM x = let intList = [1..x] in - DeltaM $ deltaFromList $ fmap returnW $ replicate 2 intList - -primeFilterM :: [Int] -> DeltaWithLog [Int] -primeFilterM xs = let primeList = filter isPrime xs - refactorList = filter even xs in - DeltaM $ deltaFromList $ fmap returnW [primeList, refactorList] - - -countM :: [Int] -> DeltaWithLog Int -countM xs = let primeCount = length xs in - DeltaM $ deltaFromList $ fmap returnW $ replicate 2 primeCount - -primeCountM :: Int -> DeltaWithLog Int -primeCountM x = generatorM x >>= primeFilterM >>= countM
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/haskell/DeltaM.hs Wed Feb 25 14:36:02 2015 +0900 @@ -0,0 +1,56 @@ +module DeltaM (DeltaM(..), unDeltaM, appendDeltaM, tailDeltaM, headDeltaM, checkOut) where + +import Control.Applicative +import Delta + + +-- DeltaM definition (Delta with Monad) + +data DeltaM m a = DeltaM (Delta (m a)) deriving (Show) + + +-- DeltaM utils + +unDeltaM :: DeltaM m a -> Delta (m a) +unDeltaM (DeltaM d) = d + +headDeltaM :: DeltaM m a -> m a +headDeltaM (DeltaM d) = headDelta d + +tailDeltaM :: DeltaM m a -> DeltaM m a +tailDeltaM (DeltaM d) = DeltaM $ tailDelta d + +appendDeltaM :: DeltaM m a -> DeltaM m a -> DeltaM m a +appendDeltaM (DeltaM d) (DeltaM dd) = DeltaM (deltaAppend d dd) + +checkOut :: Int -> DeltaM m a -> m a +checkOut 0 (DeltaM (Mono x)) = x +checkOut 0 (DeltaM (Delta x _)) = x +checkOut n (DeltaM (Mono x)) = x +checkOut n (DeltaM (Delta _ d)) = checkOut (n-1) (DeltaM d) + + +-- DeltaM instance definitions + +instance (Functor m) => Functor (DeltaM m) where + fmap f (DeltaM d) = DeltaM $ fmap (fmap f) d + +instance (Applicative m) => Applicative (DeltaM m) where + pure f = DeltaM $ Mono $ pure f + (DeltaM (Mono f)) <*> (DeltaM (Mono x)) = DeltaM $ Mono $ f <*> x + df@(DeltaM (Mono f)) <*> (DeltaM (Delta x d)) = appendDeltaM (DeltaM $ Mono $ f <*> x) (df <*> (DeltaM d)) + (DeltaM (Delta f df)) <*> dx@(DeltaM (Mono x)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> dx) + (DeltaM (Delta f df)) <*> (DeltaM (Delta x dx)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> (DeltaM dx)) + + +mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a +mu' d@(DeltaM (Mono _)) = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d +mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d) + (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d)))) + +instance (Functor m, Monad m) => Monad (DeltaM m) where + return x = DeltaM $ Mono $ return x + d >>= f = mu' $ fmap f d + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/haskell/Example/Delta.hs Wed Feb 25 14:36:02 2015 +0900 @@ -0,0 +1,47 @@ +module Example.Delta where + +import Data.Numbers.Primes +import Delta + +-- examples + +generator :: Int -> Delta [Int] +generator x = let intList = [1..x] in + return intList + +numberFilter :: [Int] -> Delta [Int] +numberFilter xs = let primeList = filter isPrime xs + evenList = filter even xs in + Delta evenList (Mono primeList) + +count :: [Int] -> Delta Int +count xs = let primeCount = length xs in + return primeCount + +numberCount :: Int -> Delta Int +numberCount x = generator x >>= numberFilter >>= count + +sort :: [Int] -> Delta [Int] +sort xs = deltaFromList [ bubbleSort xs, + singleSort xs, + swapPair xs, + identity, + nil + ] + where + nil = [] + identity = xs + + swapPair [] = [] + swapPair [x] = [x] + swapPair (x:xx:xs) = (min x xx) : (max x xx) : xs + + singleSort [] = [] + singleSort xs = (minimum xs) : (singleSort (filter (/= (minimum xs)) xs)) + + bubbleSort [] = [] + bubbleSort xs = let + minVal = minimum xs + minVals = replicate (length (filter (== minVal) xs)) minVal + in + minVals ++ (bubbleSort (filter (/= (minimum xs)) xs))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/haskell/Example/DeltaM.hs Wed Feb 25 14:36:02 2015 +0900 @@ -0,0 +1,87 @@ +module Example.DeltaM where + +import Control.Monad.Writer +import Data.Numbers.Primes -- $ cabal install primes + +import Delta +import DeltaM + + +-- DeltaM examples + +-- DeltaM example utils +type DeltaLog = Writer [String] +type DeltaWithLog = DeltaM DeltaLog + +returnW :: (Show a) => a -> DeltaLog a +returnW x = do tell $ [show x] + return x + +dmap :: (m a -> b) -> DeltaM m a -> Delta b +dmap f (DeltaM d) = fmap f d + +deltaWithLogFromList :: (Show a) => [a] -> DeltaWithLog a +deltaWithLogFromList xs = DeltaM $ deltaFromList $ fmap returnW xs + + +-- example : prime filter +-- usage : runWriter $ checkOut 0 $ numberCountM 30 -- run specific version +-- : dmap runWriter $ numberCountM 30 -- run all version + +generatorM :: Int -> DeltaWithLog [Int] +generatorM x = let intList = [1..x] in + DeltaM $ deltaFromList $ fmap returnW $ replicate 2 intList + +numberFilterM :: [Int] -> DeltaWithLog [Int] +numberFilterM xs = let primeList = filter isPrime xs + evenList = filter even xs in + DeltaM $ deltaFromList $ fmap returnW [primeList, evenList] + + +countM :: [Int] -> DeltaWithLog Int +countM xs = let numberCount = length xs in + DeltaM $ deltaFromList $ fmap returnW $ replicate 2 numberCount + +numberCountM :: Int -> DeltaWithLog Int +numberCountM x = generatorM x >>= numberFilterM >>= countM + + +-- example : sort + +sort :: [Int] -> DeltaWithLog [Int] +sort xs = DeltaM $ deltaFromList [ --bubbleSort xs, + singleSort xs, + returnW $ swapPair xs, + identity, + nil + ] + where + nil = returnW [] + + identity = returnW xs + + swapPair [] = [] + swapPair [x] = [x] + swapPair (x:xx:xs) = (min x xx) : (max x xx) : xs + + singleSort [] = returnW [] + singleSort xs = do + tell [show xs] + res <- do + remanVals <- singleSort $ filter (/= (minimum xs)) xs + return $ (minimum xs) : remanVals + tell [ show res ] + return res + + bubbleSort [] = returnW [] + bubbleSort xs = let + minVal = minimum xs + minVals = replicate (length (filter (== minVal) xs)) minVal + in + do + tell [show xs] + res <- do + remainVals <- bubbleSort $ filter (/= minVal) xs + return $ minVals ++ remainVals + tell [show res] + return res