haftmann@20946
|
1 |
theory Classes
|
haftmann@28565
|
2 |
imports Main Setup
|
haftmann@20946
|
3 |
begin
|
haftmann@20946
|
4 |
|
haftmann@20946
|
5 |
section {* Introduction *}
|
haftmann@20946
|
6 |
|
haftmann@20946
|
7 |
text {*
|
paulson@31684
|
8 |
Type classes were introduced by Wadler and Blott \cite{wadler89how}
|
paulson@31684
|
9 |
into the Haskell language to allow for a reasonable implementation
|
haftmann@22317
|
10 |
of overloading\footnote{throughout this tutorial, we are referring
|
haftmann@22317
|
11 |
to classical Haskell 1.0 type classes, not considering
|
haftmann@22317
|
12 |
later additions in expressiveness}.
|
haftmann@22317
|
13 |
As a canonical example, a polymorphic equality function
|
haftmann@22317
|
14 |
@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
|
haftmann@22550
|
15 |
types for @{text "\<alpha>"}, which is achieved by splitting introduction
|
haftmann@22317
|
16 |
of the @{text eq} function from its overloaded definitions by means
|
haftmann@22317
|
17 |
of @{text class} and @{text instance} declarations:
|
haftmann@30210
|
18 |
\footnote{syntax here is a kind of isabellized Haskell}
|
haftmann@20946
|
19 |
|
haftmann@28565
|
20 |
\begin{quote}
|
haftmann@20946
|
21 |
|
haftmann@30210
|
22 |
\noindent@{text "class eq where"} \\
|
haftmann@28565
|
23 |
\hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
|
haftmann@20946
|
24 |
|
haftmann@28565
|
25 |
\medskip\noindent@{text "instance nat \<Colon> eq where"} \\
|
haftmann@28565
|
26 |
\hspace*{2ex}@{text "eq 0 0 = True"} \\
|
haftmann@28565
|
27 |
\hspace*{2ex}@{text "eq 0 _ = False"} \\
|
haftmann@28565
|
28 |
\hspace*{2ex}@{text "eq _ 0 = False"} \\
|
haftmann@28565
|
29 |
\hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
|
haftmann@22317
|
30 |
|
haftmann@28948
|
31 |
\medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
|
haftmann@28565
|
32 |
\hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
|
haftmann@22317
|
33 |
|
haftmann@28565
|
34 |
\medskip\noindent@{text "class ord extends eq where"} \\
|
haftmann@28565
|
35 |
\hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
|
haftmann@28565
|
36 |
\hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
|
haftmann@28565
|
37 |
|
haftmann@28565
|
38 |
\end{quote}
|
haftmann@28565
|
39 |
|
haftmann@28565
|
40 |
\noindent Type variables are annotated with (finitely many) classes;
|
haftmann@22317
|
41 |
these annotations are assertions that a particular polymorphic type
|
haftmann@22317
|
42 |
provides definitions for overloaded functions.
|
haftmann@22317
|
43 |
|
haftmann@22317
|
44 |
Indeed, type classes not only allow for simple overloading
|
haftmann@22317
|
45 |
but form a generic calculus, an instance of order-sorted
|
paulson@31684
|
46 |
algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
|
haftmann@22317
|
47 |
|
paulson@31684
|
48 |
From a software engineering point of view, type classes
|
haftmann@28540
|
49 |
roughly correspond to interfaces in object-oriented languages like Java;
|
haftmann@22317
|
50 |
so, it is naturally desirable that type classes do not only
|
haftmann@24991
|
51 |
provide functions (class parameters) but also state specifications
|
haftmann@22317
|
52 |
implementations must obey. For example, the @{text "class eq"}
|
haftmann@22550
|
53 |
above could be given the following specification, demanding that
|
haftmann@22550
|
54 |
@{text "class eq"} is an equivalence relation obeying reflexivity,
|
haftmann@22550
|
55 |
symmetry and transitivity:
|
haftmann@22317
|
56 |
|
haftmann@28565
|
57 |
\begin{quote}
|
haftmann@22317
|
58 |
|
haftmann@28565
|
59 |
\noindent@{text "class eq where"} \\
|
haftmann@28565
|
60 |
\hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
|
haftmann@28565
|
61 |
@{text "satisfying"} \\
|
haftmann@28565
|
62 |
\hspace*{2ex}@{text "refl: eq x x"} \\
|
haftmann@28565
|
63 |
\hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
|
haftmann@28565
|
64 |
\hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
|
haftmann@28565
|
65 |
|
haftmann@28565
|
66 |
\end{quote}
|
haftmann@28565
|
67 |
|
paulson@31684
|
68 |
\noindent From a theoretical point of view, type classes are lightweight
|
haftmann@22347
|
69 |
modules; Haskell type classes may be emulated by
|
haftmann@22317
|
70 |
SML functors \cite{classes_modules}.
|
haftmann@22317
|
71 |
Isabelle/Isar offers a discipline of type classes which brings
|
haftmann@22317
|
72 |
all those aspects together:
|
haftmann@22317
|
73 |
|
haftmann@22317
|
74 |
\begin{enumerate}
|
haftmann@24991
|
75 |
\item specifying abstract parameters together with
|
haftmann@22317
|
76 |
corresponding specifications,
|
haftmann@28540
|
77 |
\item instantiating those abstract parameters by a particular
|
haftmann@22317
|
78 |
type
|
haftmann@22317
|
79 |
\item in connection with a ``less ad-hoc'' approach to overloading,
|
paulson@31684
|
80 |
\item with a direct link to the Isabelle module system:
|
paulson@31684
|
81 |
locales \cite{kammueller-locales}.
|
haftmann@22317
|
82 |
\end{enumerate}
|
haftmann@22317
|
83 |
|
haftmann@22550
|
84 |
\noindent Isar type classes also directly support code generation
|
paulson@31684
|
85 |
in a Haskell like fashion. Internally, they are mapped to more primitive
|
paulson@31684
|
86 |
Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
|
haftmann@22317
|
87 |
|
haftmann@22317
|
88 |
This tutorial demonstrates common elements of structured specifications
|
haftmann@22317
|
89 |
and abstract reasoning with type classes by the algebraic hierarchy of
|
haftmann@20946
|
90 |
semigroups, monoids and groups. Our background theory is that of
|
haftmann@23956
|
91 |
Isabelle/HOL \cite{isa-tutorial}, for which some
|
haftmann@22317
|
92 |
familiarity is assumed.
|
haftmann@20946
|
93 |
*}
|
haftmann@20946
|
94 |
|
haftmann@22317
|
95 |
section {* A simple algebra example \label{sec:example} *}
|
haftmann@20946
|
96 |
|
haftmann@20946
|
97 |
subsection {* Class definition *}
|
haftmann@20946
|
98 |
|
haftmann@20946
|
99 |
text {*
|
haftmann@20946
|
100 |
Depending on an arbitrary type @{text "\<alpha>"}, class @{text
|
haftmann@28565
|
101 |
"semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
|
haftmann@20946
|
102 |
assumed to be associative:
|
haftmann@20946
|
103 |
*}
|
haftmann@20946
|
104 |
|
haftmann@29705
|
105 |
class %quote semigroup =
|
haftmann@28565
|
106 |
fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
|
haftmann@28565
|
107 |
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
|
haftmann@20946
|
108 |
|
haftmann@20946
|
109 |
text {*
|
haftmann@28565
|
110 |
\noindent This @{command class} specification consists of two
|
haftmann@28565
|
111 |
parts: the \qn{operational} part names the class parameter
|
haftmann@28565
|
112 |
(@{element "fixes"}), the \qn{logical} part specifies properties on them
|
haftmann@28565
|
113 |
(@{element "assumes"}). The local @{element "fixes"} and
|
haftmann@28565
|
114 |
@{element "assumes"} are lifted to the theory toplevel,
|
haftmann@28565
|
115 |
yielding the global
|
haftmann@24991
|
116 |
parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
|
haftmann@28565
|
117 |
global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
|
haftmann@22479
|
118 |
z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
|
haftmann@20946
|
119 |
*}
|
haftmann@20946
|
120 |
|
haftmann@20946
|
121 |
|
haftmann@20946
|
122 |
subsection {* Class instantiation \label{sec:class_inst} *}
|
haftmann@20946
|
123 |
|
haftmann@20946
|
124 |
text {*
|
haftmann@28565
|
125 |
The concrete type @{typ int} is made a @{class semigroup}
|
haftmann@24991
|
126 |
instance by providing a suitable definition for the class parameter
|
haftmann@28565
|
127 |
@{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
|
haftmann@28565
|
128 |
This is accomplished by the @{command instantiation} target:
|
haftmann@20946
|
129 |
*}
|
haftmann@20946
|
130 |
|
haftmann@28565
|
131 |
instantiation %quote int :: semigroup
|
haftmann@28565
|
132 |
begin
|
haftmann@25533
|
133 |
|
haftmann@28565
|
134 |
definition %quote
|
haftmann@28565
|
135 |
mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
|
haftmann@25533
|
136 |
|
haftmann@28565
|
137 |
instance %quote proof
|
haftmann@28565
|
138 |
fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
|
haftmann@28565
|
139 |
then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
|
haftmann@28566
|
140 |
unfolding mult_int_def .
|
haftmann@28565
|
141 |
qed
|
haftmann@20946
|
142 |
|
haftmann@28565
|
143 |
end %quote
|
haftmann@25533
|
144 |
|
haftmann@20946
|
145 |
text {*
|
paulson@31684
|
146 |
\noindent @{command instantiation} defines class parameters
|
haftmann@25533
|
147 |
at a particular instance using common specification tools (here,
|
haftmann@28565
|
148 |
@{command definition}). The concluding @{command instance}
|
haftmann@25533
|
149 |
opens a proof that the given parameters actually conform
|
haftmann@25533
|
150 |
to the class specification. Note that the first proof step
|
haftmann@28565
|
151 |
is the @{method default} method,
|
haftmann@28565
|
152 |
which for such instance proofs maps to the @{method intro_classes} method.
|
paulson@31684
|
153 |
This reduces an instance judgement to the relevant primitive
|
paulson@31684
|
154 |
proof goals; typically it is the first method applied
|
haftmann@22317
|
155 |
in an instantiation proof.
|
haftmann@22317
|
156 |
|
haftmann@28565
|
157 |
From now on, the type-checker will consider @{typ int}
|
haftmann@28565
|
158 |
as a @{class semigroup} automatically, i.e.\ any general results
|
haftmann@25533
|
159 |
are immediately available on concrete instances.
|
haftmann@28565
|
160 |
|
paulson@31684
|
161 |
\medskip Another instance of @{class semigroup} yields the natural numbers:
|
haftmann@20946
|
162 |
*}
|
haftmann@20946
|
163 |
|
haftmann@28565
|
164 |
instantiation %quote nat :: semigroup
|
haftmann@28565
|
165 |
begin
|
haftmann@25533
|
166 |
|
haftmann@28565
|
167 |
primrec %quote mult_nat where
|
haftmann@28565
|
168 |
"(0\<Colon>nat) \<otimes> n = n"
|
haftmann@28565
|
169 |
| "Suc m \<otimes> n = Suc (m \<otimes> n)"
|
haftmann@25533
|
170 |
|
haftmann@28565
|
171 |
instance %quote proof
|
haftmann@28565
|
172 |
fix m n q :: nat
|
haftmann@28565
|
173 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
|
haftmann@28565
|
174 |
by (induct m) auto
|
haftmann@28565
|
175 |
qed
|
haftmann@20946
|
176 |
|
haftmann@28565
|
177 |
end %quote
|
haftmann@25247
|
178 |
|
haftmann@25871
|
179 |
text {*
|
haftmann@25871
|
180 |
\noindent Note the occurence of the name @{text mult_nat}
|
haftmann@25871
|
181 |
in the primrec declaration; by default, the local name of
|
haftmann@31675
|
182 |
a class operation @{text f} to be instantiated on type constructor
|
haftmann@31675
|
183 |
@{text \<kappa>} is mangled as @{text f_\<kappa>}. In case of uncertainty,
|
haftmann@28565
|
184 |
these names may be inspected using the @{command "print_context"} command
|
haftmann@25871
|
185 |
or the corresponding ProofGeneral button.
|
haftmann@25871
|
186 |
*}
|
haftmann@25871
|
187 |
|
haftmann@25247
|
188 |
subsection {* Lifting and parametric types *}
|
haftmann@25247
|
189 |
|
haftmann@20946
|
190 |
text {*
|
paulson@31684
|
191 |
Overloaded definitions given at a class instantiation
|
haftmann@25247
|
192 |
may include recursion over the syntactic structure of types.
|
haftmann@25247
|
193 |
As a canonical example, we model product semigroups
|
haftmann@25247
|
194 |
using our simple algebra:
|
haftmann@20946
|
195 |
*}
|
haftmann@20946
|
196 |
|
haftmann@28565
|
197 |
instantiation %quote * :: (semigroup, semigroup) semigroup
|
haftmann@28565
|
198 |
begin
|
haftmann@25533
|
199 |
|
haftmann@28565
|
200 |
definition %quote
|
haftmann@31930
|
201 |
mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
|
haftmann@25533
|
202 |
|
haftmann@28565
|
203 |
instance %quote proof
|
haftmann@31930
|
204 |
fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
|
haftmann@31930
|
205 |
show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
|
haftmann@28566
|
206 |
unfolding mult_prod_def by (simp add: assoc)
|
haftmann@28565
|
207 |
qed
|
haftmann@20946
|
208 |
|
haftmann@28565
|
209 |
end %quote
|
haftmann@25533
|
210 |
|
haftmann@25247
|
211 |
text {*
|
haftmann@31675
|
212 |
\noindent Associativity of product semigroups is established using
|
haftmann@28565
|
213 |
the definition of @{text "(\<otimes>)"} on products and the hypothetical
|
huffman@27505
|
214 |
associativity of the type components; these hypotheses
|
paulson@31684
|
215 |
are legitimate due to the @{class semigroup} constraints imposed
|
haftmann@28565
|
216 |
on the type components by the @{command instance} proposition.
|
haftmann@25247
|
217 |
Indeed, this pattern often occurs with parametric types
|
haftmann@25247
|
218 |
and type classes.
|
haftmann@25247
|
219 |
*}
|
haftmann@20946
|
220 |
|
haftmann@25247
|
221 |
|
haftmann@25247
|
222 |
subsection {* Subclassing *}
|
haftmann@20946
|
223 |
|
haftmann@20946
|
224 |
text {*
|
haftmann@28565
|
225 |
We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
|
haftmann@28565
|
226 |
by extending @{class semigroup}
|
haftmann@28565
|
227 |
with one additional parameter @{text neutral} together
|
paulson@31684
|
228 |
with its characteristic property:
|
haftmann@20946
|
229 |
*}
|
haftmann@20946
|
230 |
|
haftmann@28565
|
231 |
class %quote monoidl = semigroup +
|
haftmann@28565
|
232 |
fixes neutral :: "\<alpha>" ("\<one>")
|
haftmann@28565
|
233 |
assumes neutl: "\<one> \<otimes> x = x"
|
haftmann@20946
|
234 |
|
haftmann@20946
|
235 |
text {*
|
haftmann@25247
|
236 |
\noindent Again, we prove some instances, by
|
haftmann@24991
|
237 |
providing suitable parameter definitions and proofs for the
|
huffman@27505
|
238 |
additional specifications. Observe that instantiations
|
haftmann@25533
|
239 |
for types with the same arity may be simultaneous:
|
haftmann@20946
|
240 |
*}
|
haftmann@20946
|
241 |
|
haftmann@28566
|
242 |
instantiation %quote nat and int :: monoidl
|
haftmann@28566
|
243 |
begin
|
haftmann@25533
|
244 |
|
haftmann@28566
|
245 |
definition %quote
|
haftmann@28566
|
246 |
neutral_nat_def: "\<one> = (0\<Colon>nat)"
|
haftmann@25533
|
247 |
|
haftmann@28566
|
248 |
definition %quote
|
haftmann@28566
|
249 |
neutral_int_def: "\<one> = (0\<Colon>int)"
|
haftmann@25533
|
250 |
|
haftmann@28566
|
251 |
instance %quote proof
|
haftmann@28566
|
252 |
fix n :: nat
|
haftmann@28566
|
253 |
show "\<one> \<otimes> n = n"
|
haftmann@28566
|
254 |
unfolding neutral_nat_def by simp
|
haftmann@28566
|
255 |
next
|
haftmann@28566
|
256 |
fix k :: int
|
haftmann@28566
|
257 |
show "\<one> \<otimes> k = k"
|
haftmann@28566
|
258 |
unfolding neutral_int_def mult_int_def by simp
|
haftmann@28566
|
259 |
qed
|
haftmann@20946
|
260 |
|
haftmann@28566
|
261 |
end %quote
|
haftmann@25533
|
262 |
|
haftmann@28566
|
263 |
instantiation %quote * :: (monoidl, monoidl) monoidl
|
haftmann@28566
|
264 |
begin
|
haftmann@25533
|
265 |
|
haftmann@28566
|
266 |
definition %quote
|
haftmann@28566
|
267 |
neutral_prod_def: "\<one> = (\<one>, \<one>)"
|
haftmann@25533
|
268 |
|
haftmann@28566
|
269 |
instance %quote proof
|
haftmann@28566
|
270 |
fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
|
haftmann@28566
|
271 |
show "\<one> \<otimes> p = p"
|
haftmann@28566
|
272 |
unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
|
haftmann@28566
|
273 |
qed
|
haftmann@20946
|
274 |
|
haftmann@28566
|
275 |
end %quote
|
haftmann@25533
|
276 |
|
haftmann@20946
|
277 |
text {*
|
paulson@31684
|
278 |
\noindent Fully-fledged monoids are modelled by another subclass,
|
haftmann@24991
|
279 |
which does not add new parameters but tightens the specification:
|
haftmann@20946
|
280 |
*}
|
haftmann@20946
|
281 |
|
haftmann@28566
|
282 |
class %quote monoid = monoidl +
|
haftmann@28566
|
283 |
assumes neutr: "x \<otimes> \<one> = x"
|
haftmann@20946
|
284 |
|
haftmann@28566
|
285 |
instantiation %quote nat and int :: monoid
|
haftmann@28566
|
286 |
begin
|
haftmann@25533
|
287 |
|
haftmann@28566
|
288 |
instance %quote proof
|
haftmann@28566
|
289 |
fix n :: nat
|
haftmann@28566
|
290 |
show "n \<otimes> \<one> = n"
|
haftmann@28566
|
291 |
unfolding neutral_nat_def by (induct n) simp_all
|
haftmann@28566
|
292 |
next
|
haftmann@28566
|
293 |
fix k :: int
|
haftmann@28566
|
294 |
show "k \<otimes> \<one> = k"
|
haftmann@28566
|
295 |
unfolding neutral_int_def mult_int_def by simp
|
haftmann@28566
|
296 |
qed
|
haftmann@25247
|
297 |
|
haftmann@28566
|
298 |
end %quote
|
haftmann@25533
|
299 |
|
haftmann@28566
|
300 |
instantiation %quote * :: (monoid, monoid) monoid
|
haftmann@28566
|
301 |
begin
|
haftmann@25533
|
302 |
|
haftmann@28566
|
303 |
instance %quote proof
|
haftmann@28566
|
304 |
fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
|
haftmann@28566
|
305 |
show "p \<otimes> \<one> = p"
|
haftmann@28566
|
306 |
unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
|
haftmann@28566
|
307 |
qed
|
haftmann@22317
|
308 |
|
haftmann@28566
|
309 |
end %quote
|
haftmann@25533
|
310 |
|
haftmann@22317
|
311 |
text {*
|
haftmann@28565
|
312 |
\noindent To finish our small algebra example, we add a @{text group} class
|
haftmann@22317
|
313 |
with a corresponding instance:
|
haftmann@22317
|
314 |
*}
|
haftmann@20946
|
315 |
|
haftmann@28566
|
316 |
class %quote group = monoidl +
|
haftmann@28566
|
317 |
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
|
haftmann@28566
|
318 |
assumes invl: "x\<div> \<otimes> x = \<one>"
|
haftmann@20946
|
319 |
|
haftmann@28566
|
320 |
instantiation %quote int :: group
|
haftmann@28566
|
321 |
begin
|
haftmann@25533
|
322 |
|
haftmann@28566
|
323 |
definition %quote
|
haftmann@28566
|
324 |
inverse_int_def: "i\<div> = - (i\<Colon>int)"
|
haftmann@25533
|
325 |
|
haftmann@28566
|
326 |
instance %quote proof
|
haftmann@28566
|
327 |
fix i :: int
|
haftmann@28566
|
328 |
have "-i + i = 0" by simp
|
haftmann@28566
|
329 |
then show "i\<div> \<otimes> i = \<one>"
|
haftmann@28566
|
330 |
unfolding mult_int_def neutral_int_def inverse_int_def .
|
haftmann@28566
|
331 |
qed
|
haftmann@20946
|
332 |
|
haftmann@28566
|
333 |
end %quote
|
haftmann@28566
|
334 |
|
haftmann@25533
|
335 |
|
haftmann@22317
|
336 |
section {* Type classes as locales *}
|
haftmann@22317
|
337 |
|
paulson@31684
|
338 |
subsection {* A look behind the scenes *}
|
haftmann@22317
|
339 |
|
haftmann@22347
|
340 |
text {*
|
haftmann@22347
|
341 |
The example above gives an impression how Isar type classes work
|
haftmann@22347
|
342 |
in practice. As stated in the introduction, classes also provide
|
haftmann@22347
|
343 |
a link to Isar's locale system. Indeed, the logical core of a class
|
paulson@31684
|
344 |
is nothing other than a locale:
|
haftmann@22347
|
345 |
*}
|
haftmann@22347
|
346 |
|
haftmann@29705
|
347 |
class %quote idem =
|
haftmann@22347
|
348 |
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
|
haftmann@22347
|
349 |
assumes idem: "f (f x) = f x"
|
haftmann@22317
|
350 |
|
haftmann@22317
|
351 |
text {*
|
haftmann@22347
|
352 |
\noindent essentially introduces the locale
|
haftmann@30210
|
353 |
*} (*<*)setup %invisible {* Sign.add_path "foo" *}
|
haftmann@30210
|
354 |
(*>*)
|
haftmann@28566
|
355 |
locale %quote idem =
|
haftmann@22347
|
356 |
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
|
haftmann@22347
|
357 |
assumes idem: "f (f x) = f x"
|
haftmann@22347
|
358 |
|
haftmann@22550
|
359 |
text {* \noindent together with corresponding constant(s): *}
|
haftmann@22347
|
360 |
|
haftmann@28566
|
361 |
consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
|
haftmann@22347
|
362 |
|
haftmann@22550
|
363 |
text {*
|
haftmann@22550
|
364 |
\noindent The connection to the type system is done by means
|
haftmann@35282
|
365 |
of a primitive type class
|
haftmann@30210
|
366 |
*} (*<*)setup %invisible {* Sign.add_path "foo" *}
|
haftmann@30210
|
367 |
(*>*)
|
haftmann@35282
|
368 |
classes %quote idem < type
|
haftmann@35282
|
369 |
(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
|
haftmann@35282
|
370 |
setup %invisible {* Sign.parent_path *}(*>*)
|
haftmann@22347
|
371 |
|
haftmann@22550
|
372 |
text {* \noindent together with a corresponding interpretation: *}
|
haftmann@22347
|
373 |
|
haftmann@29513
|
374 |
interpretation %quote idem_class:
|
wenzelm@29294
|
375 |
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
|
haftmann@35282
|
376 |
(*<*)proof qed (rule idem)(*>*)
|
haftmann@28565
|
377 |
|
haftmann@22347
|
378 |
text {*
|
paulson@31684
|
379 |
\noindent This gives you the full power of the Isabelle module system;
|
haftmann@22347
|
380 |
conclusions in locale @{text idem} are implicitly propagated
|
haftmann@22479
|
381 |
to class @{text idem}.
|
haftmann@30210
|
382 |
*} (*<*)setup %invisible {* Sign.parent_path *}
|
haftmann@30210
|
383 |
(*>*)
|
haftmann@20946
|
384 |
subsection {* Abstract reasoning *}
|
haftmann@20946
|
385 |
|
haftmann@20946
|
386 |
text {*
|
haftmann@22347
|
387 |
Isabelle locales enable reasoning at a general level, while results
|
haftmann@20946
|
388 |
are implicitly transferred to all instances. For example, we can
|
haftmann@20946
|
389 |
now establish the @{text "left_cancel"} lemma for groups, which
|
haftmann@25247
|
390 |
states that the function @{text "(x \<otimes>)"} is injective:
|
haftmann@20946
|
391 |
*}
|
haftmann@20946
|
392 |
|
haftmann@28566
|
393 |
lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
|
haftmann@28566
|
394 |
proof
|
haftmann@28566
|
395 |
assume "x \<otimes> y = x \<otimes> z"
|
haftmann@28566
|
396 |
then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
|
haftmann@28566
|
397 |
then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
|
haftmann@28566
|
398 |
then show "y = z" using neutl and invl by simp
|
haftmann@28566
|
399 |
next
|
haftmann@28566
|
400 |
assume "y = z"
|
haftmann@28566
|
401 |
then show "x \<otimes> y = x \<otimes> z" by simp
|
haftmann@28566
|
402 |
qed
|
haftmann@20946
|
403 |
|
haftmann@20946
|
404 |
text {*
|
haftmann@28565
|
405 |
\noindent Here the \qt{@{keyword "in"} @{class group}} target specification
|
haftmann@20946
|
406 |
indicates that the result is recorded within that context for later
|
haftmann@28565
|
407 |
use. This local theorem is also lifted to the global one @{fact
|
haftmann@22479
|
408 |
"group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
|
haftmann@20946
|
409 |
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
|
haftmann@20946
|
410 |
@{text "group"} before, we may refer to that fact as well: @{prop
|
haftmann@22479
|
411 |
[source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
|
haftmann@20946
|
412 |
*}
|
haftmann@20946
|
413 |
|
haftmann@20946
|
414 |
|
haftmann@23956
|
415 |
subsection {* Derived definitions *}
|
haftmann@20946
|
416 |
|
haftmann@20946
|
417 |
text {*
|
haftmann@35282
|
418 |
Isabelle locales are targets which support local definitions:
|
haftmann@23956
|
419 |
*}
|
haftmann@20946
|
420 |
|
haftmann@28566
|
421 |
primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
|
haftmann@28566
|
422 |
"pow_nat 0 x = \<one>"
|
haftmann@28566
|
423 |
| "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
|
haftmann@23956
|
424 |
|
haftmann@23956
|
425 |
text {*
|
haftmann@23956
|
426 |
\noindent If the locale @{text group} is also a class, this local
|
haftmann@23956
|
427 |
definition is propagated onto a global definition of
|
haftmann@23956
|
428 |
@{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
|
haftmann@23956
|
429 |
with corresponding theorems
|
haftmann@23956
|
430 |
|
haftmann@23956
|
431 |
@{thm pow_nat.simps [no_vars]}.
|
haftmann@23956
|
432 |
|
haftmann@23956
|
433 |
\noindent As you can see from this example, for local
|
haftmann@23956
|
434 |
definitions you may use any specification tool
|
paulson@31684
|
435 |
which works together with locales, such as Krauss's recursive function package
|
paulson@31684
|
436 |
\cite{krauss2006}.
|
haftmann@23956
|
437 |
*}
|
haftmann@23956
|
438 |
|
haftmann@23956
|
439 |
|
haftmann@25247
|
440 |
subsection {* A functor analogy *}
|
haftmann@25247
|
441 |
|
haftmann@25247
|
442 |
text {*
|
paulson@31684
|
443 |
We introduced Isar classes by analogy to type classes in
|
haftmann@25247
|
444 |
functional programming; if we reconsider this in the
|
haftmann@25247
|
445 |
context of what has been said about type classes and locales,
|
haftmann@25247
|
446 |
we can drive this analogy further by stating that type
|
paulson@31684
|
447 |
classes essentially correspond to functors that have
|
haftmann@25247
|
448 |
a canonical interpretation as type classes.
|
paulson@31684
|
449 |
There is also the possibility of other interpretations.
|
paulson@31684
|
450 |
For example, @{text list}s also form a monoid with
|
haftmann@28565
|
451 |
@{text append} and @{term "[]"} as operations, but it
|
haftmann@25247
|
452 |
seems inappropriate to apply to lists
|
huffman@27505
|
453 |
the same operations as for genuinely algebraic types.
|
paulson@31684
|
454 |
In such a case, we can simply make a particular interpretation
|
haftmann@25247
|
455 |
of monoids for lists:
|
haftmann@25247
|
456 |
*}
|
haftmann@25247
|
457 |
|
wenzelm@30732
|
458 |
interpretation %quote list_monoid: monoid append "[]"
|
haftmann@28947
|
459 |
proof qed auto
|
haftmann@25247
|
460 |
|
haftmann@25247
|
461 |
text {*
|
haftmann@25247
|
462 |
\noindent This enables us to apply facts on monoids
|
haftmann@25247
|
463 |
to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
|
haftmann@25247
|
464 |
|
haftmann@25247
|
465 |
When using this interpretation pattern, it may also
|
haftmann@25247
|
466 |
be appropriate to map derived definitions accordingly:
|
haftmann@25247
|
467 |
*}
|
haftmann@25247
|
468 |
|
haftmann@28566
|
469 |
primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
|
haftmann@28566
|
470 |
"replicate 0 _ = []"
|
haftmann@28566
|
471 |
| "replicate (Suc n) xs = xs @ replicate n xs"
|
haftmann@25247
|
472 |
|
wenzelm@30732
|
473 |
interpretation %quote list_monoid: monoid append "[]" where
|
haftmann@28566
|
474 |
"monoid.pow_nat append [] = replicate"
|
haftmann@28566
|
475 |
proof -
|
haftmann@29513
|
476 |
interpret monoid append "[]" ..
|
haftmann@28566
|
477 |
show "monoid.pow_nat append [] = replicate"
|
haftmann@28566
|
478 |
proof
|
haftmann@28566
|
479 |
fix n
|
haftmann@28566
|
480 |
show "monoid.pow_nat append [] n = replicate n"
|
haftmann@28566
|
481 |
by (induct n) auto
|
haftmann@28566
|
482 |
qed
|
haftmann@28566
|
483 |
qed intro_locales
|
haftmann@25247
|
484 |
|
haftmann@31249
|
485 |
text {*
|
haftmann@31249
|
486 |
\noindent This pattern is also helpful to reuse abstract
|
haftmann@31249
|
487 |
specifications on the \emph{same} type. For example, think of a
|
haftmann@31249
|
488 |
class @{text preorder}; for type @{typ nat}, there are at least two
|
haftmann@31249
|
489 |
possible instances: the natural order or the order induced by the
|
haftmann@31249
|
490 |
divides relation. But only one of these instances can be used for
|
haftmann@31249
|
491 |
@{command instantiation}; using the locale behind the class @{text
|
haftmann@31249
|
492 |
preorder}, it is still possible to utilise the same abstract
|
haftmann@31249
|
493 |
specification again using @{command interpretation}.
|
haftmann@31249
|
494 |
*}
|
haftmann@25247
|
495 |
|
haftmann@24991
|
496 |
subsection {* Additional subclass relations *}
|
haftmann@22347
|
497 |
|
haftmann@22347
|
498 |
text {*
|
haftmann@31249
|
499 |
Any @{text "group"} is also a @{text "monoid"}; this can be made
|
haftmann@31249
|
500 |
explicit by claiming an additional subclass relation, together with
|
haftmann@31249
|
501 |
a proof of the logical difference:
|
haftmann@22347
|
502 |
*}
|
haftmann@22347
|
503 |
|
haftmann@28566
|
504 |
subclass %quote (in group) monoid
|
haftmann@28947
|
505 |
proof
|
haftmann@28566
|
506 |
fix x
|
haftmann@28566
|
507 |
from invl have "x\<div> \<otimes> x = \<one>" by simp
|
haftmann@28566
|
508 |
with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
|
haftmann@28566
|
509 |
with left_cancel show "x \<otimes> \<one> = x" by simp
|
haftmann@28566
|
510 |
qed
|
haftmann@23956
|
511 |
|
haftmann@23956
|
512 |
text {*
|
haftmann@30210
|
513 |
The logical proof is carried out on the locale level.
|
haftmann@28947
|
514 |
Afterwards it is propagated
|
haftmann@23956
|
515 |
to the type system, making @{text group} an instance of
|
haftmann@25247
|
516 |
@{text monoid} by adding an additional edge
|
haftmann@25247
|
517 |
to the graph of subclass relations
|
paulson@31684
|
518 |
(\figref{fig:subclass}).
|
haftmann@25247
|
519 |
|
haftmann@25247
|
520 |
\begin{figure}[htbp]
|
haftmann@25247
|
521 |
\begin{center}
|
haftmann@25247
|
522 |
\small
|
haftmann@25247
|
523 |
\unitlength 0.6mm
|
haftmann@25247
|
524 |
\begin{picture}(40,60)(0,0)
|
haftmann@25247
|
525 |
\put(20,60){\makebox(0,0){@{text semigroup}}}
|
haftmann@25247
|
526 |
\put(20,40){\makebox(0,0){@{text monoidl}}}
|
haftmann@25247
|
527 |
\put(00,20){\makebox(0,0){@{text monoid}}}
|
haftmann@25247
|
528 |
\put(40,00){\makebox(0,0){@{text group}}}
|
haftmann@25247
|
529 |
\put(20,55){\vector(0,-1){10}}
|
haftmann@25247
|
530 |
\put(15,35){\vector(-1,-1){10}}
|
haftmann@25247
|
531 |
\put(25,35){\vector(1,-3){10}}
|
haftmann@25247
|
532 |
\end{picture}
|
haftmann@25247
|
533 |
\hspace{8em}
|
haftmann@25247
|
534 |
\begin{picture}(40,60)(0,0)
|
haftmann@25247
|
535 |
\put(20,60){\makebox(0,0){@{text semigroup}}}
|
haftmann@25247
|
536 |
\put(20,40){\makebox(0,0){@{text monoidl}}}
|
haftmann@25247
|
537 |
\put(00,20){\makebox(0,0){@{text monoid}}}
|
haftmann@25247
|
538 |
\put(40,00){\makebox(0,0){@{text group}}}
|
haftmann@25247
|
539 |
\put(20,55){\vector(0,-1){10}}
|
haftmann@25247
|
540 |
\put(15,35){\vector(-1,-1){10}}
|
haftmann@25247
|
541 |
\put(05,15){\vector(3,-1){30}}
|
haftmann@25247
|
542 |
\end{picture}
|
haftmann@25247
|
543 |
\caption{Subclass relationship of monoids and groups:
|
haftmann@25247
|
544 |
before and after establishing the relationship
|
haftmann@30134
|
545 |
@{text "group \<subseteq> monoid"}; transitive edges are left out.}
|
haftmann@25247
|
546 |
\label{fig:subclass}
|
haftmann@25247
|
547 |
\end{center}
|
haftmann@25247
|
548 |
\end{figure}
|
haftmann@30210
|
549 |
|
haftmann@25247
|
550 |
For illustration, a derived definition
|
paulson@31684
|
551 |
in @{text group} using @{text pow_nat}
|
haftmann@23956
|
552 |
*}
|
haftmann@23956
|
553 |
|
haftmann@28565
|
554 |
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
|
haftmann@28565
|
555 |
"pow_int k x = (if k >= 0
|
haftmann@28565
|
556 |
then pow_nat (nat k) x
|
haftmann@28565
|
557 |
else (pow_nat (nat (- k)) x)\<div>)"
|
haftmann@23956
|
558 |
|
haftmann@23956
|
559 |
text {*
|
haftmann@25247
|
560 |
\noindent yields the global definition of
|
haftmann@23956
|
561 |
@{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
|
haftmann@23956
|
562 |
with the corresponding theorem @{thm pow_int_def [no_vars]}.
|
haftmann@24991
|
563 |
*}
|
haftmann@23956
|
564 |
|
haftmann@25868
|
565 |
subsection {* A note on syntax *}
|
haftmann@25868
|
566 |
|
haftmann@25868
|
567 |
text {*
|
paulson@31684
|
568 |
As a convenience, class context syntax allows references
|
huffman@27505
|
569 |
to local class operations and their global counterparts
|
haftmann@25868
|
570 |
uniformly; type inference resolves ambiguities. For example:
|
haftmann@25868
|
571 |
*}
|
haftmann@25868
|
572 |
|
haftmann@28565
|
573 |
context %quote semigroup
|
haftmann@25868
|
574 |
begin
|
haftmann@25868
|
575 |
|
haftmann@28565
|
576 |
term %quote "x \<otimes> y" -- {* example 1 *}
|
haftmann@28565
|
577 |
term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
|
haftmann@25868
|
578 |
|
haftmann@28566
|
579 |
end %quote
|
haftmann@25868
|
580 |
|
haftmann@28565
|
581 |
term %quote "x \<otimes> y" -- {* example 3 *}
|
haftmann@25868
|
582 |
|
haftmann@25868
|
583 |
text {*
|
haftmann@25868
|
584 |
\noindent Here in example 1, the term refers to the local class operation
|
haftmann@25868
|
585 |
@{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
|
haftmann@25868
|
586 |
enforces the global class operation @{text "mult [nat]"}.
|
haftmann@25868
|
587 |
In the global context in example 3, the reference is
|
haftmann@25868
|
588 |
to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
|
haftmann@25868
|
589 |
*}
|
haftmann@22347
|
590 |
|
haftmann@29705
|
591 |
section {* Further issues *}
|
haftmann@29705
|
592 |
|
haftmann@29705
|
593 |
subsection {* Type classes and code generation *}
|
haftmann@22317
|
594 |
|
haftmann@22317
|
595 |
text {*
|
haftmann@22317
|
596 |
Turning back to the first motivation for type classes,
|
haftmann@22317
|
597 |
namely overloading, it is obvious that overloading
|
haftmann@28565
|
598 |
stemming from @{command class} statements and
|
haftmann@28565
|
599 |
@{command instantiation}
|
haftmann@25533
|
600 |
targets naturally maps to Haskell type classes.
|
haftmann@22317
|
601 |
The code generator framework \cite{isabelle-codegen}
|
paulson@31684
|
602 |
takes this into account. If the target language (e.g.~SML)
|
paulson@31684
|
603 |
lacks type classes, then they
|
paulson@31684
|
604 |
are implemented by an explicit dictionary construction.
|
haftmann@28540
|
605 |
As example, let's go back to the power function:
|
haftmann@22317
|
606 |
*}
|
haftmann@22317
|
607 |
|
haftmann@28565
|
608 |
definition %quote example :: int where
|
haftmann@28565
|
609 |
"example = pow_int 10 (-2)"
|
haftmann@22317
|
610 |
|
haftmann@22317
|
611 |
text {*
|
paulson@31684
|
612 |
\noindent This maps to Haskell as follows:
|
haftmann@22317
|
613 |
*}
|
haftmann@22317
|
614 |
|
haftmann@28565
|
615 |
text %quote {*@{code_stmts example (Haskell)}*}
|
haftmann@22317
|
616 |
|
haftmann@22317
|
617 |
text {*
|
paulson@31684
|
618 |
\noindent The code in SML has explicit dictionary passing:
|
haftmann@22317
|
619 |
*}
|
haftmann@22317
|
620 |
|
haftmann@28565
|
621 |
text %quote {*@{code_stmts example (SML)}*}
|
haftmann@20946
|
622 |
|
haftmann@29705
|
623 |
subsection {* Inspecting the type class universe *}
|
haftmann@29705
|
624 |
|
haftmann@29705
|
625 |
text {*
|
haftmann@29705
|
626 |
To facilitate orientation in complex subclass structures,
|
haftmann@29705
|
627 |
two diagnostics commands are provided:
|
haftmann@29705
|
628 |
|
haftmann@29705
|
629 |
\begin{description}
|
haftmann@29705
|
630 |
|
haftmann@29705
|
631 |
\item[@{command "print_classes"}] print a list of all classes
|
haftmann@29705
|
632 |
together with associated operations etc.
|
haftmann@29705
|
633 |
|
haftmann@29705
|
634 |
\item[@{command "class_deps"}] visualizes the subclass relation
|
haftmann@29705
|
635 |
between all classes as a Hasse diagram.
|
haftmann@29705
|
636 |
|
haftmann@29705
|
637 |
\end{description}
|
haftmann@29705
|
638 |
*}
|
haftmann@29705
|
639 |
|
haftmann@20946
|
640 |
end
|