author  haftmann 
Sun, 07 Sep 2014 17:51:32 +0200  
changeset 58202  be1d10595b7b 
parent 56678  71a8ac5d039f 
child 58620  7435b6a3f72e 
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 {* 
56678  178 
\noindent Note the occurrence of the name @{text mult_nat} in the 
38812  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 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51143
diff
changeset

198 
mult_prod_def: "p\<^sub>1 \<otimes> p\<^sub>2 = (fst p\<^sub>1 \<otimes> fst p\<^sub>2, snd p\<^sub>1 \<otimes> snd p\<^sub>2)" 
25533  199 

28565  200 
instance %quote proof 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51143
diff
changeset

201 
fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup" 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51143
diff
changeset

202 
show "p\<^sub>1 \<otimes> p\<^sub>2 \<otimes> p\<^sub>3 = p\<^sub>1 \<otimes> (p\<^sub>2 \<otimes> p\<^sub>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 {* 
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
53015
diff
changeset

359 
\noindent The connection to the type system is done by means of a 
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
53015
diff
changeset

360 
primitive type class @{text "idem"}, together with a corresponding 
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
53015
diff
changeset

361 
interpretation: 
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
53015
diff
changeset

362 
*} 
22347  363 

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

365 
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>" 
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
53015
diff
changeset

366 
(*<*)sorry(*>*) 
28565  367 

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

20946  374 
subsection {* Abstract reasoning *} 
375 

376 
text {* 

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

25247  380 
states that the function @{text "(x \<otimes>)"} is injective: 
20946  381 
*} 
382 

28566  383 
lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z" 
384 
proof 

385 
assume "x \<otimes> y = x \<otimes> z" 

386 
then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp 

387 
then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp 

388 
then show "y = z" using neutl and invl by simp 

389 
next 

390 
assume "y = z" 

391 
then show "x \<otimes> y = x \<otimes> z" by simp 

392 
qed 

20946  393 

394 
text {* 

38812  395 
\noindent Here the \qt{@{keyword "in"} @{class group}} target 
396 
specification indicates that the result is recorded within that 

397 
context for later use. This local theorem is also lifted to the 

398 
global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> 

399 
\<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been 

400 
made an instance of @{text "group"} before, we may refer to that 

401 
fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = 

402 
z"}. 

20946  403 
*} 
404 

405 

23956  406 
subsection {* Derived definitions *} 
407 

408 
text {* 

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

409 
Isabelle locales are targets which support local definitions: 
23956  410 
*} 
411 

28566  412 
primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where 
413 
"pow_nat 0 x = \<one>" 

414 
 "pow_nat (Suc n) x = x \<otimes> pow_nat n x" 

20946  415 

416 
text {* 

23956  417 
\noindent If the locale @{text group} is also a class, this local 
38812  418 
definition is propagated onto a global definition of @{term [source] 
419 
"pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems 

23956  420 

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

20946  422 

38812  423 
\noindent As you can see from this example, for local definitions 
424 
you may use any specification tool which works together with 

425 
locales, such as Krauss's recursive function package 

31691  426 
\cite{krauss2006}. 
23956  427 
*} 
428 

429 

25247  430 
subsection {* A functor analogy *} 
431 

432 
text {* 

38812  433 
We introduced Isar classes by analogy to type classes in functional 
434 
programming; if we reconsider this in the context of what has been 

435 
said about type classes and locales, we can drive this analogy 

436 
further by stating that type classes essentially correspond to 

437 
functors that have a canonical interpretation as type classes. 

438 
There is also the possibility of other interpretations. For 

439 
example, @{text list}s also form a monoid with @{text append} and 

440 
@{term "[]"} as operations, but it seems inappropriate to apply to 

441 
lists the same operations as for genuinely algebraic types. In such 

442 
a case, we can simply make a particular interpretation of monoids 

443 
for lists: 

25247  444 
*} 
445 

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

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

447 
proof qed auto 
25247  448 

449 
text {* 

450 
\noindent This enables us to apply facts on monoids 

451 
to lists, e.g. @{thm list_monoid.neutl [no_vars]}. 

452 

453 
When using this interpretation pattern, it may also 

454 
be appropriate to map derived definitions accordingly: 

455 
*} 

456 

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

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

25247  460 

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

461 
interpretation %quote list_monoid: monoid append "[]" where 
28566  462 
"monoid.pow_nat append [] = replicate" 
463 
proof  

29513  464 
interpret monoid append "[]" .. 
28566  465 
show "monoid.pow_nat append [] = replicate" 
466 
proof 

467 
fix n 

468 
show "monoid.pow_nat append [] n = replicate n" 

469 
by (induct n) auto 

470 
qed 

471 
qed intro_locales 

25247  472 

31255  473 
text {* 
474 
\noindent This pattern is also helpful to reuse abstract 

475 
specifications on the \emph{same} type. For example, think of a 

476 
class @{text preorder}; for type @{typ nat}, there are at least two 

477 
possible instances: the natural order or the order induced by the 

478 
divides relation. But only one of these instances can be used for 

479 
@{command instantiation}; using the locale behind the class @{text 

480 
preorder}, it is still possible to utilise the same abstract 

481 
specification again using @{command interpretation}. 

482 
*} 

25247  483 

24991  484 
subsection {* Additional subclass relations *} 
22347  485 

486 
text {* 

31255  487 
Any @{text "group"} is also a @{text "monoid"}; this can be made 
488 
explicit by claiming an additional subclass relation, together with 

489 
a proof of the logical difference: 

22347  490 
*} 
491 

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

493 
proof 
28566  494 
fix x 
495 
from invl have "x\<div> \<otimes> x = \<one>" by simp 

496 
with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp 

497 
with left_cancel show "x \<otimes> \<one> = x" by simp 

498 
qed 

23956  499 

500 
text {* 

38812  501 
The logical proof is carried out on the locale level. Afterwards it 
502 
is propagated to the type system, making @{text group} an instance 

503 
of @{text monoid} by adding an additional edge to the graph of 

504 
subclass relations (\figref{fig:subclass}). 

25247  505 

506 
\begin{figure}[htbp] 

507 
\begin{center} 

508 
\small 

509 
\unitlength 0.6mm 

510 
\begin{picture}(40,60)(0,0) 

511 
\put(20,60){\makebox(0,0){@{text semigroup}}} 

512 
\put(20,40){\makebox(0,0){@{text monoidl}}} 

513 
\put(00,20){\makebox(0,0){@{text monoid}}} 

514 
\put(40,00){\makebox(0,0){@{text group}}} 

515 
\put(20,55){\vector(0,1){10}} 

516 
\put(15,35){\vector(1,1){10}} 

517 
\put(25,35){\vector(1,3){10}} 

518 
\end{picture} 

519 
\hspace{8em} 

520 
\begin{picture}(40,60)(0,0) 

521 
\put(20,60){\makebox(0,0){@{text semigroup}}} 

522 
\put(20,40){\makebox(0,0){@{text monoidl}}} 

523 
\put(00,20){\makebox(0,0){@{text monoid}}} 

524 
\put(40,00){\makebox(0,0){@{text group}}} 

525 
\put(20,55){\vector(0,1){10}} 

526 
\put(15,35){\vector(1,1){10}} 

527 
\put(05,15){\vector(3,1){30}} 

528 
\end{picture} 

529 
\caption{Subclass relationship of monoids and groups: 

530 
before and after establishing the relationship 

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

534 
\end{figure} 

30227  535 

38812  536 
For illustration, a derived definition in @{text group} using @{text 
537 
pow_nat} 

23956  538 
*} 
539 

28565  540 
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where 
541 
"pow_int k x = (if k >= 0 

542 
then pow_nat (nat k) x 

543 
else (pow_nat (nat ( k)) x)\<div>)" 

23956  544 

545 
text {* 

38812  546 
\noindent yields the global definition of @{term [source] "pow_int \<Colon> 
547 
int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm 

548 
pow_int_def [no_vars]}. 

24991  549 
*} 
23956  550 

25868  551 
subsection {* A note on syntax *} 
552 

553 
text {* 

38812  554 
As a convenience, class context syntax allows references to local 
555 
class operations and their global counterparts uniformly; type 

556 
inference resolves ambiguities. For example: 

25868  557 
*} 
558 

28565  559 
context %quote semigroup 
25868  560 
begin 
561 

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

25868  564 

28566  565 
end %quote 
25868  566 

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

569 
text {* 

38812  570 
\noindent Here in example 1, the term refers to the local class 
571 
operation @{text "mult [\<alpha>]"}, whereas in example 2 the type 

572 
constraint enforces the global class operation @{text "mult [nat]"}. 

573 
In the global context in example 3, the reference is to the 

574 
polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}. 

25868  575 
*} 
22347  576 

29705  577 
section {* Further issues *} 
578 

579 
subsection {* Type classes and code generation *} 

22317  580 

581 
text {* 

38812  582 
Turning back to the first motivation for type classes, namely 
583 
overloading, it is obvious that overloading stemming from @{command 

584 
class} statements and @{command instantiation} targets naturally 

585 
maps to Haskell type classes. The code generator framework 

586 
\cite{isabellecodegen} takes this into account. If the target 

587 
language (e.g.~SML) lacks type classes, then they are implemented by 

588 
an explicit dictionary construction. As example, let's go back to 

589 
the power function: 

22317  590 
*} 
591 

28565  592 
definition %quote example :: int where 
593 
"example = pow_int 10 (2)" 

22317  594 

595 
text {* 

31691  596 
\noindent This maps to Haskell as follows: 
22317  597 
*} 
39743  598 
text %quotetypewriter {* 
39680  599 
@{code_stmts example (Haskell)} 
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
38812
diff
changeset

600 
*} 
22317  601 

602 
text {* 

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

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

608 

20946  609 

38812  610 
text {* 
611 
\noindent In Scala, implicts are used as dictionaries: 

612 
*} 

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

615 
*} 
38812  616 

617 

29705  618 
subsection {* Inspecting the type class universe *} 
619 

620 
text {* 

38812  621 
To facilitate orientation in complex subclass structures, two 
622 
diagnostics commands are provided: 

29705  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 

58202  630 
between all classes as a Hasse diagram. An optional first sort argument 
631 
constrains the set of classes to all subclasses of this sort, 

632 
an optional second sort argument to all superclasses of this sort. 

29705  633 

634 
\end{description} 

635 
*} 

636 

20946  637 
end 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48985
diff
changeset

638 