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