Mercurial > hg > Members > atton > delta_monad
annotate delta.hs @ 79:7307e43a3c76
Prove monad-law-4
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 01 Dec 2014 17:25:59 +0900 |
parents | 0ad0ae7a3cbe |
children | 1339772b2e36 |
rev | line source |
---|---|
17
279ebcf670c4
Define Similar as Applicative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
16
diff
changeset
|
1 import Control.Applicative |
18
c77397d0677f
Try define Similar as Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
2 import Data.Numbers.Primes -- $ cabal install primes |
c77397d0677f
Try define Similar as Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
3 |
58 | 4 -- delta definition |
5 | |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
6 data Delta a = Mono a | Delta a (Delta a) deriving Show |
17
279ebcf670c4
Define Similar as Applicative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
16
diff
changeset
|
7 |
73
0ad0ae7a3cbe
Proving monad-law-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
8 instance (Eq a) => Eq (Delta a) where |
0ad0ae7a3cbe
Proving monad-law-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
9 (Mono x) == (Mono y) = x == y |
0ad0ae7a3cbe
Proving monad-law-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
10 (Mono _) == (Delta _ _) = False |
0ad0ae7a3cbe
Proving monad-law-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
11 (Delta x xs) == (Delta y ys) = (x == y) && (xs == ys) |
0ad0ae7a3cbe
Proving monad-law-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
12 |
58 | 13 -- basic functions |
14 | |
52
69a01cc80075
Define Delta for Infinite changes in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
15 deltaAppend :: Delta a -> Delta a -> Delta a |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
16 deltaAppend (Mono x) d = Delta x d |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
17 deltaAppend (Delta x d) ds = Delta x (deltaAppend d ds) |
47
1aefea69f71b
Implement bubble sort by delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
46
diff
changeset
|
18 |
69
295e8ed39c0c
Change headDelta definition. return non-delta value
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
19 headDelta :: Delta a -> a |
295e8ed39c0c
Change headDelta definition. return non-delta value
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
20 headDelta (Mono x) = x |
295e8ed39c0c
Change headDelta definition. return non-delta value
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
21 headDelta (Delta x _) = x |
14
116131b196bb
Define fmap and mu
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
22 |
52
69a01cc80075
Define Delta for Infinite changes in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
23 tailDelta :: Delta a -> Delta a |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
24 tailDelta d@(Mono _) = d |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
25 tailDelta (Delta _ ds) = ds |
18
c77397d0677f
Try define Similar as Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
26 |
58 | 27 -- instance definitions |
28 | |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
29 instance Functor Delta where |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
30 fmap f (Mono x) = Mono (f x) |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
31 fmap f (Delta x d) = Delta (f x) (fmap f d) |
18
c77397d0677f
Try define Similar as Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
32 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
33 instance Applicative Delta where |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
34 pure f = Mono f |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
35 (Mono f) <*> (Mono x) = Mono (f x) |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
36 df@(Mono f) <*> (Delta x d) = Delta (f x) (df <*> d) |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
37 (Delta f df) <*> d@(Mono x) = Delta (f x) (df <*> d) |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
38 (Delta f df) <*> (Delta x d) = Delta (f x) (df <*> d) |
52
69a01cc80075
Define Delta for Infinite changes in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
39 |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
40 bind :: (Delta a) -> (a -> Delta b) -> (Delta b) |
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
41 bind (Mono x) f = f x |
69
295e8ed39c0c
Change headDelta definition. return non-delta value
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
42 bind (Delta x d) f = Delta (headDelta (f x)) (bind d (tailDelta . f)) |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
43 |
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
44 mu :: (Delta (Delta a)) -> (Delta a) |
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
45 mu d = bind d id |
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
46 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
47 instance Monad Delta where |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
48 return x = Mono x |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
49 d >>= f = mu $ fmap f d |
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
58
diff
changeset
|
50 |
58 | 51 |
52 | |
53 -- utils | |
18
c77397d0677f
Try define Similar as Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
54 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
55 returnS :: (Show s) => s -> Delta s |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
53
diff
changeset
|
56 returnS x = Mono x |
0
7a82a5e50499
Initial commit. define to Functor for Similer
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
58 returnSS :: (Show s) => s -> s -> Delta s |
52
69a01cc80075
Define Delta for Infinite changes in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
59 returnSS x y = (returnS x) `deltaAppend` (returnS y) |
69a01cc80075
Define Delta for Infinite changes in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
60 |
58 | 61 deltaFromList :: [a] -> Delta a |
62 deltaFromList = (foldl1 deltaAppend) . (fmap return) | |
63 | |
23
b4d3960af901
Define similar constructor for different element
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
22
diff
changeset
|
64 |
16
4b315cf0edb9
Improve mu definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
65 -- samples |
3
3c5fbce357af
Define >>= for Similer
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
66 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
67 generator :: Int -> Delta [Int] |
21
af8754322ed4
Define Similar sample
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
20
diff
changeset
|
68 generator x = let intList = [1..x] in |
22
f0400c4c953f
Imporve Similar definition. delete "Single" constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
69 returnS intList |
6 | 70 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
71 primeFilter :: [Int] -> Delta [Int] |
21
af8754322ed4
Define Similar sample
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
20
diff
changeset
|
72 primeFilter xs = let primeList = filter isPrime xs |
23
b4d3960af901
Define similar constructor for different element
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
22
diff
changeset
|
73 refactorList = filter even xs in |
b4d3960af901
Define similar constructor for different element
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
22
diff
changeset
|
74 returnSS primeList refactorList |
11
e8a5df54480e
Define sample for Monad style
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
75 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
76 count :: [Int] -> Delta Int |
21
af8754322ed4
Define Similar sample
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
20
diff
changeset
|
77 count xs = let primeCount = length xs in |
22
f0400c4c953f
Imporve Similar definition. delete "Single" constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
78 returnS primeCount |
15 | 79 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
80 primeCount :: Int -> Delta Int |
21
af8754322ed4
Define Similar sample
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
20
diff
changeset
|
81 primeCount x = generator x >>= primeFilter >>= count |
46
cb5c190aa45d
Define bubble sort
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
45
diff
changeset
|
82 |
cb5c190aa45d
Define bubble sort
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
45
diff
changeset
|
83 bubbleSort :: [Int] -> Delta [Int] |
48
820af7cc8485
Wrote >>= style bubble sort
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
47
diff
changeset
|
84 bubbleSort [] = returnS [] |
49
d654fdecdcd0
Wrote bubble sort with modified calculate
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
85 bubbleSort xs = bubbleSort remainValue >>= (\xs -> returnSS (sortedValueL : xs) |
d654fdecdcd0
Wrote bubble sort with modified calculate
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
86 (sortedValueR ++ xs)) |
46
cb5c190aa45d
Define bubble sort
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
45
diff
changeset
|
87 where |
51 | 88 maximumValue = maximum xs |
89 sortedValueL = maximumValue | |
90 sortedValueR = replicate (length $ filter (== maximumValue) xs) maximumValue | |
91 remainValue = filter (/= maximumValue) xs |