Changeset 1640 for src/utilities/monad.ma
 Timestamp:
 Jan 11, 2012, 5:41:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r1635 r1640 3 3 include "utilities/setoids.ma". 4 4 include "utilities/proper.ma". 5 5 6 6 record MonadDefinition : Type[1] ≝ { 7 7 monad : Type[0] → Type[0] ; … … 37 37 with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. 38 38 notation > "! ident v ← e; e'" 39 with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.39 with precedence 48 for @{'m_bind' (λ${ident v}. ${e'}) ${e}}. 40 40 notation > "! ident v : ty ← e; e'" 41 41 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 42 42 notation < "vbox(! \nbsp ident v ← e ; break e')" 43 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'})}. 44 46 notation < "vbox(! \nbsp ident v : ty ← e ; break e')" 45 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'})}. 46 50 notation > "! 〈ident v1, ident v2〉 ← e ; e'" 47 51 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. … … 52 56 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; break e')" 53 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'})}. 54 81 55 notation > "'return' t" with precedence 30 for @{'m_return $t}. 56 notation < "'return' \nbsp t" with precedence 30 for @{'m_return $t}. 57 58 (* 59 notation > "!!_ e; e'" 60 with precedence 40 for @{'sm_bind ${e} (λ_.${e'})}. 61 notation > "!! ident v ← e; e'" 62 with precedence 40 for @{'sm_bind ${e} (λ${ident v}.${e'})}. 63 notation > "!! ident v : ty ← e; e'" 64 with precedence 40 for @{'sm_bind ${e} (λ${ident v} : ${ty}.${e'})}. 65 notation < "vbox(!! ident v ← e; break e')" 66 with precedence 40 for @{'sm_bind ${e} (λ${ident v}.${e'})}. 67 notation < "vbox(!! ident v : ty ← e; break e')" 68 with precedence 40 for @{'sm_bind ${e} (λ${ident v} : ${ty}.${e'})}. 69 notation > "!! 〈ident v1, ident v2〉 ← e; e'" 70 with precedence 40 for @{'sm_bind ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 71 notation > "!! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" 72 with precedence 40 for @{'sm_bind ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 73 notation < "vbox(!! \nbsp 〈ident v1, ident v2〉 ← e; break e')" 74 with precedence 40 for @{'sm_bind ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 75 notation < "vbox(!! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" 76 with precedence 40 for @{'sm_bind ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 77 78 notation "m !»= f" with precedence 40 79 for @{'sm_bind $m $f) }. 80 81 notation "'sreturn' t" with precedence 30 for @{'sm_return $t}. 82 83 interpretation "setoid monad bind" 'sm_bind m f = (sm_bind ? ? ? m f). 84 interpretation "setoid monad return" 'sm_return x = (sm_return ? ? x). 85 *) 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}. 86 107 87 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). 88 110 interpretation "setoid monad return" 'm_return x = (sm_return ? ? x). 89 111 interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f). 112 interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f). 90 113 interpretation "monad return" 'm_return x = (m_return ? ? x). 114 115 include "basics/lists/list.ma". 91 116 92 117 (* add structure and properties as needed *) … … 97 122 monad m_def X → monad m_def Y → monad m_def Z; 98 123 m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z; 99 m_join : ∀X.monad m_def (monad m_def X) → monad m_def X 100 }. 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. 101 143 102 144 definition MakeMonad : MonadDefinition → Monad ≝ λM. … … 116 158 let 〈x, y〉 ≝ p in 117 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) 118 164 (* join *) 119 (λX,m.! x ← m ; x). 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 120 171 (* add structure and properties as needed *) 121 172 record SetoidMonad : Type[1] ≝ { … … 145 196 f x y). 146 197 147 interpretation "monad bind2" 'm_bind2 m f = (sm_map2 ? ? ? ? m f). 148 198 interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f). 149 199 150 200 record MonadTransformer : Type[1] ≝ { … … 155 205 m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x) 156 206 }. 157 158 159
Note: See TracChangeset
for help on using the changeset viewer.