Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (8 years ago)
Author:
tranquil
Message:
  • 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/monad.ma

    r1635 r1640  
    33include "utilities/setoids.ma".
    44include "utilities/proper.ma".
    5 
     5 
    66record MonadDefinition : Type[1] ≝ {
    77  monad : Type[0] → Type[0] ;
     
    3737  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    3838notation > "! 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}}.
    4040notation > "! ident v : ty ← e; e'"
    4141  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    4242notation < "vbox(! \nbsp ident v ← e ; break e')"
    4343  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'})}.
    4446notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
    4547  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'})}.
    4650notation > "! 〈ident v1, ident v2〉 ← e ; e'"
    4751  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     
    5256notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; break e')"
    5357  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'})}.
    5481 
    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 *)
     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}.
    86107
    87108interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f).
     109interpretation "setoid monad bind'" 'm_bind' f m = (sm_bind ? ? ? m f).
    88110interpretation "setoid monad return" 'm_return x = (sm_return ? ? x).
    89111interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
     112interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).
    90113interpretation "monad return" 'm_return x = (m_return ? ? x).
     114
     115include "basics/lists/list.ma".
    91116
    92117(* add structure and properties as needed *)
     
    97122    monad m_def X → monad m_def Y → monad m_def Z;
    98123  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
     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.
    101143
    102144definition MakeMonad : MonadDefinition → Monad ≝ λM.
     
    116158    let 〈x, y〉 ≝ p in
    117159    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)
    118164  (* 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
    120171(* add structure and properties as needed *)
    121172record SetoidMonad : Type[1] ≝ {
     
    145196    f x y).
    146197
    147 interpretation "monad bind2" 'm_bind2 m f = (sm_map2 ? ? ? ? m f).
    148 
     198interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f).
    149199
    150200record MonadTransformer : Type[1] ≝ {
     
    155205    m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x)
    156206}.
    157 
    158 
    159 
Note: See TracChangeset for help on using the changeset viewer.