1 | include "basics/types.ma". |
---|
2 | include "basics/relations.ma". |
---|
3 | include "utilities/setoids.ma". |
---|
4 | include "utilities/proper.ma". |
---|
5 | |
---|
6 | record MonadDefinition : Type[1] ≝ { |
---|
7 | monad : Type[0] → Type[0] ; |
---|
8 | m_return : ∀X. X → monad X ; |
---|
9 | m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y; |
---|
10 | m_return_bind : ∀X,Y.∀x : X.∀f : X → monad Y. |
---|
11 | m_bind ?? (m_return ? x) f = f x ; |
---|
12 | m_bind_return : ∀X.∀m : monad X. |
---|
13 | m_bind ?? m (m_return ?) = m ; |
---|
14 | m_bind_bind : ∀X,Y,Z. ∀m : monad X.∀f : X → monad Y.∀g : Y → monad Z. |
---|
15 | m_bind ?? (m_bind ?? m f) g = m_bind ?? m (λx. m_bind ?? (f x) g) |
---|
16 | }. |
---|
17 | |
---|
18 | record SetoidMonadDefinition : Type[1] ≝ { |
---|
19 | std_monad : Type[0] → Setoid ; |
---|
20 | sm_return : ∀X. X → std_monad X ; |
---|
21 | sm_bind : ∀X,Y. std_monad X → (X → std_monad Y) → std_monad Y; |
---|
22 | sm_return_proper : ∀X. sm_return X ⊨ eq ? ++> std_eq …; |
---|
23 | sm_bind_proper : ∀X,Y. |
---|
24 | sm_bind X Y ⊨ std_eq … ++> (eq ? ++> std_eq …) ++> std_eq …; |
---|
25 | sm_return_bind : ∀X,Y : Setoid.∀x : X.∀f : X → std_monad Y. |
---|
26 | sm_bind ?? (sm_return ? x) f ≅ f x ; |
---|
27 | sm_bind_return : ∀X.∀m : std_monad X. |
---|
28 | sm_bind ?? m (sm_return ?) ≅ m ; |
---|
29 | sm_bind_bind : ∀X,Y,Z. ∀m : std_monad X.∀f : X → std_monad Y.∀g : Y → std_monad Z. |
---|
30 | sm_bind ?? (sm_bind ?? m f) g ≅ sm_bind ?? m (λx. sm_bind ?? (f x) g) |
---|
31 | }. |
---|
32 | |
---|
33 | notation "m »= f" with precedence 47 |
---|
34 | for @{'m_bind $m $f) }. |
---|
35 | |
---|
36 | notation > "!_ e; e'" |
---|
37 | with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. |
---|
38 | notation > "! ident v ← e; e'" |
---|
39 | with precedence 48 for @{'m_bind' (λ${ident v}. ${e'}) ${e}}. |
---|
40 | notation > "! ident v : ty ← e; e'" |
---|
41 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
42 | notation < "vbox(! \nbsp ident v ← e ; break e')" |
---|
43 | with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}. |
---|
44 | notation > "! ident v ← e : ty ; e'" |
---|
45 | with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. |
---|
46 | notation < "vbox(! \nbsp ident v : ty ← e ; break e')" |
---|
47 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
48 | notation > "! ident v : ty ← e : ty' ; e'" |
---|
49 | with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}. |
---|
50 | notation > "! 〈ident v1, ident v2〉 ← e ; e'" |
---|
51 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
52 | notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" |
---|
53 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. |
---|
54 | notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')" |
---|
55 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
56 | notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; break e')" |
---|
57 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. |
---|
58 | notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'" |
---|
59 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. |
---|
60 | notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'" |
---|
61 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. |
---|
62 | notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 ← e ; break e')" |
---|
63 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. |
---|
64 | notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; break e')" |
---|
65 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. |
---|
66 | |
---|
67 | |
---|
68 | (* "do" alternative notation for backward compatibility *) |
---|
69 | notation > "'do' ident v ← e; e'" |
---|
70 | with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. |
---|
71 | notation > "'do' ident v : ty ← e; e'" |
---|
72 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
73 | notation > "'do' 〈ident v1, ident v2〉 ← e ; e'" |
---|
74 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
75 | notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" |
---|
76 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. |
---|
77 | notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'" |
---|
78 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. |
---|
79 | notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'" |
---|
80 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. |
---|
81 | |
---|
82 | (* dependent pair versions *) |
---|
83 | notation > "! «ident v1, ident v2» ← e ; e'" |
---|
84 | with precedence 48 for |
---|
85 | @{'m_bind ${e} (λ${fresh p_sig}. |
---|
86 | match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}. |
---|
87 | |
---|
88 | notation > "! «ident v1, ident v2, ident H» ← e ; e'" |
---|
89 | with precedence 48 for |
---|
90 | @{'m_bind ${e} (λ${fresh p_sig}. |
---|
91 | match ${fresh p_sig} with [mk_Sig ${fresh p} ${ident H} ⇒ |
---|
92 | match ${fresh p} with [mk_Prod ${ident v1} ${ident v2} ⇒ ${e'}]])}. |
---|
93 | |
---|
94 | notation > "'do' «ident v1, ident v2» ← e ; e'" |
---|
95 | with precedence 48 for |
---|
96 | @{'m_bind ${e} (λ${fresh p_sig}. |
---|
97 | match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}. |
---|
98 | |
---|
99 | notation > "'do' «ident v1, ident v2, ident H» ← e ; e'" |
---|
100 | with precedence 48 for |
---|
101 | @{'m_bind ${e} (λ${fresh p_sig}. |
---|
102 | match ${fresh p_sig} with [mk_Sig ${fresh p} ${ident H} ⇒ |
---|
103 | match ${fresh p} with [mk_Prod ${ident v1} ${ident v2} ⇒ ${e'}]])}. |
---|
104 | |
---|
105 | notation > "'return' t" with precedence 46 for @{'m_return $t}. |
---|
106 | notation < "'return' \nbsp t" with precedence 46 for @{'m_return $t}. |
---|
107 | |
---|
108 | interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f). |
---|
109 | interpretation "setoid monad bind'" 'm_bind' f m = (sm_bind ? ? ? m f). |
---|
110 | interpretation "setoid monad return" 'm_return x = (sm_return ? ? x). |
---|
111 | interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f). |
---|
112 | interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f). |
---|
113 | interpretation "monad return" 'm_return x = (m_return ? ? x). |
---|
114 | |
---|
115 | include "basics/lists/list.ma". |
---|
116 | |
---|
117 | (* add structure and properties as needed *) |
---|
118 | record Monad : Type[1] ≝ { |
---|
119 | m_def :> MonadDefinition ; |
---|
120 | m_map : ∀X, Y. (X → Y) → monad m_def X → monad m_def Y ; |
---|
121 | m_map2 : ∀X, Y, Z. (X → Y → Z) → |
---|
122 | monad m_def X → monad m_def Y → monad m_def Z; |
---|
123 | m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z; |
---|
124 | m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W; |
---|
125 | m_join : ∀X.monad m_def (monad m_def X) → monad m_def X; |
---|
126 | m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y); |
---|
127 | m_mmap_sigma : ∀X,Y,P.(X → monad m_def (Σy : Y.P y)) → list X → monad m_def (Σl : list Y.All ? P l) |
---|
128 | }. |
---|
129 | |
---|
130 | interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f). |
---|
131 | interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f). |
---|
132 | |
---|
133 | (* notation breaks completely here.... *) |
---|
134 | definition mmap_sigma_helper : ∀M.∀X,Y,P.?→?→?→monad M (Σl : list Y.All ? P l) ≝ |
---|
135 | λM.λX,Y:Type[0].λP.λf : X → monad M (Σy : Y.P y). |
---|
136 | λel.λmacc : monad M (Σl : list Y.All ? P l). |
---|
137 | m_bind M ?? (f el) (λp. |
---|
138 | match p with [mk_Sig r r_prf ⇒ |
---|
139 | m_bind M ?? macc (λq. |
---|
140 | match q with [mk_Sig acc acc_prf ⇒ |
---|
141 | return (mk_Sig … (r :: acc) ?)])]). |
---|
142 | whd %{r_prf acc_prf} qed. |
---|
143 | |
---|
144 | definition MakeMonad : MonadDefinition → Monad ≝ λM. |
---|
145 | mk_Monad M |
---|
146 | (* map *) |
---|
147 | (λX,Y,f,m. |
---|
148 | ! x ← m ; |
---|
149 | return f x) |
---|
150 | (* map2 *) |
---|
151 | (λX,Y,Z,f,m,n. |
---|
152 | ! x ← m ; |
---|
153 | ! y ← n ; |
---|
154 | return (f x y)) |
---|
155 | (* bind2 *) |
---|
156 | (λX,Y,Z,m,f. |
---|
157 | ! p ← m ; |
---|
158 | let 〈x, y〉 ≝ p in |
---|
159 | f x y) |
---|
160 | (λX,Y,Z,W,m,f. |
---|
161 | ! p ← m ; |
---|
162 | let 〈x, y, z〉 ≝ p in |
---|
163 | f x y z) |
---|
164 | (* join *) |
---|
165 | (λX,m.! x ← m ; x) |
---|
166 | (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l) |
---|
167 | (λX,Y,P,f,l.foldr … (mmap_sigma_helper M … f) (return (mk_Sig … [ ] ?)) l). |
---|
168 | % qed. |
---|
169 | |
---|
170 | |
---|
171 | (* add structure and properties as needed *) |
---|
172 | record SetoidMonad : Type[1] ≝ { |
---|
173 | sm_def :> SetoidMonadDefinition ; |
---|
174 | sm_map : ∀X, Y. (X → Y) → std_monad sm_def X → std_monad sm_def Y ; |
---|
175 | sm_map2 : ∀X, Y, Z. (X → Y → Z) → |
---|
176 | std_monad sm_def X → std_monad sm_def Y → std_monad sm_def Z; |
---|
177 | sm_bind2 : ∀X,Y,Z.std_monad sm_def (X×Y) → |
---|
178 | (X → Y → std_monad sm_def Z) → std_monad sm_def Z |
---|
179 | }. |
---|
180 | |
---|
181 | definition MakeSetoidMonad : SetoidMonadDefinition → SetoidMonad ≝ λM. |
---|
182 | mk_SetoidMonad M |
---|
183 | (* map *) |
---|
184 | (λX,Y,f,m. |
---|
185 | ! x ← m ; |
---|
186 | return f x) |
---|
187 | (* map2 *) |
---|
188 | (λX,Y,Z,f,m,n. |
---|
189 | ! x ← m ; |
---|
190 | ! y ← n ; |
---|
191 | return (f x y)) |
---|
192 | (* bind2 *) |
---|
193 | (λX,Y,Z,m,f. |
---|
194 | ! p ← m ; |
---|
195 | let 〈x, y〉 ≝ p in |
---|
196 | f x y). |
---|
197 | |
---|
198 | interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f). |
---|
199 | |
---|
200 | record MonadTransformer : Type[1] ≝ { |
---|
201 | monad_trans : MonadDefinition → MonadDefinition ; |
---|
202 | m_lift : ∀M,X. monad M X → monad (monad_trans M) X ; |
---|
203 | m_lift_return : ∀M,X.∀x : X. m_lift M X (return x) = return x ; |
---|
204 | m_lift_bind : ∀M,X,Y.∀m : monad M X.∀f : X → monad M Y. |
---|
205 | m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x) |
---|
206 | }. |
---|