maybe.bend
bend-mathlib@0.7.2.0 · 390 lines · 0 definitions
1# bend-mathlib/maybe.bend: Maybe monad and map laws over &2.
2import Base
3
4# Left identity: binding a pure value applies the function.
5law maybe_pure_bind:
6 for ~A: Data
7 for ~B: Data
8 for -f: A -> Maybe<&2, B>
9 for -x: A
10 {Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) == f(x) : Maybe<&2, B>}
11
12def maybe_pure_bind(A, B, f, x):
13 {==}
14
15# Right identity: binding pure is the identity.
16law maybe_bind_pure:
17 for ~A: Data
18 for m: Maybe<&2, A>
19 {Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) == m : Maybe<&2, A>}
20
21def maybe_bind_pure(A, m):
22 match m:
23 case None{}:
24 {==}
25 case Some{x}:
26 {==}
27
28# Bind is associative.
29law maybe_bind_assoc:
30 for ~A: Data
31 for ~B: Data
32 for ~C: Data
33 for -f: A -> Maybe<&2, B>
34 for -g: B -> Maybe<&2, C>
35 for m: Maybe<&2, A>
36 {Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) == Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) : Maybe<&2, C>}
37
38def maybe_bind_assoc(A, B, C, f, g, m):
39 match m:
40 case None{}:
41 {==}
42 case Some{x}:
43 {==}
44
45# Mapping a pure value is pure of the mapped value.
46law maybe_map_pure:
47 for ~A: Data
48 for ~B: Data
49 for -f: A -> B
50 for -x: A
51 {Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) == Maybe.pure(&2, B, f(x)) : Maybe<&2, B>}
52
53def maybe_map_pure(A, B, f, x):
54 {==}
55
56# Mapping a composition maps the composition.
57law maybe_map_compose:
58 for ~A: Data
59 for ~B: Data
60 for ~C: Data
61 for -f: A -> B
62 for -g: B -> C
63 for m: Maybe<&2, A>
64 {Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) == Maybe.map(&2, A, C, x => g(f(x)), m) : Maybe<&2, C>}
65
66def maybe_map_compose(A, B, C, f, g, m):
67 match m:
68 case None{}:
69 {==}
70 case Some{x}:
71 {==}
72
73# Mapping the identity gives the value back.
74law maybe_map_id:
75 for ~A: Data
76 for m: Maybe<&2, A>
77 {Maybe.map(&2, A, A, x => x, m) == m : Maybe<&2, A>}
78
79def maybe_map_id(A, m):
80 match m:
81 case None{}:
82 {==}
83 case Some{x}:
84 {==}
85
86# Binding a function that always fails gives None.
87law maybe_bind_none:
88 for ~A: Data
89 for ~B: Data
90 for m: Maybe<&2, A>
91 {Maybe.bind(&2, A, B, m, x => None{}) == None{} : Maybe<&2, B>}
92
93def maybe_bind_none(A, B, m):
94 match m:
95 case None{}:
96 {==}
97 case Some{x}:
98 {==}
99
100# Mapping is binding the function followed by pure.
101law maybe_map_eq_bind:
102 for ~A: Data
103 for ~B: Data
104 for ~f: A -> B
105 for m: Maybe<&2, A>
106 {Maybe.map(&2, A, B, f, m) == Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) : Maybe<&2, B>}
107
108def maybe_map_eq_bind(A, B, f, m):
109 match m:
110 case None{}:
111 {==}
112 case Some{x}:
113 {==}
114
115# Mapping keeps whether a value is present.
116law maybe_is_some_map:
117 for ~A: Data
118 for ~B: Data
119 for ~f: A -> B
120 for m: Maybe<&2, A>
121 {Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)) == Maybe.is_some(&2, A, m) : Bool}
122
123def maybe_is_some_map(A, B, f, m):
124 match m:
125 case None{}:
126 {==}
127 case Some{x}:
128 {==}
129
130# Mapping keeps whether a value is absent.
131law maybe_is_none_map:
132 for ~A: Data
133 for ~B: Data
134 for ~f: A -> B
135 for m: Maybe<&2, A>
136 {Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)) == Maybe.is_none(&2, A, m) : Bool}
137
138def maybe_is_none_map(A, B, f, m):
139 match m:
140 case None{}:
141 {==}
142 case Some{x}:
143 {==}
144
145# The default of a map, with the mapped default, is the mapped default of the original.
146law maybe_default_map:
147 for ~A: Data
148 for ~B: Data
149 for ~f: A -> B
150 for m: Maybe<&2, A>
151 for -d: A
152 {Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)) == f(Maybe.default(&2, A, m, d)) : B}
153
154def maybe_default_map(A, B, f, m, d):
155 match m:
156 case None{}:
157 {==}
158 case Some{x}:
159 {==}
160
161# None is a right identity for or.
162law maybe_or_none:
163 for ~A: Data
164 for m: Maybe<&2, A>
165 {Maybe.or(&2, A, m, None{}) == m : Maybe<&2, A>}
166
167def maybe_or_none(A, m):
168 match m:
169 case None{}:
170 {==}
171 case Some{x}:
172 {==}
173
174# Or is associative.
175law maybe_or_assoc:
176 for ~A: Data
177 for m: Maybe<&2, A>
178 for -n: Maybe<&2, A>
179 for -k: Maybe<&2, A>
180 {Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) == Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) : Maybe<&2, A>}
181
182def maybe_or_assoc(A, m, n, k):
183 match m:
184 case None{}:
185 {==}
186 case Some{x}:
187 {==}
188
189# Binding after a map binds the composition.
190law maybe_bind_map:
191 for ~A: Data
192 for ~B: Data
193 for ~C: Data
194 for ~f: A -> B
195 for ~g: B -> Maybe<&2, C>
196 for m: Maybe<&2, A>
197 {Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) == Maybe.bind(&2, A, C, m, x => g(f(x))) : Maybe<&2, C>}
198
199def maybe_bind_map(A, B, C, f, g, m):
200 match m:
201 case None{}:
202 {==}
203 case Some{x}:
204 {==}
205
206# Mapping after a bind maps inside the bound function.
207law maybe_map_bind:
208 for ~A: Data
209 for ~B: Data
210 for ~C: Data
211 for ~f: A -> Maybe<&2, B>
212 for ~g: B -> C
213 for m: Maybe<&2, A>
214 {Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) == Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) : Maybe<&2, C>}
215
216def maybe_map_bind(A, B, C, f, g, m):
217 match m:
218 case None{}:
219 {==}
220 case Some{x}:
221 {==}
222
223# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
224
225# Left identity: binding a pure value applies the function, reversed to rewrite toward the simple side.
226law maybe_pure_bind_sym:
227 for ~A: Data
228 for ~B: Data
229 for -f: A -> Maybe<&2, B>
230 for -x: A
231 {f(x) == Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) : Maybe<&2, B>}
232
233def maybe_pure_bind_sym(A, B, f, x):
234 Equal.sym(Maybe<&2, B>, Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f), f(x), maybe_pure_bind(~A, ~B, f, x))
235
236# Right identity: binding pure is the identity, reversed to rewrite toward the simple side.
237law maybe_bind_pure_sym:
238 for ~A: Data
239 for m: Maybe<&2, A>
240 {m == Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) : Maybe<&2, A>}
241
242def maybe_bind_pure_sym(A, m):
243 Equal.sym(Maybe<&2, A>, Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)), m, maybe_bind_pure(~A, m))
244
245# Bind is associative, reversed to rewrite toward the simple side.
246law maybe_bind_assoc_sym:
247 for ~A: Data
248 for ~B: Data
249 for ~C: Data
250 for -f: A -> Maybe<&2, B>
251 for -g: B -> Maybe<&2, C>
252 for m: Maybe<&2, A>
253 {Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) == Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) : Maybe<&2, C>}
254
255def maybe_bind_assoc_sym(A, B, C, f, g, m):
256 Equal.sym(Maybe<&2, C>, Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g), Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)), maybe_bind_assoc(~A, ~B, ~C, f, g, m))
257
258# Mapping a pure value is pure of the mapped value, reversed to rewrite toward the simple side.
259law maybe_map_pure_sym:
260 for ~A: Data
261 for ~B: Data
262 for -f: A -> B
263 for -x: A
264 {Maybe.pure(&2, B, f(x)) == Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) : Maybe<&2, B>}
265
266def maybe_map_pure_sym(A, B, f, x):
267 Equal.sym(Maybe<&2, B>, Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)), Maybe.pure(&2, B, f(x)), maybe_map_pure(~A, ~B, f, x))
268
269# Mapping a composition maps the composition, reversed to rewrite toward the simple side.
270law maybe_map_compose_sym:
271 for ~A: Data
272 for ~B: Data
273 for ~C: Data
274 for -f: A -> B
275 for -g: B -> C
276 for m: Maybe<&2, A>
277 {Maybe.map(&2, A, C, x => g(f(x)), m) == Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) : Maybe<&2, C>}
278
279def maybe_map_compose_sym(A, B, C, f, g, m):
280 Equal.sym(Maybe<&2, C>, Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)), Maybe.map(&2, A, C, x => g(f(x)), m), maybe_map_compose(~A, ~B, ~C, f, g, m))
281
282# Mapping the identity gives the value back, reversed to rewrite toward the simple side.
283law maybe_map_id_sym:
284 for ~A: Data
285 for m: Maybe<&2, A>
286 {m == Maybe.map(&2, A, A, x => x, m) : Maybe<&2, A>}
287
288def maybe_map_id_sym(A, m):
289 Equal.sym(Maybe<&2, A>, Maybe.map(&2, A, A, x => x, m), m, maybe_map_id(~A, m))
290
291# Binding a function that always fails gives None, reversed to rewrite toward the simple side.
292law maybe_bind_none_sym:
293 for ~A: Data
294 for ~B: Data
295 for m: Maybe<&2, A>
296 {None{} == Maybe.bind(&2, A, B, m, x => None{}) : Maybe<&2, B>}
297
298def maybe_bind_none_sym(A, B, m):
299 Equal.sym(Maybe<&2, B>, Maybe.bind(&2, A, B, m, x => None{}), None{}, maybe_bind_none(~A, ~B, m))
300
301# Mapping is binding the function followed by pure, reversed to rewrite toward the simple side.
302law maybe_map_eq_bind_sym:
303 for ~A: Data
304 for ~B: Data
305 for ~f: A -> B
306 for m: Maybe<&2, A>
307 {Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) == Maybe.map(&2, A, B, f, m) : Maybe<&2, B>}
308
309def maybe_map_eq_bind_sym(A, B, f, m):
310 Equal.sym(Maybe<&2, B>, Maybe.map(&2, A, B, f, m), Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))), maybe_map_eq_bind(~A, ~B, ~f, m))
311
312# Mapping keeps whether a value is present, reversed to rewrite toward the simple side.
313law maybe_is_some_map_sym:
314 for ~A: Data
315 for ~B: Data
316 for ~f: A -> B
317 for m: Maybe<&2, A>
318 {Maybe.is_some(&2, A, m) == Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)) : Bool}
319
320def maybe_is_some_map_sym(A, B, f, m):
321 Equal.sym(Bool, Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)), Maybe.is_some(&2, A, m), maybe_is_some_map(~A, ~B, ~f, m))
322
323# Mapping keeps whether a value is absent, reversed to rewrite toward the simple side.
324law maybe_is_none_map_sym:
325 for ~A: Data
326 for ~B: Data
327 for ~f: A -> B
328 for m: Maybe<&2, A>
329 {Maybe.is_none(&2, A, m) == Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)) : Bool}
330
331def maybe_is_none_map_sym(A, B, f, m):
332 Equal.sym(Bool, Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)), Maybe.is_none(&2, A, m), maybe_is_none_map(~A, ~B, ~f, m))
333
334# The default of a map, with the mapped default, is the mapped default of the original, reversed to rewrite toward the simple side.
335law maybe_default_map_sym:
336 for ~A: Data
337 for ~B: Data
338 for ~f: A -> B
339 for m: Maybe<&2, A>
340 for -d: A
341 {f(Maybe.default(&2, A, m, d)) == Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)) : B}
342
343def maybe_default_map_sym(A, B, f, m, d):
344 Equal.sym(B, Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)), f(Maybe.default(&2, A, m, d)), maybe_default_map(~A, ~B, ~f, m, d))
345
346# None is a right identity for or, reversed to rewrite toward the simple side.
347law maybe_or_none_sym:
348 for ~A: Data
349 for m: Maybe<&2, A>
350 {m == Maybe.or(&2, A, m, None{}) : Maybe<&2, A>}
351
352def maybe_or_none_sym(A, m):
353 Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, m, None{}), m, maybe_or_none(~A, m))
354
355# Or is associative, reversed to rewrite toward the simple side.
356law maybe_or_assoc_sym:
357 for ~A: Data
358 for m: Maybe<&2, A>
359 for -n: Maybe<&2, A>
360 for -k: Maybe<&2, A>
361 {Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) == Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) : Maybe<&2, A>}
362
363def maybe_or_assoc_sym(A, m, n, k):
364 Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, Maybe.or(&2, A, m, n), k), Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)), maybe_or_assoc(~A, m, n, k))
365
366# Binding after a map binds the composition, reversed to rewrite toward the simple side.
367law maybe_bind_map_sym:
368 for ~A: Data
369 for ~B: Data
370 for ~C: Data
371 for ~f: A -> B
372 for ~g: B -> Maybe<&2, C>
373 for m: Maybe<&2, A>
374 {Maybe.bind(&2, A, C, m, x => g(f(x))) == Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) : Maybe<&2, C>}
375
376def maybe_bind_map_sym(A, B, C, f, g, m):
377 Equal.sym(Maybe<&2, C>, Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g), Maybe.bind(&2, A, C, m, x => g(f(x))), maybe_bind_map(~A, ~B, ~C, ~f, ~g, m))
378
379# Mapping after a bind maps inside the bound function, reversed to rewrite toward the simple side.
380law maybe_map_bind_sym:
381 for ~A: Data
382 for ~B: Data
383 for ~C: Data
384 for ~f: A -> Maybe<&2, B>
385 for ~g: B -> C
386 for m: Maybe<&2, A>
387 {Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) == Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) : Maybe<&2, C>}
388
389def maybe_map_bind_sym(A, B, C, f, g, m):
390 Equal.sym(Maybe<&2, C>, Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)), Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))), maybe_map_bind(~A, ~B, ~C, ~f, ~g, m))