-
Notifications
You must be signed in to change notification settings - Fork 15
/
ex9.txt
149 lines (132 loc) · 2.88 KB
/
ex9.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
1. pure id <*> x = x
2. pure (g x) = pure g <*> pure x
3. x <*> pure y = pure (\g -> g y) <*> x
4. x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z
pure = Just
Nothing <*> _ = Nothing
(Just g) <*> mx = fmap g mx
fmap id = id
fmap (g . h) = fmap g . fmap h
fmap :: (a -> b) -> Maybe a -> Maybe b
fmap g Nothing = Nothing
fmap g (Just a) = Just (g a)
Proof of 1. pure id <*> x = x
case Nothing:
pure id <*> Nothing
= {applying pure}
Just id <*> Nothing
= {applying <*>}
fmap id Nothing
= {applying fmap}
Nothing
case Just:
pure id <*> Just x
= {applying pure}
Just id <*> Just x
= {applying <*>}
fmap id (Just x)
= {applying fmap}
Just (id x)
= {applying id}
Just x
Proof of 2. pure (g x) = pure g <*> pure x
case Nothing:
pure (g Nothing)
= {applying pure}
Just (g Nothing)
= {unapplying fmap}
fmap g (Just Nothing)
= {unapplying <*>}
Just g <*> Just Nothing
= {unapplying pure}
pure g <*> pure Nothing
case Just:
pure (g (Just a))
= {applying pure}
Just (g (Just a))
= {unapplying fmap}
fmap g (Just (Just a))
= {unapplying <*>}
Just g <*> Just (Just a)
= {unapplying pure}
pure g <*> pure (Just a)
Proof of 3. x <*> pure y = pure (\g -> g y) <*> x
case Nothing:
Nothing <*> pure y
= {applying <*>}
Nothing
= {unapplying fmap}
fmap (\g -> g y) Nothing
= {unapplying <*>}
Just (\g -> g y) <*> Nothing
= {unapplying pure}
pure (\g -> g y) <*> Nothing
case Just:
Just a <*> pure y
= {applying <*>}
fmap a (pure y)
= {applying pure}
fmap a (Just y)
= {applying fmap}
Just (a y)
= {unapplying (\g -> g y)}
Just ((\g -> g y) a)
= {unapplying fmap}
fmap (\g -> g y) (Just a)
= {unapplying <*>}
Just (\g -> g y) <*> Just a
= {unapplying pure}
pure (\g -> g y) <*> Just a
Proof of 4. x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z
case Nothing:
Nothing <*> (y <*> z)
= {applying <*>}
Nothing
= {unapplying <*>}
Nothing <*> z
= {unapplying <*>}
(Nothing <*> y) <*> z
= {unapplying fmap}
((fmap . Nothing) <*> y) <*> z
= {unapplying <*>}
(Just (.) <*> Nothing <*> y) <*> z
= {unapplying pure}
(pure (.) <*> Nothing <*> y) <*> z
case Just a, Nothing:
(Just a) <*> (Nothing <*> z)
= {applying <*>}
fmap a (Nothing <*> z)
= {applicative <*>}
fmap a Nothing
= {applying fmap}
Nothing
= {unapplying <*>}
Nothing <*> z
= {unapplying fmap}
fmap (. a) Nothing <*> z
= {unapplying <*>}
(Just (. a) <*> Nothing) <*> z
= {unapplying fmap}
((fmap . (Just a)) <*> Nothing) <*> z
= {unapplying <*>}
(Just (.) <*> (Just a) <*> Nothing) <*> z
= {unapplying pure}
(pure (.) <*> (Just a) <*> Nothing) <*> z
case Just a, Just b:
(Just a) <*> ((Just b) <*> z)
= {applying <*>}
fmap a ((Just b) <*> z)
= {applying <*>}
fmap a (fmap b z)
= {unapplying .}
fmap (a . b) z
= {unapplying <*>}
Just (a . b) <*> z
= {unapplying applicative property 3}
(Just (. a) <*> (Just b)) <*> z
= {unapplying fmap}
((fmap . (Just a)) <*> (Just b)) <*> z
= {unapplying <*>}
(Just (.) <*> (Just a) <*> (Just b)) <*> z
= {unapplying pure}
(pure (.) <*> (Just a) <*> (Just b)) <*> z