1	# bend-mathlib/maybe.bend: Maybe monad and map laws over &2.
2	import Base
3	
4	# Left identity: binding a pure value applies the function.
5	law 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	
12	def maybe_pure_bind(A, B, f, x):
13	  {==}
14	
15	# Right identity: binding pure is the identity.
16	law 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	
21	def maybe_bind_pure(A, m):
22	  match m:
23	    case None{}:
24	      {==}
25	    case Some{x}:
26	      {==}
27	
28	# Bind is associative.
29	law 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	
38	def 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.
46	law 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	
53	def maybe_map_pure(A, B, f, x):
54	  {==}
55	
56	# Mapping a composition maps the composition.
57	law 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	
66	def 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.
76	law 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	
83	def 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.
87	law 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	
92	def 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.
96	law 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	
105	def 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.
109	law 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	
116	def 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.
120	law 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	
129	def 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))