author  boehmes 
Tue, 07 Dec 2010 15:44:38 +0100  
changeset 41064  0c447a17770a 
parent 39743  7aef0e4a3aac 
permissions  rwrr 
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 
38812  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} 

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 

38812  44 
Indeed, type classes not only allow for simple overloading but form 
45 
a generic calculus, an instance of ordersorted algebra 

46 
\cite{nipkowsorts93,NipkowPrehofer:1993,Wenzel:1997:TPHOL}. 

20946  47 

38812  48 
From a software engineering point of view, type classes roughly 
49 
correspond to interfaces in objectoriented languages like Java; so, 

50 
it is naturally desirable that type classes do not only provide 

51 
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 

38812  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: 

22317  72 

73 
\begin{enumerate} 

24991  74 
\item specifying abstract parameters together with 
22317  75 
corresponding specifications, 
28540  76 
\item instantiating those abstract parameters by a particular 
22317  77 
type 
78 
\item in connection with a ``less adhoc'' approach to overloading, 

31691  79 
\item with a direct link to the Isabelle module system: 
80 
locales \cite{kammuellerlocales}. 

22317  81 
\end{enumerate} 
82 

38812  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{HaftmannWenzel:2006:classes}. 

22317  86 

38812  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{isatutorial}, for 

91 
which some familiarity is assumed. 

20946  92 
*} 
93 

22317  94 
section {* A simple algebra example \label{sec:example} *} 
20946  95 

96 
subsection {* Class definition *} 

97 

98 
text {* 

99 
Depending on an arbitrary type @{text "\<alpha>"}, class @{text 

28565  100 
"semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is 
20946  101 
assumed to be associative: 
102 
*} 

103 

29705  104 
class %quote semigroup = 
28565  105 
fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70) 
106 
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 

20946  107 

108 
text {* 

38812  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 

24991  114 
parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the 
38812  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)"}. 

20946  117 
*} 
118 

119 

120 
subsection {* Class instantiation \label{sec:class_inst} *} 

121 

122 
text {* 

38812  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: 

20946  127 
*} 
128 

28565  129 
instantiation %quote int :: semigroup 
130 
begin 

25533  131 

28565  132 
definition %quote 
133 
mult_int_def: "i \<otimes> j = i + (j\<Colon>int)" 

25533  134 

28565  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)" 

28566  138 
unfolding mult_int_def . 
28565  139 
qed 
20946  140 

28565  141 
end %quote 
25533  142 

20946  143 
text {* 
38812  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. 

22317  153 

38812  154 
From now on, the typechecker will consider @{typ int} as a @{class 
155 
semigroup} automatically, i.e.\ any general results are immediately 

156 
available on concrete instances. 

28565  157 

38812  158 
\medskip Another instance of @{class semigroup} yields the natural 
159 
numbers: 

20946  160 
*} 
161 

28565  162 
instantiation %quote nat :: semigroup 
163 
begin 

25533  164 

28565  165 
primrec %quote mult_nat where 
166 
"(0\<Colon>nat) \<otimes> n = n" 

167 
 "Suc m \<otimes> n = Suc (m \<otimes> n)" 

25533  168 

28565  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 

20946  174 

28565  175 
end %quote 
20946  176 

25871  177 
text {* 
38812  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. 

25871  184 
*} 
185 

25247  186 
subsection {* Lifting and parametric types *} 
187 

188 
text {* 

38812  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: 

25247  192 
*} 
193 

37706  194 
instantiation %quote prod :: (semigroup, semigroup) semigroup 
28565  195 
begin 
25533  196 

28565  197 
definition %quote 
31931  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)" 
25533  199 

28565  200 
instance %quote proof 
31931  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)" 

28566  203 
unfolding mult_prod_def by (simp add: assoc) 
28565  204 
qed 
25247  205 

28565  206 
end %quote 
25533  207 

25247  208 
text {* 
31675  209 
\noindent Associativity of product semigroups is established using 
28565  210 
the definition of @{text "(\<otimes>)"} on products and the hypothetical 
38812  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. 

25247  215 
*} 
216 

217 

218 
subsection {* Subclassing *} 

20946  219 

220 
text {* 

38812  221 
We define a subclass @{text monoidl} (a semigroup with a lefthand 
222 
neutral) by extending @{class semigroup} with one additional 

223 
parameter @{text neutral} together with its characteristic property: 

20946  224 
*} 
225 

28565  226 
class %quote monoidl = semigroup + 
227 
fixes neutral :: "\<alpha>" ("\<one>") 

228 
assumes neutl: "\<one> \<otimes> x = x" 

20946  229 

230 
text {* 

38812  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: 

20946  235 
*} 
236 

28566  237 
instantiation %quote nat and int :: monoidl 
238 
begin 

25533  239 

28566  240 
definition %quote 
241 
neutral_nat_def: "\<one> = (0\<Colon>nat)" 

25533  242 

28566  243 
definition %quote 
244 
neutral_int_def: "\<one> = (0\<Colon>int)" 

25533  245 

28566  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 

20946  255 

28566  256 
end %quote 
25533  257 

37706  258 
instantiation %quote prod :: (monoidl, monoidl) monoidl 
28566  259 
begin 
25533  260 

28566  261 
definition %quote 
262 
neutral_prod_def: "\<one> = (\<one>, \<one>)" 

25533  263 

28566  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 

20946  269 

28566  270 
end %quote 
25533  271 

20946  272 
text {* 
31691  273 
\noindent Fullyfledged monoids are modelled by another subclass, 
24991  274 
which does not add new parameters but tightens the specification: 
20946  275 
*} 
276 

28566  277 
class %quote monoid = monoidl + 
278 
assumes neutr: "x \<otimes> \<one> = x" 

20946  279 

28566  280 
instantiation %quote nat and int :: monoid 
281 
begin 

25533  282 

28566  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 

25247  292 

28566  293 
end %quote 
25533  294 

37706  295 
instantiation %quote prod :: (monoid, monoid) monoid 
28566  296 
begin 
25533  297 

28566  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 

22317  303 

28566  304 
end %quote 
25533  305 

22317  306 
text {* 
38812  307 
\noindent To finish our small algebra example, we add a @{text 
308 
group} class with a corresponding instance: 

22317  309 
*} 
20946  310 

28566  311 
class %quote group = monoidl + 
312 
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999) 

313 
assumes invl: "x\<div> \<otimes> x = \<one>" 

20946  314 

28566  315 
instantiation %quote int :: group 
316 
begin 

317 

318 
definition %quote 

319 
inverse_int_def: "i\<div> =  (i\<Colon>int)" 

25533  320 

28566  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 

25533  327 

28566  328 
end %quote 
20946  329 

25533  330 

22317  331 
section {* Type classes as locales *} 
332 

31691  333 
subsection {* A look behind the scenes *} 
22317  334 

22347  335 
text {* 
38812  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 

31691  339 
is nothing other than a locale: 
22347  340 
*} 
341 

29705  342 
class %quote idem = 
22347  343 
fixes f :: "\<alpha> \<Rightarrow> \<alpha>" 
344 
assumes idem: "f (f x) = f x" 

22317  345 

346 
text {* 

22347  347 
\noindent essentially introduces the locale 
30227  348 
*} (*<*)setup %invisible {* Sign.add_path "foo" *} 
349 
(*>*) 

28566  350 
locale %quote idem = 
22347  351 
fixes f :: "\<alpha> \<Rightarrow> \<alpha>" 
352 
assumes idem: "f (f x) = f x" 

353 

22550  354 
text {* \noindent together with corresponding constant(s): *} 
22347  355 

28566  356 
consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>" 
22347  357 

22550  358 
text {* 
359 
\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

360 
of a primitive type class 
30227  361 
*} (*<*)setup %invisible {* Sign.add_path "foo" *} 
362 
(*>*) 

35282
8fd9d555d04d
dropped references to old axclass from documentation
haftmann
parents:
31931
diff
changeset

363 
classes %quote idem < type 
8fd9d555d04d
dropped references to old axclass from documentation
haftmann
parents:
31931
diff
changeset

364 
(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x" 
8fd9d555d04d
dropped references to old axclass from documentation
haftmann
parents:
31931
diff
changeset

365 
setup %invisible {* Sign.parent_path *}(*>*) 
22347  366 

22550  367 
text {* \noindent together with a corresponding interpretation: *} 
22347  368 

29513  369 
interpretation %quote idem_class: 
29294
6cd3ac4708d2
crude adaption to intermediate class/locale version;
wenzelm
parents:
28948
diff
changeset

370 
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>" 
35282
8fd9d555d04d
dropped references to old axclass from documentation
haftmann
parents:
31931
diff
changeset

371 
(*<*)proof qed (rule idem)(*>*) 
28565  372 

22347  373 
text {* 
31691  374 
\noindent This gives you the full power of the Isabelle module system; 
22347  375 
conclusions in locale @{text idem} are implicitly propagated 
22479  376 
to class @{text idem}. 
30227  377 
*} (*<*)setup %invisible {* Sign.parent_path *} 
378 
(*>*) 

20946  379 
subsection {* Abstract reasoning *} 
380 

381 
text {* 

22347  382 
Isabelle locales enable reasoning at a general level, while results 
20946  383 
are implicitly transferred to all instances. For example, we can 
384 
now establish the @{text "left_cancel"} lemma for groups, which 

25247  385 
states that the function @{text "(x \<otimes>)"} is injective: 
20946  386 
*} 
387 

28566  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 

20946  398 

399 
text {* 

38812  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"}. 

20946  408 
*} 
409 

410 

23956  411 
subsection {* Derived definitions *} 
412 

413 
text {* 

35282
8fd9d555d04d
dropped references to old axclass from documentation
haftmann
parents:
31931
diff
changeset

414 
Isabelle locales are targets which support local definitions: 
23956  415 
*} 
416 

28566  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" 

20946  420 

421 
text {* 

23956  422 
\noindent If the locale @{text group} is also a class, this local 
38812  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 

23956  425 

426 
@{thm pow_nat.simps [no_vars]}. 

20946  427 

38812  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 

31691  431 
\cite{krauss2006}. 
23956  432 
*} 
433 

434 

25247  435 
subsection {* A functor analogy *} 
436 

437 
text {* 

38812  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: 

25247  449 
*} 
450 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30227
diff
changeset

451 
interpretation %quote list_monoid: monoid append "[]" 
28947
ac1a14b5a085
unfold_locales is default method  no need for explicit references
haftmann
parents:
28566
diff
changeset

452 
proof qed auto 
25247  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 

28566  462 
primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where 
463 
"replicate 0 _ = []" 

464 
 "replicate (Suc n) xs = xs @ replicate n xs" 

25247  465 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30227
diff
changeset

466 
interpretation %quote list_monoid: monoid append "[]" where 
28566  467 
"monoid.pow_nat append [] = replicate" 
468 
proof  

29513  469 
interpret monoid append "[]" .. 
28566  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 

25247  477 

31255  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 
*} 

25247  488 

24991  489 
subsection {* Additional subclass relations *} 
22347  490 

491 
text {* 

31255  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: 

22347  495 
*} 
496 

28566  497 
subclass %quote (in group) monoid 
28947
ac1a14b5a085
unfold_locales is default method  no need for explicit references
haftmann
parents:
28566
diff
changeset

498 
proof 
28566  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 

23956  504 

505 
text {* 

38812  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}). 

25247  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 

30134  536 
@{text "group \<subseteq> monoid"}; transitive edges are left out.} 
25247  537 
\label{fig:subclass} 
538 
\end{center} 

539 
\end{figure} 

30227  540 

38812  541 
For illustration, a derived definition in @{text group} using @{text 
542 
pow_nat} 

23956  543 
*} 
544 

28565  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>)" 

23956  549 

550 
text {* 

38812  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]}. 

24991  554 
*} 
23956  555 

25868  556 
subsection {* A note on syntax *} 
557 

558 
text {* 

38812  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: 

25868  562 
*} 
563 

28565  564 
context %quote semigroup 
25868  565 
begin 
566 

28565  567 
term %quote "x \<otimes> y"  {* example 1 *} 
568 
term %quote "(x\<Colon>nat) \<otimes> y"  {* example 2 *} 

25868  569 

28566  570 
end %quote 
25868  571 

28565  572 
term %quote "x \<otimes> y"  {* example 3 *} 
25868  573 

574 
text {* 

38812  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]"}. 

25868  580 
*} 
22347  581 

29705  582 
section {* Further issues *} 
583 

584 
subsection {* Type classes and code generation *} 

22317  585 

586 
text {* 

38812  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{isabellecodegen} 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: 

22317  595 
*} 
596 

28565  597 
definition %quote example :: int where 
598 
"example = pow_int 10 (2)" 

22317  599 

600 
text {* 

31691  601 
\noindent This maps to Haskell as follows: 
22317  602 
*} 
38322
5888841c38da
avoid inclusion of Natural module in generated code
haftmann
parents:
37706
diff
changeset

603 
(*<*)code_include %invisible Haskell "Natural" (*>*) 
39743  604 
text %quotetypewriter {* 
39680  605 
@{code_stmts example (Haskell)} 
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
38812
diff
changeset

606 
*} 
22317  607 

608 
text {* 

31691  609 
\noindent The code in SML has explicit dictionary passing: 
22317  610 
*} 
39743  611 
text %quotetypewriter {* 
39680  612 
@{code_stmts example (SML)} 
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
38812
diff
changeset

613 
*} 
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
38812
diff
changeset

614 

20946  615 

38812  616 
text {* 
617 
\noindent In Scala, implicts are used as dictionaries: 

618 
*} 

619 
(*<*)code_include %invisible Scala "Natural" (*>*) 

39743  620 
text %quotetypewriter {* 
39680  621 
@{code_stmts example (Scala)} 
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
38812
diff
changeset

622 
*} 
38812  623 

624 

29705  625 
subsection {* Inspecting the type class universe *} 
626 

627 
text {* 

38812  628 
To facilitate orientation in complex subclass structures, two 
629 
diagnostics commands are provided: 

29705  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 

20946  642 
end 