this repo has no description
final
+34
-38
+34
-38
logical-equivalences-in-haskell.ipynb
+34
-38
logical-equivalences-in-haskell.ipynb
···
7
7
"---\n",
8
8
"title: \"Logical equivalences in Haskell\"\n",
9
9
"published: 2019-01-03\n",
10
-
"tags: technology haskell\n",
10
+
"tags: technology , haskell\n",
11
11
"link: \n",
12
12
"---"
13
-
]
14
-
},
15
-
{
16
-
"cell_type": "markdown",
17
-
"metadata": {},
18
-
"source": [
19
-
"\n"
20
13
]
21
14
},
22
15
{
···
34
27
"cell_type": "markdown",
35
28
"metadata": {},
36
29
"source": [
37
-
"\n"
38
-
]
39
-
},
40
-
{
41
-
"cell_type": "markdown",
42
-
"metadata": {},
43
-
"source": [
44
30
"Let's set some language pragmas"
45
31
]
46
32
},
47
33
{
48
34
"cell_type": "code",
49
-
"execution_count": 1,
35
+
"execution_count": 2,
50
36
"metadata": {},
51
37
"outputs": [],
52
38
"source": [
···
66
52
},
67
53
{
68
54
"cell_type": "code",
69
-
"execution_count": 2,
55
+
"execution_count": 3,
70
56
"metadata": {},
71
57
"outputs": [],
72
58
"source": [
···
87
73
},
88
74
{
89
75
"cell_type": "code",
90
-
"execution_count": 3,
76
+
"execution_count": 4,
91
77
"metadata": {},
92
78
"outputs": [],
93
79
"source": [
···
99
85
"cell_type": "markdown",
100
86
"metadata": {},
101
87
"source": [
102
-
"\n"
103
-
]
104
-
},
105
-
{
106
-
"cell_type": "markdown",
107
-
"metadata": {},
108
-
"source": [
109
88
"And now the propositions..."
110
89
]
111
90
},
112
91
{
113
92
"cell_type": "code",
114
-
"execution_count": 4,
93
+
"execution_count": 5,
115
94
"metadata": {},
116
95
"outputs": [],
117
96
"source": [
···
135
114
},
136
115
{
137
116
"cell_type": "code",
138
-
"execution_count": 5,
117
+
"execution_count": 6,
139
118
"metadata": {},
140
119
"outputs": [],
141
120
"source": [
···
162
141
},
163
142
{
164
143
"cell_type": "code",
165
-
"execution_count": 6,
144
+
"execution_count": 12,
166
145
"metadata": {},
167
146
"outputs": [],
168
147
"source": [
169
148
"-- forall. P,Q. - (P /\\ Q) -> (P -> - Q)\n",
170
-
"import Control.Applicative (liftA2)\n",
149
+
"import Control.Applicative (liftA2)\n",
171
150
"\n",
172
151
"newtype Prop3 m = \n",
173
152
" Prop3\n",
···
177
156
"-- proof, Prop3 <==> LEM\n",
178
157
"instance Monad m => Proof.Iso (Prop3 m) (Lem m) where\n",
179
158
" to :: Prop3 m -> Lem m\n",
180
-
" to (Prop3 p) = Lem $ fmap Right $ proof >>= (\\f -> pure (liftA2 (>>=) f (flip id))) where\n",
181
-
" proof :: m (a -> m (a -> m Void))\n",
182
-
" proof = p (\\(x,y) -> proof >>= (($ y) =<<) . ($ x))\n",
159
+
" to (Prop3 p) = Lem \n",
160
+
" $ fmap Right \n",
161
+
" $ proof \n",
162
+
" >>= \n",
163
+
" (\\f -> pure (liftA2 (>>=) f (flip id))) \n",
164
+
" where\n",
165
+
" proof :: m (a -> m (a -> m Void))\n",
166
+
" proof = p (\\(x,y) -> proof >>= (($ y) =<<) . ($ x))\n",
183
167
" \n",
184
168
" from :: Lem m -> Prop3 m\n",
185
-
" from (Lem l) = Prop3 $ (\\f -> pure (\\a -> either (const . f . (a ,)) id <$> l))"
169
+
" from (Lem l) = Prop3\n",
170
+
" $ (\\f ->\n",
171
+
" pure\n",
172
+
" $ \\a ->\n",
173
+
" either (const . f . (a ,)) id <$> l)"
186
174
]
187
175
},
188
176
{
189
177
"cell_type": "code",
190
-
"execution_count": 7,
178
+
"execution_count": 10,
191
179
"metadata": {},
192
180
"outputs": [],
193
181
"source": [
194
-
"import Proof\n",
195
182
"-- forall. P,Q. -P /\\ -Q -> - (P \\/ Q)\n",
196
183
"\n",
197
184
"newtype Prop4 m = \n",
···
202
189
"-- proof, Prop4 <==> LEM\n",
203
190
"instance Monad m => Proof.Iso (Prop4 m) (Lem m) where\n",
204
191
" to :: Prop4 m -> Lem m\n",
205
-
" to (Prop4 p) = Lem $ pure $ Right ((proof >>=) . flip id . Left) where\n",
206
-
" proof :: m (Either a a -> m Void)\n",
207
-
" proof = curry p ((proof >>=) . flip id . Left) ((proof >>=) . flip id . Right)\n",
192
+
" to (Prop4 p) = Lem \n",
193
+
" $ pure \n",
194
+
" $ Right \n",
195
+
" ((proof >>=) . flip id . Left)\n",
196
+
" where\n",
197
+
" proof :: m (Either a a -> m Void)\n",
198
+
" proof = curry p ((proof >>=)\n",
199
+
" . flip id\n",
200
+
" . Left) \n",
201
+
" ((proof >>=)\n",
202
+
" . flip id\n",
203
+
" . Right)\n",
208
204
" \n",
209
205
" from :: Lem m -> Prop4 m\n",
210
206
" from _ = Prop4 $ uncurry $ (pure .) . either"