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