Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (8 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/monad.ma

    r1640 r1647  
    77  monad : Type[0] → Type[0] ;
    88  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
    1610}.
    1711
    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
     12notation "m »= f" with precedence 49
    3413  for @{'m_bind $m $f) }.
    3514
     
    3716  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    3817notation > "! 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'})}.
    4019notation > "! ident v : ty ← e; e'"
    4120  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    42 notation < "vbox(! \nbsp ident v ← e ; break e')"
     21notation < "vbox(! \nbsp ident v ← e ; break e')"
    4322  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
    4423notation > "! ident v ← e : ty ; e'"
    4524  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
    46 notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
     25notation < "vbox(! \nbsp ident v : ty \nbsp ←  \nbsp e ; break e')"
    4726  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    4827notation > "! ident v : ty ← e : ty' ; e'"
     
    5029notation > "! 〈ident v1, ident v2〉 ← e ; e'"
    5130  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'})}.
    5233notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
    5334  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5435notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
    5536  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')"
     37notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉  \nbsp ←  \nbsp e ; break e')"
    5738  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5839notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
    5940  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'})}.
    6043notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    6144  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')"
     45notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')"
    6346  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')"
     47notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')"
    6548  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    6649
    67  
    68 (* "do" alternative notation for backward compatibility *)
     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'})}.
    6972notation > "'do' ident v ← e; e'"
    7073  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
    7174notation > "'do' ident v : ty ← e; e'"
    7275  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'})}.
    7380notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
    7481  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     
    7986notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    8087  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    81  
     88
    8289(* dependent pair versions *)
    83 notation > "! «ident v1, ident v2» ← e ; e'"
     90notation > "'do' «ident v1, ident v2» ← e ; e'"
    8491  with precedence 48 for
    8592  @{'m_bind ${e} (λ${fresh p_sig}.
    8693    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
    8794
    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 
    9995notation > "'do' «ident v1, ident v2, ident H» ← e ; e'"
    10096  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
     99notation > "'return' t" with precedence 49 for @{'m_return $t}.
     100notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}.
     101
    111102interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
    112 interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).
    113103interpretation "monad return" 'm_return x = (m_return ? ? x).
    114104
     105
    115106include "basics/lists/list.ma".
     107
    116108
    117109(* add structure and properties as needed *)
     
    124116  m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
    125117  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;
    126120  m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
    127121  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)
     
    130124interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
    131125interpretation "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
     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)
    146158  (* map *)
    147159  (λX,Y,f,m.
     
    164176  (* join *)
    165177  (λ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    ])
    166188  (λ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
     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 TracChangeset for help on using the changeset viewer.