Changeset 1647 for src/utilities/monad.ma
 Timestamp:
 Jan 17, 2012, 1:13:08 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r1640 r1647 7 7 monad : Type[0] → Type[0] ; 8 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) 9 m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y 16 10 }. 17 11 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 12 notation "m »= f" with precedence 49 34 13 for @{'m_bind $m $f) }. 35 14 … … 37 16 with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. 38 17 notation > "! ident v ← e; e'" 39 with precedence 48 for @{'m_bind ' (λ${ident v}. ${e'}) ${e}}.18 with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. 40 19 notation > "! ident v : ty ← e; e'" 41 20 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 42 notation < "vbox(! \nbsp 21 notation < "vbox(! \nbsp ident v ← e ; break e')" 43 22 with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}. 44 23 notation > "! ident v ← e : ty ; e'" 45 24 with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. 46 notation < "vbox(! \nbsp ident v : ty ←e ; break e')"25 notation < "vbox(! \nbsp ident v : ty \nbsp ← \nbsp e ; break e')" 47 26 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 48 27 notation > "! ident v : ty ← e : ty' ; e'" … … 50 29 notation > "! 〈ident v1, ident v2〉 ← e ; e'" 51 30 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. 31 notation > "! 〈ident v1, ident v2〉 ← e : ty ; e'" 32 with precedence 48 for @{'m_bind2 (${e} : $ty) (λ${ident v1}. λ${ident v2}. ${e'})}. 52 33 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" 53 34 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. 54 35 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')" 55 36 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')"37 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 \nbsp ← \nbsp e ; break e')" 57 38 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. 58 39 notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'" 59 40 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. 41 notation > "! 〈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'})}. 60 43 notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'" 61 44 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')"45 notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')" 63 46 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')"47 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')" 65 48 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. 66 49 67 68 (* "do" alternative notation for backward compatibility *) 50 (* dependent pair versions *) 51 notation > "! «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'}])}. 55 notation < "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 60 notation > "! «ident v1, ident v2, ident H» ← e ; e'" 61 with precedence 48 for 62 @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}. 63 notation < "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 *) 70 notation > "'do'_ e; e'" 71 with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. 69 72 notation > "'do' ident v ← e; e'" 70 73 with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. 71 74 notation > "'do' ident v : ty ← e; e'" 72 75 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 76 notation > "'do' ident v ← e : ty ; e'" 77 with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. 78 notation > "'do' ident v : ty ← e : ty' ; e'" 79 with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}. 73 80 notation > "'do' 〈ident v1, ident v2〉 ← e ; e'" 74 81 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. … … 79 86 notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'" 80 87 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. 81 88 82 89 (* dependent pair versions *) 83 notation > " !«ident v1, ident v2» ← e ; e'"90 notation > "'do' «ident v1, ident v2» ← e ; e'" 84 91 with precedence 48 for 85 92 @{'m_bind ${e} (λ${fresh p_sig}. 86 93 match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}. 87 94 88 notation > "! «ident v1, ident v2, ident H» ← e ; e'"89 with precedence 48 for90 @{'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 for96 @{'m_bind ${e} (λ${fresh p_sig}.97 match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.98 99 95 notation > "'do' «ident v1, ident v2, ident H» ← e ; e'" 100 96 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). 97 @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}. 98 99 notation > "'return' t" with precedence 49 for @{'m_return $t}. 100 notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}. 101 111 102 interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f). 112 interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).113 103 interpretation "monad return" 'm_return x = (m_return ? ? x). 114 104 105 115 106 include "basics/lists/list.ma". 107 116 108 117 109 (* add structure and properties as needed *) … … 124 116 m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W; 125 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; 126 120 m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y); 127 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) … … 130 124 interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f). 131 125 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 126 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f). 127 128 check (λ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 130 record 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 138 record 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 153 interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y). 154 155 156 definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind. 157 mk_Monad (mk_MonadDefinition monad m_return m_bind) 146 158 (* map *) 147 159 (λX,Y,f,m. … … 164 176 (* join *) 165 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 ]) 166 188 (λ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 }. 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 196 definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3. 197 mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3. 198 199 definition 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 TracChangeset
for help on using the changeset viewer.