source: src/utilities/monad.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 6.2 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  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)
16}.
17
18record 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
33notation "m »= f" with precedence 47
34  for @{'m_bind $m $f) }.
35
36notation > "!_ e; e'"
37  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
38notation > "! ident v ← e; e'"
39  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
40notation > "! ident v : ty ← e; e'"
41  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
42notation < "vbox(! \nbsp ident v ← e ; break e')"
43  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
44notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
45  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
46notation > "! 〈ident v1, ident v2〉 ← e ; e'"
47  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
48notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
49  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
50notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
51  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
52notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; break e')"
53  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
54 
55notation > "'return' t" with precedence 30 for @{'m_return $t}.
56notation < "'return' \nbsp t" with precedence 30 for @{'m_return $t}.
57
58(*
59notation > "!!_ e; e'"
60  with precedence 40 for @{'sm_bind ${e} (λ_.${e'})}.
61notation > "!! ident v ← e; e'"
62  with precedence 40 for @{'sm_bind ${e} (λ${ident v}.${e'})}.
63notation > "!! ident v : ty ← e; e'"
64  with precedence 40 for @{'sm_bind ${e} (λ${ident v} : ${ty}.${e'})}.
65notation < "vbox(!!  ident v ← e; break e')"
66  with precedence 40 for @{'sm_bind ${e} (λ${ident v}.${e'})}.
67notation < "vbox(!!  ident v : ty ← e; break e')"
68  with precedence 40 for @{'sm_bind ${e} (λ${ident v} : ${ty}.${e'})}.
69notation > "!! 〈ident v1, ident v2〉 ← e; e'"
70  with precedence 40 for @{'sm_bind ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
71notation > "!! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'"
72  with precedence 40 for @{'sm_bind ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
73notation < "vbox(!! \nbsp 〈ident v1, ident v2〉 ← e; break e')"
74  with precedence 40 for @{'sm_bind ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
75notation < "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
78notation "m !»= f" with precedence 40
79  for @{'sm_bind $m $f) }.
80
81notation "'sreturn' t" with precedence 30 for @{'sm_return $t}.
82
83interpretation "setoid monad bind" 'sm_bind m f = (sm_bind ? ? ? m f).
84interpretation "setoid monad return" 'sm_return x = (sm_return ? ? x).
85*)
86
87interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f).
88interpretation "setoid monad return" 'm_return x = (sm_return ? ? x).
89interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
90interpretation "monad return" 'm_return x = (m_return ? ? x).
91
92(* add structure and properties as needed *)
93record Monad : Type[1] ≝ {
94  m_def :> MonadDefinition ;
95  m_map : ∀X, Y. (X → Y) → monad m_def X → monad m_def Y ;
96  m_map2 : ∀X, Y, Z. (X → Y → Z) →
97    monad m_def X → monad m_def Y → monad m_def Z;
98  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}.
101
102definition MakeMonad : MonadDefinition → Monad ≝ λM.
103  mk_Monad M
104  (* map *)
105  (λX,Y,f,m.
106    ! x ← m ;
107    return f x)
108  (* map2 *)
109  (λX,Y,Z,f,m,n.
110    ! x ← m ;
111    ! y ← n ;
112    return (f x y))
113  (* bind2 *)
114  (λX,Y,Z,m,f.
115    ! p ← m ;
116    let 〈x, y〉 ≝ p in
117    f x y)
118  (* join *)
119  (λX,m.! x ← m ; x).
120(* add structure and properties as needed *)
121record SetoidMonad : Type[1] ≝ {
122  sm_def :> SetoidMonadDefinition ;
123  sm_map : ∀X, Y. (X → Y) → std_monad sm_def X → std_monad sm_def Y ;
124  sm_map2 : ∀X, Y, Z. (X → Y → Z) →
125    std_monad sm_def X → std_monad sm_def Y → std_monad sm_def Z;
126  sm_bind2 : ∀X,Y,Z.std_monad sm_def (X×Y) →
127    (X → Y → std_monad sm_def Z) → std_monad sm_def Z
128}.
129
130definition MakeSetoidMonad : SetoidMonadDefinition → SetoidMonad ≝ λM.
131  mk_SetoidMonad M
132  (* map *)
133  (λX,Y,f,m.
134    ! x ← m ;
135    return f x)
136  (* map2 *)
137  (λX,Y,Z,f,m,n.
138    ! x ← m ;
139    ! y ← n ;
140    return (f x y))
141  (* bind2 *)
142  (λX,Y,Z,m,f.
143    ! p ← m ;
144    let 〈x, y〉 ≝ p in
145    f x y).
146
147interpretation "monad bind2" 'm_bind2 m f = (sm_map2 ? ? ? ? m f).
148
149
150record MonadTransformer : Type[1] ≝ {
151  monad_trans : MonadDefinition → MonadDefinition ;
152  m_lift : ∀M,X. monad M X → monad (monad_trans M) X ;
153  m_lift_return : ∀M,X.∀x : X. m_lift M X (return x) = return x ;
154  m_lift_bind : ∀M,X,Y.∀m : monad M X.∀f : X → monad M Y.
155    m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x)
156}.
157
158
159
Note: See TracBrowser for help on using the repository browser.