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