maybe.bend
bend-mathlib@0.5.0.0 · 130 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# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
74
75# Left identity: binding a pure value applies the function, reversed to rewrite toward the simple side.
76law maybe_pure_bind_sym:
77 for ~A: Data
78 for ~B: Data
79 for -f: A -> Maybe<&2, B>
80 for -x: A
81 {f(x) == Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) : Maybe<&2, B>}
82
83def maybe_pure_bind_sym(A, B, f, x):
84 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))
85
86# Right identity: binding pure is the identity, reversed to rewrite toward the simple side.
87law maybe_bind_pure_sym:
88 for ~A: Data
89 for m: Maybe<&2, A>
90 {m == Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) : Maybe<&2, A>}
91
92def maybe_bind_pure_sym(A, m):
93 Equal.sym(Maybe<&2, A>, Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)), m, maybe_bind_pure(~A, m))
94
95# Bind is associative, reversed to rewrite toward the simple side.
96law maybe_bind_assoc_sym:
97 for ~A: Data
98 for ~B: Data
99 for ~C: Data
100 for -f: A -> Maybe<&2, B>
101 for -g: B -> Maybe<&2, C>
102 for m: Maybe<&2, A>
103 {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>}
104
105def maybe_bind_assoc_sym(A, B, C, f, g, m):
106 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))
107
108# Mapping a pure value is pure of the mapped value, reversed to rewrite toward the simple side.
109law maybe_map_pure_sym:
110 for ~A: Data
111 for ~B: Data
112 for -f: A -> B
113 for -x: A
114 {Maybe.pure(&2, B, f(x)) == Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) : Maybe<&2, B>}
115
116def maybe_map_pure_sym(A, B, f, x):
117 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))
118
119# Mapping a composition maps the composition, reversed to rewrite toward the simple side.
120law maybe_map_compose_sym:
121 for ~A: Data
122 for ~B: Data
123 for ~C: Data
124 for -f: A -> B
125 for -g: B -> C
126 for m: Maybe<&2, A>
127 {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>}
128
129def maybe_map_compose_sym(A, B, C, f, g, m):
130 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))