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