5 chapter {* Haskell-style classes with Isabelle/Isar *}
7 section {* Introduction *}
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:
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"}
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"}
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"}
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"}
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.
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}.
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:
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"}
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:
76 \item specifying abstract parameters together with
77 corresponding specifications,
78 \item instantiating those abstract parameters by a particular
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}).
85 \noindent Isar type classes also directly support code generation
86 in a Haskell like fashion.
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.
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.
99 section {* A simple algebra example \label{sec:example} *}
101 subsection {* Class definition *}
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:
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)"
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,
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)"}.
126 subsection {* Class instantiation \label{sec:class_inst} *}
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:
135 instantiation %quote int :: semigroup
139 mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
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 .
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.
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.
165 \medskip Another instance of @{class semigroup} are the natural numbers:
168 instantiation %quote nat :: semigroup
171 primrec %quote mult_nat where
172 "(0\<Colon>nat) \<otimes> n = n"
173 | "Suc m \<otimes> n = Suc (m \<otimes> n)"
175 instance %quote proof
177 show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
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.
192 subsection {* Lifting and parametric types *}
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:
201 instantiation %quote * :: (semigroup, semigroup) semigroup
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)"
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)
216 \noindent Associativity from product semigroups is
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
227 subsection {* Subclassing *}
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
236 class %quote monoidl = semigroup +
237 fixes neutral :: "\<alpha>" ("\<one>")
238 assumes neutl: "\<one> \<otimes> x = x"
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:
247 instantiation %quote nat and int :: monoidl
251 neutral_nat_def: "\<one> = (0\<Colon>nat)"
254 neutral_int_def: "\<one> = (0\<Colon>int)"
256 instance %quote proof
258 show "\<one> \<otimes> n = n"
259 unfolding neutral_nat_def by simp
262 show "\<one> \<otimes> k = k"
263 unfolding neutral_int_def mult_int_def by simp
268 instantiation %quote * :: (monoidl, monoidl) monoidl
272 neutral_prod_def: "\<one> = (\<one>, \<one>)"
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)
283 \noindent Fully-fledged monoids are modelled by another subclass
284 which does not add new parameters but tightens the specification:
287 class %quote monoid = monoidl +
288 assumes neutr: "x \<otimes> \<one> = x"
290 instantiation %quote nat and int :: monoid
293 instance %quote proof
295 show "n \<otimes> \<one> = n"
296 unfolding neutral_nat_def by (induct n) simp_all
299 show "k \<otimes> \<one> = k"
300 unfolding neutral_int_def mult_int_def by simp
305 instantiation %quote * :: (monoid, monoid) monoid
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)
317 \noindent To finish our small algebra example, we add a @{text group} class
318 with a corresponding instance:
321 class %quote group = monoidl +
322 fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
323 assumes invl: "x\<div> \<otimes> x = \<one>"
325 instantiation %quote int :: group
329 inverse_int_def: "i\<div> = - (i\<Colon>int)"
331 instance %quote proof
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 .
341 section {* Type classes as locales *}
343 subsection {* A look behind the scene *}
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:
353 fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
354 assumes idem: "f (f x) = f x"
357 \noindent essentially introduces the locale
358 *} setup %invisible {* Sign.add_path "foo" *}
361 fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
362 assumes idem: "f (f x) = f x"
364 text {* \noindent together with corresponding constant(s): *}
366 consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
369 \noindent The connection to the type system is done by means
370 of a primitive axclass
371 *} setup %invisible {* Sign.add_path "foo" *}
373 axclass %quote idem < type
374 idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
376 text {* \noindent together with a corresponding interpretation: *}
378 interpretation %quote idem_class:
379 idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
380 proof qed (rule idem)
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 *}
388 subsection {* Abstract reasoning *}
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:
397 lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
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
405 then show "x \<otimes> y = x \<otimes> z" by simp
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"}.
419 subsection {* Derived definitions *}
422 Isabelle locales support a concept of local definitions
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"
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
436 @{thm pow_nat.simps [no_vars]}.
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}).
444 subsection {* A functor analogy *}
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:
462 interpretation %quote list_monoid!: monoid append "[]"
466 \noindent This enables us to apply facts on monoids
467 to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
469 When using this interpretation pattern, it may also
470 be appropriate to map derived definitions accordingly:
473 primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
475 | "replicate (Suc n) xs = xs @ replicate n xs"
477 interpretation %quote list_monoid!: monoid append "[]" where
478 "monoid.pow_nat append [] = replicate"
480 interpret monoid append "[]" ..
481 show "monoid.pow_nat append [] = replicate"
484 show "monoid.pow_nat append [] n = replicate n"
490 subsection {* Additional subclass relations *}
493 Any @{text "group"} is also a @{text "monoid"}; this
494 can be made explicit by claiming an additional
496 together with a proof of the logical difference:
499 subclass %quote (in group) monoid
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
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}).
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}}
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}}
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.}
545 For illustration, a derived definition
546 in @{text group} which uses @{text pow_nat}:
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>)"
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]}.
560 subsection {* A note on syntax *}
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:
568 context %quote semigroup
571 term %quote "x \<otimes> y" -- {* example 1 *}
572 term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
576 term %quote "x \<otimes> y" -- {* example 3 *}
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]"}.
586 section {* Further issues *}
588 subsection {* Type classes and code generation *}
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:
603 definition %quote example :: int where
604 "example = pow_int 10 (-2)"
607 \noindent This maps to Haskell as:
610 text %quote {*@{code_stmts example (Haskell)}*}
613 \noindent The whole code in SML with explicit dictionary passing:
616 text %quote {*@{code_stmts example (SML)}*}
618 subsection {* Inspecting the type class universe *}
621 To facilitate orientation in complex subclass structures,
622 two diagnostics commands are provided:
626 \item[@{command "print_classes"}] print a list of all classes
627 together with associated operations etc.
629 \item[@{command "class_deps"}] visualizes the subclass relation
630 between all classes as a Hasse diagram.