source: src/utilities/monad.ma @ 1640

Last change on this file since 1640 was 1640, checked in by tranquil, 8 years ago
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File size: 8.9 KB
Line 
1include "basics/types.ma".
2include "basics/relations.ma".
3include "utilities/setoids.ma".
4include "utilities/proper.ma".
5 
6record 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
18record 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
33notation "m »= f" with precedence 47
34  for @{'m_bind $m $f) }.
35
36notation > "!_ e; e'"
37  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
38notation > "! ident v ← e; e'"
39  with precedence 48 for @{'m_bind' (λ${ident v}. ${e'}) ${e}}.
40notation > "! ident v : ty ← e; e'"
41  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
42notation < "vbox(! \nbsp ident v ← e ; break e')"
43  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
44notation > "! ident v ← e : ty ; e'"
45  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
46notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
47  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
48notation > "! ident v : ty ← e : ty' ; e'"
49  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
50notation > "! 〈ident v1, ident v2〉 ← e ; e'"
51  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
52notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
53  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
54notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
55  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
56notation < "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'})}.
58notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
59  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
60notation > "! 〈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'})}.
62notation < "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'})}.
64notation < "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 *)
69notation > "'do' ident v ← e; e'"
70  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
71notation > "'do' ident v : ty ← e; e'"
72  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
73notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
74  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
75notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
76  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
77notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'"
78  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
79notation > "'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 *)
83notation > "! «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
88notation > "! «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
94notation > "'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
99notation > "'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
105notation > "'return' t" with precedence 46 for @{'m_return $t}.
106notation < "'return' \nbsp t" with precedence 46 for @{'m_return $t}.
107
108interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f).
109interpretation "setoid monad bind'" 'm_bind' f m = (sm_bind ? ? ? m f).
110interpretation "setoid monad return" 'm_return x = (sm_return ? ? x).
111interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
112interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).
113interpretation "monad return" 'm_return x = (m_return ? ? x).
114
115include "basics/lists/list.ma".
116
117(* add structure and properties as needed *)
118record 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
130interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
131interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
132
133(* notation breaks completely here.... *)
134definition 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) ?)])]).
142whd %{r_prf acc_prf} qed.
143
144definition 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 *)
172record 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
181definition 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
198interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f).
199
200record 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}.
Note: See TracBrowser for help on using the repository browser.