haftmann@20946: theory Classes haftmann@28565: imports Main Setup haftmann@20946: begin haftmann@20946: haftmann@20946: section {* Introduction *} haftmann@20946: haftmann@20946: text {* paulson@31684: Type classes were introduced by Wadler and Blott \cite{wadler89how} paulson@31684: into the Haskell language to allow for a reasonable implementation haftmann@22317: of overloading\footnote{throughout this tutorial, we are referring haftmann@22317: to classical Haskell 1.0 type classes, not considering haftmann@22317: later additions in expressiveness}. haftmann@22317: As a canonical example, a polymorphic equality function haftmann@22317: @{text "eq \ \ \ \ \ bool"} which is overloaded on different haftmann@22550: types for @{text "\"}, which is achieved by splitting introduction haftmann@22317: of the @{text eq} function from its overloaded definitions by means haftmann@22317: of @{text class} and @{text instance} declarations: haftmann@30210: \footnote{syntax here is a kind of isabellized Haskell} haftmann@20946: haftmann@28565: \begin{quote} haftmann@20946: haftmann@30210: \noindent@{text "class eq where"} \\ haftmann@28565: \hspace*{2ex}@{text "eq \ \ \ \ \ bool"} haftmann@20946: haftmann@28565: \medskip\noindent@{text "instance nat \ eq where"} \\ haftmann@28565: \hspace*{2ex}@{text "eq 0 0 = True"} \\ haftmann@28565: \hspace*{2ex}@{text "eq 0 _ = False"} \\ haftmann@28565: \hspace*{2ex}@{text "eq _ 0 = False"} \\ haftmann@28565: \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"} haftmann@22317: haftmann@28948: \medskip\noindent@{text "instance (\\eq, \\eq) pair \ eq where"} \\ haftmann@28565: \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \ eq y1 y2"} haftmann@22317: haftmann@28565: \medskip\noindent@{text "class ord extends eq where"} \\ haftmann@28565: \hspace*{2ex}@{text "less_eq \ \ \ \ \ bool"} \\ haftmann@28565: \hspace*{2ex}@{text "less \ \ \ \ \ bool"} haftmann@28565: haftmann@28565: \end{quote} haftmann@28565: haftmann@28565: \noindent Type variables are annotated with (finitely many) classes; haftmann@22317: these annotations are assertions that a particular polymorphic type haftmann@22317: provides definitions for overloaded functions. haftmann@22317: haftmann@22317: Indeed, type classes not only allow for simple overloading haftmann@22317: but form a generic calculus, an instance of order-sorted paulson@31684: algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}. haftmann@22317: paulson@31684: From a software engineering point of view, type classes haftmann@28540: roughly correspond to interfaces in object-oriented languages like Java; haftmann@22317: so, it is naturally desirable that type classes do not only haftmann@24991: provide functions (class parameters) but also state specifications haftmann@22317: implementations must obey. For example, the @{text "class eq"} haftmann@22550: above could be given the following specification, demanding that haftmann@22550: @{text "class eq"} is an equivalence relation obeying reflexivity, haftmann@22550: symmetry and transitivity: haftmann@22317: haftmann@28565: \begin{quote} haftmann@22317: haftmann@28565: \noindent@{text "class eq where"} \\ haftmann@28565: \hspace*{2ex}@{text "eq \ \ \ \ \ bool"} \\ haftmann@28565: @{text "satisfying"} \\ haftmann@28565: \hspace*{2ex}@{text "refl: eq x x"} \\ haftmann@28565: \hspace*{2ex}@{text "sym: eq x y \ eq x y"} \\ haftmann@28565: \hspace*{2ex}@{text "trans: eq x y \ eq y z \ eq x z"} haftmann@28565: haftmann@28565: \end{quote} haftmann@28565: paulson@31684: \noindent From a theoretical point of view, type classes are lightweight haftmann@22347: modules; Haskell type classes may be emulated by haftmann@22317: SML functors \cite{classes_modules}. haftmann@22317: Isabelle/Isar offers a discipline of type classes which brings haftmann@22317: all those aspects together: haftmann@22317: haftmann@22317: \begin{enumerate} haftmann@24991: \item specifying abstract parameters together with haftmann@22317: corresponding specifications, haftmann@28540: \item instantiating those abstract parameters by a particular haftmann@22317: type haftmann@22317: \item in connection with a ``less ad-hoc'' approach to overloading, paulson@31684: \item with a direct link to the Isabelle module system: paulson@31684: locales \cite{kammueller-locales}. haftmann@22317: \end{enumerate} haftmann@22317: haftmann@22550: \noindent Isar type classes also directly support code generation paulson@31684: in a Haskell like fashion. Internally, they are mapped to more primitive paulson@31684: Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}. haftmann@22317: haftmann@22317: This tutorial demonstrates common elements of structured specifications haftmann@22317: and abstract reasoning with type classes by the algebraic hierarchy of haftmann@20946: semigroups, monoids and groups. Our background theory is that of haftmann@23956: Isabelle/HOL \cite{isa-tutorial}, for which some haftmann@22317: familiarity is assumed. haftmann@20946: *} haftmann@20946: haftmann@22317: section {* A simple algebra example \label{sec:example} *} haftmann@20946: haftmann@20946: subsection {* Class definition *} haftmann@20946: haftmann@20946: text {* haftmann@20946: Depending on an arbitrary type @{text "\"}, class @{text haftmann@28565: "semigroup"} introduces a binary operator @{text "(\)"} that is haftmann@20946: assumed to be associative: haftmann@20946: *} haftmann@20946: haftmann@29705: class %quote semigroup = haftmann@28565: fixes mult :: "\ \ \ \ \" (infixl "\" 70) haftmann@28565: assumes assoc: "(x \ y) \ z = x \ (y \ z)" haftmann@20946: haftmann@20946: text {* haftmann@28565: \noindent This @{command class} specification consists of two haftmann@28565: parts: the \qn{operational} part names the class parameter haftmann@28565: (@{element "fixes"}), the \qn{logical} part specifies properties on them haftmann@28565: (@{element "assumes"}). The local @{element "fixes"} and haftmann@28565: @{element "assumes"} are lifted to the theory toplevel, haftmann@28565: yielding the global haftmann@24991: parameter @{term [source] "mult \ \\semigroup \ \ \ \"} and the haftmann@28565: global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\x y haftmann@22479: z \ \\semigroup. (x \ y) \ z = x \ (y \ z)"}. haftmann@20946: *} haftmann@20946: haftmann@20946: haftmann@20946: subsection {* Class instantiation \label{sec:class_inst} *} haftmann@20946: haftmann@20946: text {* haftmann@28565: The concrete type @{typ int} is made a @{class semigroup} haftmann@24991: instance by providing a suitable definition for the class parameter haftmann@28565: @{text "(\)"} and a proof for the specification of @{fact assoc}. haftmann@28565: This is accomplished by the @{command instantiation} target: haftmann@20946: *} haftmann@20946: haftmann@28565: instantiation %quote int :: semigroup haftmann@28565: begin haftmann@25533: haftmann@28565: definition %quote haftmann@28565: mult_int_def: "i \ j = i + (j\int)" haftmann@25533: haftmann@28565: instance %quote proof haftmann@28565: fix i j k :: int have "(i + j) + k = i + (j + k)" by simp haftmann@28565: then show "(i \ j) \ k = i \ (j \ k)" haftmann@28566: unfolding mult_int_def . haftmann@28565: qed haftmann@20946: haftmann@28565: end %quote haftmann@25533: haftmann@20946: text {* paulson@31684: \noindent @{command instantiation} defines class parameters haftmann@25533: at a particular instance using common specification tools (here, haftmann@28565: @{command definition}). The concluding @{command instance} haftmann@25533: opens a proof that the given parameters actually conform haftmann@25533: to the class specification. Note that the first proof step haftmann@28565: is the @{method default} method, haftmann@28565: which for such instance proofs maps to the @{method intro_classes} method. paulson@31684: This reduces an instance judgement to the relevant primitive paulson@31684: proof goals; typically it is the first method applied haftmann@22317: in an instantiation proof. haftmann@22317: haftmann@28565: From now on, the type-checker will consider @{typ int} haftmann@28565: as a @{class semigroup} automatically, i.e.\ any general results haftmann@25533: are immediately available on concrete instances. haftmann@28565: paulson@31684: \medskip Another instance of @{class semigroup} yields the natural numbers: haftmann@20946: *} haftmann@20946: haftmann@28565: instantiation %quote nat :: semigroup haftmann@28565: begin haftmann@25533: haftmann@28565: primrec %quote mult_nat where haftmann@28565: "(0\nat) \ n = n" haftmann@28565: | "Suc m \ n = Suc (m \ n)" haftmann@25533: haftmann@28565: instance %quote proof haftmann@28565: fix m n q :: nat haftmann@28565: show "m \ n \ q = m \ (n \ q)" haftmann@28565: by (induct m) auto haftmann@28565: qed haftmann@20946: haftmann@28565: end %quote haftmann@25247: haftmann@25871: text {* haftmann@25871: \noindent Note the occurence of the name @{text mult_nat} haftmann@25871: in the primrec declaration; by default, the local name of haftmann@31675: a class operation @{text f} to be instantiated on type constructor haftmann@31675: @{text \} is mangled as @{text f_\}. In case of uncertainty, haftmann@28565: these names may be inspected using the @{command "print_context"} command haftmann@25871: or the corresponding ProofGeneral button. haftmann@25871: *} haftmann@25871: haftmann@25247: subsection {* Lifting and parametric types *} haftmann@25247: haftmann@20946: text {* paulson@31684: Overloaded definitions given at a class instantiation haftmann@25247: may include recursion over the syntactic structure of types. haftmann@25247: As a canonical example, we model product semigroups haftmann@25247: using our simple algebra: haftmann@20946: *} haftmann@20946: haftmann@28565: instantiation %quote * :: (semigroup, semigroup) semigroup haftmann@28565: begin haftmann@25533: haftmann@28565: definition %quote haftmann@31930: mult_prod_def: "p\<^isub>1 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" haftmann@25533: haftmann@28565: instance %quote proof haftmann@31930: fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" haftmann@31930: show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ p\<^isub>3)" haftmann@28566: unfolding mult_prod_def by (simp add: assoc) haftmann@28565: qed haftmann@20946: haftmann@28565: end %quote haftmann@25533: haftmann@25247: text {* haftmann@31675: \noindent Associativity of product semigroups is established using haftmann@28565: the definition of @{text "(\)"} on products and the hypothetical huffman@27505: associativity of the type components; these hypotheses paulson@31684: are legitimate due to the @{class semigroup} constraints imposed haftmann@28565: on the type components by the @{command instance} proposition. haftmann@25247: Indeed, this pattern often occurs with parametric types haftmann@25247: and type classes. haftmann@25247: *} haftmann@20946: haftmann@25247: haftmann@25247: subsection {* Subclassing *} haftmann@20946: haftmann@20946: text {* haftmann@28565: We define a subclass @{text monoidl} (a semigroup with a left-hand neutral) haftmann@28565: by extending @{class semigroup} haftmann@28565: with one additional parameter @{text neutral} together paulson@31684: with its characteristic property: haftmann@20946: *} haftmann@20946: haftmann@28565: class %quote monoidl = semigroup + haftmann@28565: fixes neutral :: "\" ("\") haftmann@28565: assumes neutl: "\ \ x = x" haftmann@20946: haftmann@20946: text {* haftmann@25247: \noindent Again, we prove some instances, by haftmann@24991: providing suitable parameter definitions and proofs for the huffman@27505: additional specifications. Observe that instantiations haftmann@25533: for types with the same arity may be simultaneous: haftmann@20946: *} haftmann@20946: haftmann@28566: instantiation %quote nat and int :: monoidl haftmann@28566: begin haftmann@25533: haftmann@28566: definition %quote haftmann@28566: neutral_nat_def: "\ = (0\nat)" haftmann@25533: haftmann@28566: definition %quote haftmann@28566: neutral_int_def: "\ = (0\int)" haftmann@25533: haftmann@28566: instance %quote proof haftmann@28566: fix n :: nat haftmann@28566: show "\ \ n = n" haftmann@28566: unfolding neutral_nat_def by simp haftmann@28566: next haftmann@28566: fix k :: int haftmann@28566: show "\ \ k = k" haftmann@28566: unfolding neutral_int_def mult_int_def by simp haftmann@28566: qed haftmann@20946: haftmann@28566: end %quote haftmann@25533: haftmann@28566: instantiation %quote * :: (monoidl, monoidl) monoidl haftmann@28566: begin haftmann@25533: haftmann@28566: definition %quote haftmann@28566: neutral_prod_def: "\ = (\, \)" haftmann@25533: haftmann@28566: instance %quote proof haftmann@28566: fix p :: "\\monoidl \ \\monoidl" haftmann@28566: show "\ \ p = p" haftmann@28566: unfolding neutral_prod_def mult_prod_def by (simp add: neutl) haftmann@28566: qed haftmann@20946: haftmann@28566: end %quote haftmann@25533: haftmann@20946: text {* paulson@31684: \noindent Fully-fledged monoids are modelled by another subclass, haftmann@24991: which does not add new parameters but tightens the specification: haftmann@20946: *} haftmann@20946: haftmann@28566: class %quote monoid = monoidl + haftmann@28566: assumes neutr: "x \ \ = x" haftmann@20946: haftmann@28566: instantiation %quote nat and int :: monoid haftmann@28566: begin haftmann@25533: haftmann@28566: instance %quote proof haftmann@28566: fix n :: nat haftmann@28566: show "n \ \ = n" haftmann@28566: unfolding neutral_nat_def by (induct n) simp_all haftmann@28566: next haftmann@28566: fix k :: int haftmann@28566: show "k \ \ = k" haftmann@28566: unfolding neutral_int_def mult_int_def by simp haftmann@28566: qed haftmann@25247: haftmann@28566: end %quote haftmann@25533: haftmann@28566: instantiation %quote * :: (monoid, monoid) monoid haftmann@28566: begin haftmann@25533: haftmann@28566: instance %quote proof haftmann@28566: fix p :: "\\monoid \ \\monoid" haftmann@28566: show "p \ \ = p" haftmann@28566: unfolding neutral_prod_def mult_prod_def by (simp add: neutr) haftmann@28566: qed haftmann@22317: haftmann@28566: end %quote haftmann@25533: haftmann@22317: text {* haftmann@28565: \noindent To finish our small algebra example, we add a @{text group} class haftmann@22317: with a corresponding instance: haftmann@22317: *} haftmann@20946: haftmann@28566: class %quote group = monoidl + haftmann@28566: fixes inverse :: "\ \ \" ("(_\
)" [1000] 999) haftmann@28566: assumes invl: "x\
\ x = \" haftmann@20946: haftmann@28566: instantiation %quote int :: group haftmann@28566: begin haftmann@25533: haftmann@28566: definition %quote haftmann@28566: inverse_int_def: "i\
= - (i\int)" haftmann@25533: haftmann@28566: instance %quote proof haftmann@28566: fix i :: int haftmann@28566: have "-i + i = 0" by simp haftmann@28566: then show "i\
\ i = \" haftmann@28566: unfolding mult_int_def neutral_int_def inverse_int_def . haftmann@28566: qed haftmann@20946: haftmann@28566: end %quote haftmann@28566: haftmann@25533: haftmann@22317: section {* Type classes as locales *} haftmann@22317: paulson@31684: subsection {* A look behind the scenes *} haftmann@22317: haftmann@22347: text {* haftmann@22347: The example above gives an impression how Isar type classes work haftmann@22347: in practice. As stated in the introduction, classes also provide haftmann@22347: a link to Isar's locale system. Indeed, the logical core of a class paulson@31684: is nothing other than a locale: haftmann@22347: *} haftmann@22347: haftmann@29705: class %quote idem = haftmann@22347: fixes f :: "\ \ \" haftmann@22347: assumes idem: "f (f x) = f x" haftmann@22317: haftmann@22317: text {* haftmann@22347: \noindent essentially introduces the locale haftmann@30210: *} (*<*)setup %invisible {* Sign.add_path "foo" *} haftmann@30210: (*>*) haftmann@28566: locale %quote idem = haftmann@22347: fixes f :: "\ \ \" haftmann@22347: assumes idem: "f (f x) = f x" haftmann@22347: haftmann@22550: text {* \noindent together with corresponding constant(s): *} haftmann@22347: haftmann@28566: consts %quote f :: "\ \ \" haftmann@22347: haftmann@22550: text {* haftmann@22550: \noindent The connection to the type system is done by means haftmann@35282: of a primitive type class haftmann@30210: *} (*<*)setup %invisible {* Sign.add_path "foo" *} haftmann@30210: (*>*) haftmann@35282: classes %quote idem < type haftmann@35282: (*<*)axiomatization where idem: "f (f (x::\\idem)) = f x" haftmann@35282: setup %invisible {* Sign.parent_path *}(*>*) haftmann@22347: haftmann@22550: text {* \noindent together with a corresponding interpretation: *} haftmann@22347: haftmann@29513: interpretation %quote idem_class: wenzelm@29294: idem "f \ (\\idem) \ \" haftmann@35282: (*<*)proof qed (rule idem)(*>*) haftmann@28565: haftmann@22347: text {* paulson@31684: \noindent This gives you the full power of the Isabelle module system; haftmann@22347: conclusions in locale @{text idem} are implicitly propagated haftmann@22479: to class @{text idem}. haftmann@30210: *} (*<*)setup %invisible {* Sign.parent_path *} haftmann@30210: (*>*) haftmann@20946: subsection {* Abstract reasoning *} haftmann@20946: haftmann@20946: text {* haftmann@22347: Isabelle locales enable reasoning at a general level, while results haftmann@20946: are implicitly transferred to all instances. For example, we can haftmann@20946: now establish the @{text "left_cancel"} lemma for groups, which haftmann@25247: states that the function @{text "(x \)"} is injective: haftmann@20946: *} haftmann@20946: haftmann@28566: lemma %quote (in group) left_cancel: "x \ y = x \ z \ y = z" haftmann@28566: proof haftmann@28566: assume "x \ y = x \ z" haftmann@28566: then have "x\
\ (x \ y) = x\
\ (x \ z)" by simp haftmann@28566: then have "(x\
\ x) \ y = (x\
\ x) \ z" using assoc by simp haftmann@28566: then show "y = z" using neutl and invl by simp haftmann@28566: next haftmann@28566: assume "y = z" haftmann@28566: then show "x \ y = x \ z" by simp haftmann@28566: qed haftmann@20946: haftmann@20946: text {* haftmann@28565: \noindent Here the \qt{@{keyword "in"} @{class group}} target specification haftmann@20946: indicates that the result is recorded within that context for later haftmann@28565: use. This local theorem is also lifted to the global one @{fact haftmann@22479: "group.left_cancel:"} @{prop [source] "\x y z \ \\group. x \ y = x \ haftmann@20946: z \ y = z"}. Since type @{text "int"} has been made an instance of haftmann@20946: @{text "group"} before, we may refer to that fact as well: @{prop haftmann@22479: [source] "\x y z \ int. x \ y = x \ z \ y = z"}. haftmann@20946: *} haftmann@20946: haftmann@20946: haftmann@23956: subsection {* Derived definitions *} haftmann@20946: haftmann@20946: text {* haftmann@35282: Isabelle locales are targets which support local definitions: haftmann@23956: *} haftmann@20946: haftmann@28566: primrec %quote (in monoid) pow_nat :: "nat \ \ \ \" where haftmann@28566: "pow_nat 0 x = \" haftmann@28566: | "pow_nat (Suc n) x = x \ pow_nat n x" haftmann@23956: haftmann@23956: text {* haftmann@23956: \noindent If the locale @{text group} is also a class, this local haftmann@23956: definition is propagated onto a global definition of haftmann@23956: @{term [source] "pow_nat \ nat \ \\monoid \ \\monoid"} haftmann@23956: with corresponding theorems haftmann@23956: haftmann@23956: @{thm pow_nat.simps [no_vars]}. haftmann@23956: haftmann@23956: \noindent As you can see from this example, for local haftmann@23956: definitions you may use any specification tool paulson@31684: which works together with locales, such as Krauss's recursive function package paulson@31684: \cite{krauss2006}. haftmann@23956: *} haftmann@23956: haftmann@23956: haftmann@25247: subsection {* A functor analogy *} haftmann@25247: haftmann@25247: text {* paulson@31684: We introduced Isar classes by analogy to type classes in haftmann@25247: functional programming; if we reconsider this in the haftmann@25247: context of what has been said about type classes and locales, haftmann@25247: we can drive this analogy further by stating that type paulson@31684: classes essentially correspond to functors that have haftmann@25247: a canonical interpretation as type classes. paulson@31684: There is also the possibility of other interpretations. paulson@31684: For example, @{text list}s also form a monoid with haftmann@28565: @{text append} and @{term "[]"} as operations, but it haftmann@25247: seems inappropriate to apply to lists huffman@27505: the same operations as for genuinely algebraic types. paulson@31684: In such a case, we can simply make a particular interpretation haftmann@25247: of monoids for lists: haftmann@25247: *} haftmann@25247: wenzelm@30732: interpretation %quote list_monoid: monoid append "[]" haftmann@28947: proof qed auto haftmann@25247: haftmann@25247: text {* haftmann@25247: \noindent This enables us to apply facts on monoids haftmann@25247: to lists, e.g. @{thm list_monoid.neutl [no_vars]}. haftmann@25247: haftmann@25247: When using this interpretation pattern, it may also haftmann@25247: be appropriate to map derived definitions accordingly: haftmann@25247: *} haftmann@25247: haftmann@28566: primrec %quote replicate :: "nat \ \ list \ \ list" where haftmann@28566: "replicate 0 _ = []" haftmann@28566: | "replicate (Suc n) xs = xs @ replicate n xs" haftmann@25247: wenzelm@30732: interpretation %quote list_monoid: monoid append "[]" where haftmann@28566: "monoid.pow_nat append [] = replicate" haftmann@28566: proof - haftmann@29513: interpret monoid append "[]" .. haftmann@28566: show "monoid.pow_nat append [] = replicate" haftmann@28566: proof haftmann@28566: fix n haftmann@28566: show "monoid.pow_nat append [] n = replicate n" haftmann@28566: by (induct n) auto haftmann@28566: qed haftmann@28566: qed intro_locales haftmann@25247: haftmann@31249: text {* haftmann@31249: \noindent This pattern is also helpful to reuse abstract haftmann@31249: specifications on the \emph{same} type. For example, think of a haftmann@31249: class @{text preorder}; for type @{typ nat}, there are at least two haftmann@31249: possible instances: the natural order or the order induced by the haftmann@31249: divides relation. But only one of these instances can be used for haftmann@31249: @{command instantiation}; using the locale behind the class @{text haftmann@31249: preorder}, it is still possible to utilise the same abstract haftmann@31249: specification again using @{command interpretation}. haftmann@31249: *} haftmann@25247: haftmann@24991: subsection {* Additional subclass relations *} haftmann@22347: haftmann@22347: text {* haftmann@31249: Any @{text "group"} is also a @{text "monoid"}; this can be made haftmann@31249: explicit by claiming an additional subclass relation, together with haftmann@31249: a proof of the logical difference: haftmann@22347: *} haftmann@22347: haftmann@28566: subclass %quote (in group) monoid haftmann@28947: proof haftmann@28566: fix x haftmann@28566: from invl have "x\
\ x = \" by simp haftmann@28566: with assoc [symmetric] neutl invl have "x\
\ (x \ \) = x\
\ x" by simp haftmann@28566: with left_cancel show "x \ \ = x" by simp haftmann@28566: qed haftmann@23956: haftmann@23956: text {* haftmann@30210: The logical proof is carried out on the locale level. haftmann@28947: Afterwards it is propagated haftmann@23956: to the type system, making @{text group} an instance of haftmann@25247: @{text monoid} by adding an additional edge haftmann@25247: to the graph of subclass relations paulson@31684: (\figref{fig:subclass}). haftmann@25247: haftmann@25247: \begin{figure}[htbp] haftmann@25247: \begin{center} haftmann@25247: \small haftmann@25247: \unitlength 0.6mm haftmann@25247: \begin{picture}(40,60)(0,0) haftmann@25247: \put(20,60){\makebox(0,0){@{text semigroup}}} haftmann@25247: \put(20,40){\makebox(0,0){@{text monoidl}}} haftmann@25247: \put(00,20){\makebox(0,0){@{text monoid}}} haftmann@25247: \put(40,00){\makebox(0,0){@{text group}}} haftmann@25247: \put(20,55){\vector(0,-1){10}} haftmann@25247: \put(15,35){\vector(-1,-1){10}} haftmann@25247: \put(25,35){\vector(1,-3){10}} haftmann@25247: \end{picture} haftmann@25247: \hspace{8em} haftmann@25247: \begin{picture}(40,60)(0,0) haftmann@25247: \put(20,60){\makebox(0,0){@{text semigroup}}} haftmann@25247: \put(20,40){\makebox(0,0){@{text monoidl}}} haftmann@25247: \put(00,20){\makebox(0,0){@{text monoid}}} haftmann@25247: \put(40,00){\makebox(0,0){@{text group}}} haftmann@25247: \put(20,55){\vector(0,-1){10}} haftmann@25247: \put(15,35){\vector(-1,-1){10}} haftmann@25247: \put(05,15){\vector(3,-1){30}} haftmann@25247: \end{picture} haftmann@25247: \caption{Subclass relationship of monoids and groups: haftmann@25247: before and after establishing the relationship haftmann@30134: @{text "group \ monoid"}; transitive edges are left out.} haftmann@25247: \label{fig:subclass} haftmann@25247: \end{center} haftmann@25247: \end{figure} haftmann@30210: haftmann@25247: For illustration, a derived definition paulson@31684: in @{text group} using @{text pow_nat} haftmann@23956: *} haftmann@23956: haftmann@28565: definition %quote (in group) pow_int :: "int \ \ \ \" where haftmann@28565: "pow_int k x = (if k >= 0 haftmann@28565: then pow_nat (nat k) x haftmann@28565: else (pow_nat (nat (- k)) x)\
)" haftmann@23956: haftmann@23956: text {* haftmann@25247: \noindent yields the global definition of haftmann@23956: @{term [source] "pow_int \ int \ \\group \ \\group"} haftmann@23956: with the corresponding theorem @{thm pow_int_def [no_vars]}. haftmann@24991: *} haftmann@23956: haftmann@25868: subsection {* A note on syntax *} haftmann@25868: haftmann@25868: text {* paulson@31684: As a convenience, class context syntax allows references huffman@27505: to local class operations and their global counterparts haftmann@25868: uniformly; type inference resolves ambiguities. For example: haftmann@25868: *} haftmann@25868: haftmann@28565: context %quote semigroup haftmann@25868: begin haftmann@25868: haftmann@28565: term %quote "x \ y" -- {* example 1 *} haftmann@28565: term %quote "(x\nat) \ y" -- {* example 2 *} haftmann@25868: haftmann@28566: end %quote haftmann@25868: haftmann@28565: term %quote "x \ y" -- {* example 3 *} haftmann@25868: haftmann@25868: text {* haftmann@25868: \noindent Here in example 1, the term refers to the local class operation haftmann@25868: @{text "mult [\]"}, whereas in example 2 the type constraint haftmann@25868: enforces the global class operation @{text "mult [nat]"}. haftmann@25868: In the global context in example 3, the reference is haftmann@25868: to the polymorphic global class operation @{text "mult [?\ \ semigroup]"}. haftmann@25868: *} haftmann@22347: haftmann@29705: section {* Further issues *} haftmann@29705: haftmann@29705: subsection {* Type classes and code generation *} haftmann@22317: haftmann@22317: text {* haftmann@22317: Turning back to the first motivation for type classes, haftmann@22317: namely overloading, it is obvious that overloading haftmann@28565: stemming from @{command class} statements and haftmann@28565: @{command instantiation} haftmann@25533: targets naturally maps to Haskell type classes. haftmann@22317: The code generator framework \cite{isabelle-codegen} paulson@31684: takes this into account. If the target language (e.g.~SML) paulson@31684: lacks type classes, then they paulson@31684: are implemented by an explicit dictionary construction. haftmann@28540: As example, let's go back to the power function: haftmann@22317: *} haftmann@22317: haftmann@28565: definition %quote example :: int where haftmann@28565: "example = pow_int 10 (-2)" haftmann@22317: haftmann@22317: text {* paulson@31684: \noindent This maps to Haskell as follows: haftmann@22317: *} haftmann@22317: haftmann@28565: text %quote {*@{code_stmts example (Haskell)}*} haftmann@22317: haftmann@22317: text {* paulson@31684: \noindent The code in SML has explicit dictionary passing: haftmann@22317: *} haftmann@22317: haftmann@28565: text %quote {*@{code_stmts example (SML)}*} haftmann@20946: haftmann@29705: subsection {* Inspecting the type class universe *} haftmann@29705: haftmann@29705: text {* haftmann@29705: To facilitate orientation in complex subclass structures, haftmann@29705: two diagnostics commands are provided: haftmann@29705: haftmann@29705: \begin{description} haftmann@29705: haftmann@29705: \item[@{command "print_classes"}] print a list of all classes haftmann@29705: together with associated operations etc. haftmann@29705: haftmann@29705: \item[@{command "class_deps"}] visualizes the subclass relation haftmann@29705: between all classes as a Hasse diagram. haftmann@29705: haftmann@29705: \end{description} haftmann@29705: *} haftmann@29705: haftmann@20946: end