maybe.bend

bend-mathlib@0.8.1.0 · 390 lines · 30 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))