source: src/utilities/monad.ma @ 1647

Last change on this file since 1647 was 1647, checked in by tranquil, 7 years ago
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File size: 9.3 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}.
11
12notation "m »= f" with precedence 49
13  for @{'m_bind $m $f) }.
14
15notation > "!_ e; e'"
16  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
17notation > "! ident v ← e; e'"
18  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
19notation > "! ident v : ty ← e; e'"
20  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
21notation < "vbox(! \nbsp ident v ← e ; break e')"
22  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
23notation > "! ident v ← e : ty ; e'"
24  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
25notation < "vbox(! \nbsp ident v : ty \nbsp ←  \nbsp e ; break e')"
26  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
27notation > "! ident v : ty ← e : ty' ; e'"
28  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
29notation > "! 〈ident v1, ident v2〉 ← e ; e'"
30  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
31notation > "! 〈ident v1, ident v2〉 ← e : ty ; e'"
32  with precedence 48 for @{'m_bind2 (${e} : $ty) (λ${ident v1}. λ${ident v2}. ${e'})}.
33notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
34  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
35notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
36  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
37notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉  \nbsp ←  \nbsp e ; break e')"
38  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
39notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
40  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
41notation > "! 〈ident v1, ident v2, ident v3〉 ← e : ty ; e'"
42  with precedence 48 for @{'m_bind3 (${e} : ${ty}) (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
43notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
44  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
45notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')"
46  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
47notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')"
48  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
49
50(* dependent pair versions *)
51notation > "! «ident v1, ident v2» ← e ; e'"
52  with precedence 48 for
53  @{'m_bind ${e} (λ${fresh p_sig}.
54    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
55notation < "vbox(! \nbsp «ident v1, ident v2» \nbsp ← \nbsp e ; break e')"
56  with precedence 48 for
57  @{'m_bind ${e} (λ${fresh p_sig}.
58    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
59   
60notation > "! «ident v1, ident v2, ident H» ← e ; e'"
61  with precedence 48 for
62  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
63notation < "vbox(! \nbsp «ident v1, ident v2, ident H» \nbsp ← \nbsp e ; e')"
64  with precedence 48 for
65  @{'m_sigbind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.
66    λ${ident H} : ${ty3}. ${e'})}.
67   
68 
69(*alternative do notation for backward compatibility *)
70notation > "'do'_ e; e'"
71  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
72notation > "'do' ident v ← e; e'"
73  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
74notation > "'do' ident v : ty ← e; e'"
75  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
76notation > "'do' ident v ← e : ty ; e'"
77  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
78notation > "'do' ident v : ty ← e : ty' ; e'"
79  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
80notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
81  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
82notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
83  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
84notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'"
85  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
86notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
87  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
88
89(* dependent pair versions *)
90notation > "'do' «ident v1, ident v2» ← e ; e'"
91  with precedence 48 for
92  @{'m_bind ${e} (λ${fresh p_sig}.
93    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
94
95notation > "'do' «ident v1, ident v2, ident H» ← e ; e'"
96  with precedence 48 for
97  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
98
99notation > "'return' t" with precedence 49 for @{'m_return $t}.
100notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}.
101
102interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
103interpretation "monad return" 'm_return x = (m_return ? ? x).
104
105
106include "basics/lists/list.ma".
107
108
109(* add structure and properties as needed *)
110record Monad : Type[1] ≝ {
111  m_def :> MonadDefinition ;
112  m_map : ∀X, Y. (X → Y) → monad m_def X → monad m_def Y ;
113  m_map2 : ∀X, Y, Z. (X → Y → Z) →
114    monad m_def X → monad m_def Y → monad m_def Z;
115  m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z;
116  m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
117  m_join : ∀X.monad m_def (monad m_def X) → monad m_def X;
118  m_sigbind2 : ∀A,B,C.∀P:A×B → Prop. monad m_def (Σx:A×B.P x) →
119      (∀a,b. P 〈a,b〉 → monad m_def C) → monad m_def C;
120  m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
121  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)
122}.
123
124interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
125interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
126interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
127
128check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)
129
130record MonadProps : Type[1] ≝
131  { max_def :> Monad
132  ; m_return_bind : ∀X,Y.∀x : X.∀f : X → monad max_def Y. ! y ← return x ; f y = f x
133  ; m_bind_return : ∀X.∀m : monad max_def X.! x ← m ; return x = m
134  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
135      ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
136  }.
137
138record SetoidMonadProps : Type[1] ≝
139  { smax_def :> Monad
140  ; sm_eq : ∀X.relation (monad smax_def X)
141  ; sm_eq_refl : ∀X.reflexive ? (sm_eq X)
142  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
143  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
144  ; sm_return_proper : ∀X .m_return smax_def X ⊨ eq ? ++> sm_eq ?
145  ; sm_bind_proper : ∀X, Y.m_bind smax_def X Y ⊨ sm_eq ? ++> (eq ? ++> sm_eq ?) ++> sm_eq ?
146  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
147      sm_eq Y (! y ← return x ; f y) (f x)
148  ; sm_bind_return : ∀X.∀m : monad smax_def X.sm_eq X (! x ← m ; return x) m
149  ; sm_bind_bind : ∀X,Y,Z. ∀m : monad smax_def X.∀f : X → monad smax_def Y.
150      ∀g : Y → monad smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)
151  }.
152
153interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y).
154
155
156definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind.
157  mk_Monad (mk_MonadDefinition monad m_return m_bind)
158  (* map *)
159  (λX,Y,f,m.
160    ! x ← m ;
161    return f x)
162  (* map2 *)
163  (λX,Y,Z,f,m,n.
164    ! x ← m ;
165    ! y ← n ;
166    return (f x y))
167  (* bind2 *)
168  (λX,Y,Z,m,f.
169    ! p ← m ;
170    let 〈x, y〉 ≝ p in
171    f x y)
172  (λX,Y,Z,W,m,f.
173    ! p ← m ;
174    let 〈x, y, z〉 ≝ p in
175    f x y z)
176  (* join *)
177  (λX,m.! x ← m ; x)
178  (* m_sigbind2 *)
179  (λA,B,C,P,e,f.
180    ! e_sig ← e ;
181    match e_sig with
182    [ mk_Sig p p_prf ⇒
183      match p return λx.x = p → ? with
184      [ mk_Prod a b ⇒
185      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
186      ](refl …)
187    ])
188  (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l)
189  (λX,Y,P,f,l.foldr … (λel,macc.
190    ! «r, r_prf» ← f el ;
191    ! «acc, acc_prf» ← macc ;
192    return (mk_Sig ?? (r :: acc) ?))
193    (return (mk_Sig … [ ] ?)) l).
194  % assumption qed.
195
196definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3.
197mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3.
198
199definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝
200  λmonad,m_return,m_bind,sm_eq,p1,p2,p3,p4,p5,p6,p7,p8.
201  mk_SetoidMonadProps (MakeMonad monad m_return m_bind) sm_eq p1 p2 p3 p4 p5 p6 p7 p8.
Note: See TracBrowser for help on using the repository browser.