1 | include "basics/types.ma". |
---|
2 | include "basics/relations.ma". |
---|
3 | include "utilities/setoids.ma". |
---|
4 | include "utilities/proper.ma". |
---|
5 | |
---|
6 | record 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 | |
---|
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 |
---|
34 | for @{'m_bind $m $f) }. |
---|
35 | |
---|
36 | notation > "!_ e; e'" |
---|
37 | with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. |
---|
38 | notation > "! ident v ← e; e'" |
---|
39 | with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. |
---|
40 | notation > "! ident v : ty ← e; e'" |
---|
41 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
42 | notation < "vbox(! \nbsp ident v ← e ; break e')" |
---|
43 | with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}. |
---|
44 | notation < "vbox(! \nbsp ident v : ty ← e ; break e')" |
---|
45 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
46 | notation > "! 〈ident v1, ident v2〉 ← e ; e'" |
---|
47 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
48 | notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" |
---|
49 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. |
---|
50 | notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')" |
---|
51 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
52 | notation < "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 | |
---|
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 | *) |
---|
86 | |
---|
87 | interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f). |
---|
88 | interpretation "setoid monad return" 'm_return x = (sm_return ? ? x). |
---|
89 | interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f). |
---|
90 | interpretation "monad return" 'm_return x = (m_return ? ? x). |
---|
91 | |
---|
92 | (* add structure and properties as needed *) |
---|
93 | record 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 | |
---|
102 | definition 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 *) |
---|
121 | record 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 | |
---|
130 | definition 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 | |
---|
147 | interpretation "monad bind2" 'm_bind2 m f = (sm_map2 ? ? ? ? m f). |
---|
148 | |
---|
149 | |
---|
150 | record 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 | |
---|