1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Classes/Thy/Classes.thy Tue Mar 03 11:00:51 2009 +0100
1.3 @@ -0,0 +1,635 @@
1.4 +theory Classes
1.5 +imports Main Setup
1.6 +begin
1.7 +
1.8 +chapter {* Haskell-style classes with Isabelle/Isar *}
1.9 +
1.10 +section {* Introduction *}
1.11 +
1.12 +text {*
1.13 + Type classes were introduces by Wadler and Blott \cite{wadler89how}
1.14 + into the Haskell language, to allow for a reasonable implementation
1.15 + of overloading\footnote{throughout this tutorial, we are referring
1.16 + to classical Haskell 1.0 type classes, not considering
1.17 + later additions in expressiveness}.
1.18 + As a canonical example, a polymorphic equality function
1.19 + @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
1.20 + types for @{text "\<alpha>"}, which is achieved by splitting introduction
1.21 + of the @{text eq} function from its overloaded definitions by means
1.22 + of @{text class} and @{text instance} declarations:
1.23 +
1.24 + \begin{quote}
1.25 +
1.26 + \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
1.27 + \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
1.28 +
1.29 + \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
1.30 + \hspace*{2ex}@{text "eq 0 0 = True"} \\
1.31 + \hspace*{2ex}@{text "eq 0 _ = False"} \\
1.32 + \hspace*{2ex}@{text "eq _ 0 = False"} \\
1.33 + \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
1.34 +
1.35 + \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
1.36 + \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
1.37 +
1.38 + \medskip\noindent@{text "class ord extends eq where"} \\
1.39 + \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
1.40 + \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
1.41 +
1.42 + \end{quote}
1.43 +
1.44 + \noindent Type variables are annotated with (finitely many) classes;
1.45 + these annotations are assertions that a particular polymorphic type
1.46 + provides definitions for overloaded functions.
1.47 +
1.48 + Indeed, type classes not only allow for simple overloading
1.49 + but form a generic calculus, an instance of order-sorted
1.50 + algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
1.51 +
1.52 + From a software engeneering point of view, type classes
1.53 + roughly correspond to interfaces in object-oriented languages like Java;
1.54 + so, it is naturally desirable that type classes do not only
1.55 + provide functions (class parameters) but also state specifications
1.56 + implementations must obey. For example, the @{text "class eq"}
1.57 + above could be given the following specification, demanding that
1.58 + @{text "class eq"} is an equivalence relation obeying reflexivity,
1.59 + symmetry and transitivity:
1.60 +
1.61 + \begin{quote}
1.62 +
1.63 + \noindent@{text "class eq where"} \\
1.64 + \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
1.65 + @{text "satisfying"} \\
1.66 + \hspace*{2ex}@{text "refl: eq x x"} \\
1.67 + \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
1.68 + \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
1.69 +
1.70 + \end{quote}
1.71 +
1.72 + \noindent From a theoretic point of view, type classes are lightweight
1.73 + modules; Haskell type classes may be emulated by
1.74 + SML functors \cite{classes_modules}.
1.75 + Isabelle/Isar offers a discipline of type classes which brings
1.76 + all those aspects together:
1.77 +
1.78 + \begin{enumerate}
1.79 + \item specifying abstract parameters together with
1.80 + corresponding specifications,
1.81 + \item instantiating those abstract parameters by a particular
1.82 + type
1.83 + \item in connection with a ``less ad-hoc'' approach to overloading,
1.84 + \item with a direct link to the Isabelle module system
1.85 + (aka locales \cite{kammueller-locales}).
1.86 + \end{enumerate}
1.87 +
1.88 + \noindent Isar type classes also directly support code generation
1.89 + in a Haskell like fashion.
1.90 +
1.91 + This tutorial demonstrates common elements of structured specifications
1.92 + and abstract reasoning with type classes by the algebraic hierarchy of
1.93 + semigroups, monoids and groups. Our background theory is that of
1.94 + Isabelle/HOL \cite{isa-tutorial}, for which some
1.95 + familiarity is assumed.
1.96 +
1.97 + Here we merely present the look-and-feel for end users.
1.98 + Internally, those are mapped to more primitive Isabelle concepts.
1.99 + See \cite{Haftmann-Wenzel:2006:classes} for more detail.
1.100 +*}
1.101 +
1.102 +section {* A simple algebra example \label{sec:example} *}
1.103 +
1.104 +subsection {* Class definition *}
1.105 +
1.106 +text {*
1.107 + Depending on an arbitrary type @{text "\<alpha>"}, class @{text
1.108 + "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
1.109 + assumed to be associative:
1.110 +*}
1.111 +
1.112 +class %quote semigroup =
1.113 + fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
1.114 + assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.115 +
1.116 +text {*
1.117 + \noindent This @{command class} specification consists of two
1.118 + parts: the \qn{operational} part names the class parameter
1.119 + (@{element "fixes"}), the \qn{logical} part specifies properties on them
1.120 + (@{element "assumes"}). The local @{element "fixes"} and
1.121 + @{element "assumes"} are lifted to the theory toplevel,
1.122 + yielding the global
1.123 + parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
1.124 + global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
1.125 + z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
1.126 +*}
1.127 +
1.128 +
1.129 +subsection {* Class instantiation \label{sec:class_inst} *}
1.130 +
1.131 +text {*
1.132 + The concrete type @{typ int} is made a @{class semigroup}
1.133 + instance by providing a suitable definition for the class parameter
1.134 + @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
1.135 + This is accomplished by the @{command instantiation} target:
1.136 +*}
1.137 +
1.138 +instantiation %quote int :: semigroup
1.139 +begin
1.140 +
1.141 +definition %quote
1.142 + mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
1.143 +
1.144 +instance %quote proof
1.145 + fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
1.146 + then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
1.147 + unfolding mult_int_def .
1.148 +qed
1.149 +
1.150 +end %quote
1.151 +
1.152 +text {*
1.153 + \noindent @{command instantiation} allows to define class parameters
1.154 + at a particular instance using common specification tools (here,
1.155 + @{command definition}). The concluding @{command instance}
1.156 + opens a proof that the given parameters actually conform
1.157 + to the class specification. Note that the first proof step
1.158 + is the @{method default} method,
1.159 + which for such instance proofs maps to the @{method intro_classes} method.
1.160 + This boils down an instance judgement to the relevant primitive
1.161 + proof goals and should conveniently always be the first method applied
1.162 + in an instantiation proof.
1.163 +
1.164 + From now on, the type-checker will consider @{typ int}
1.165 + as a @{class semigroup} automatically, i.e.\ any general results
1.166 + are immediately available on concrete instances.
1.167 +
1.168 + \medskip Another instance of @{class semigroup} are the natural numbers:
1.169 +*}
1.170 +
1.171 +instantiation %quote nat :: semigroup
1.172 +begin
1.173 +
1.174 +primrec %quote mult_nat where
1.175 + "(0\<Colon>nat) \<otimes> n = n"
1.176 + | "Suc m \<otimes> n = Suc (m \<otimes> n)"
1.177 +
1.178 +instance %quote proof
1.179 + fix m n q :: nat
1.180 + show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
1.181 + by (induct m) auto
1.182 +qed
1.183 +
1.184 +end %quote
1.185 +
1.186 +text {*
1.187 + \noindent Note the occurence of the name @{text mult_nat}
1.188 + in the primrec declaration; by default, the local name of
1.189 + a class operation @{text f} to instantiate on type constructor
1.190 + @{text \<kappa>} are mangled as @{text f_\<kappa>}. In case of uncertainty,
1.191 + these names may be inspected using the @{command "print_context"} command
1.192 + or the corresponding ProofGeneral button.
1.193 +*}
1.194 +
1.195 +subsection {* Lifting and parametric types *}
1.196 +
1.197 +text {*
1.198 + Overloaded definitions giving on class instantiation
1.199 + may include recursion over the syntactic structure of types.
1.200 + As a canonical example, we model product semigroups
1.201 + using our simple algebra:
1.202 +*}
1.203 +
1.204 +instantiation %quote * :: (semigroup, semigroup) semigroup
1.205 +begin
1.206 +
1.207 +definition %quote
1.208 + 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)"
1.209 +
1.210 +instance %quote proof
1.211 + fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
1.212 + show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
1.213 + unfolding mult_prod_def by (simp add: assoc)
1.214 +qed
1.215 +
1.216 +end %quote
1.217 +
1.218 +text {*
1.219 + \noindent Associativity from product semigroups is
1.220 + established using
1.221 + the definition of @{text "(\<otimes>)"} on products and the hypothetical
1.222 + associativity of the type components; these hypotheses
1.223 + are facts due to the @{class semigroup} constraints imposed
1.224 + on the type components by the @{command instance} proposition.
1.225 + Indeed, this pattern often occurs with parametric types
1.226 + and type classes.
1.227 +*}
1.228 +
1.229 +
1.230 +subsection {* Subclassing *}
1.231 +
1.232 +text {*
1.233 + We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
1.234 + by extending @{class semigroup}
1.235 + with one additional parameter @{text neutral} together
1.236 + with its property:
1.237 +*}
1.238 +
1.239 +class %quote monoidl = semigroup +
1.240 + fixes neutral :: "\<alpha>" ("\<one>")
1.241 + assumes neutl: "\<one> \<otimes> x = x"
1.242 +
1.243 +text {*
1.244 + \noindent Again, we prove some instances, by
1.245 + providing suitable parameter definitions and proofs for the
1.246 + additional specifications. Observe that instantiations
1.247 + for types with the same arity may be simultaneous:
1.248 +*}
1.249 +
1.250 +instantiation %quote nat and int :: monoidl
1.251 +begin
1.252 +
1.253 +definition %quote
1.254 + neutral_nat_def: "\<one> = (0\<Colon>nat)"
1.255 +
1.256 +definition %quote
1.257 + neutral_int_def: "\<one> = (0\<Colon>int)"
1.258 +
1.259 +instance %quote proof
1.260 + fix n :: nat
1.261 + show "\<one> \<otimes> n = n"
1.262 + unfolding neutral_nat_def by simp
1.263 +next
1.264 + fix k :: int
1.265 + show "\<one> \<otimes> k = k"
1.266 + unfolding neutral_int_def mult_int_def by simp
1.267 +qed
1.268 +
1.269 +end %quote
1.270 +
1.271 +instantiation %quote * :: (monoidl, monoidl) monoidl
1.272 +begin
1.273 +
1.274 +definition %quote
1.275 + neutral_prod_def: "\<one> = (\<one>, \<one>)"
1.276 +
1.277 +instance %quote proof
1.278 + fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
1.279 + show "\<one> \<otimes> p = p"
1.280 + unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
1.281 +qed
1.282 +
1.283 +end %quote
1.284 +
1.285 +text {*
1.286 + \noindent Fully-fledged monoids are modelled by another subclass
1.287 + which does not add new parameters but tightens the specification:
1.288 +*}
1.289 +
1.290 +class %quote monoid = monoidl +
1.291 + assumes neutr: "x \<otimes> \<one> = x"
1.292 +
1.293 +instantiation %quote nat and int :: monoid
1.294 +begin
1.295 +
1.296 +instance %quote proof
1.297 + fix n :: nat
1.298 + show "n \<otimes> \<one> = n"
1.299 + unfolding neutral_nat_def by (induct n) simp_all
1.300 +next
1.301 + fix k :: int
1.302 + show "k \<otimes> \<one> = k"
1.303 + unfolding neutral_int_def mult_int_def by simp
1.304 +qed
1.305 +
1.306 +end %quote
1.307 +
1.308 +instantiation %quote * :: (monoid, monoid) monoid
1.309 +begin
1.310 +
1.311 +instance %quote proof
1.312 + fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
1.313 + show "p \<otimes> \<one> = p"
1.314 + unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
1.315 +qed
1.316 +
1.317 +end %quote
1.318 +
1.319 +text {*
1.320 + \noindent To finish our small algebra example, we add a @{text group} class
1.321 + with a corresponding instance:
1.322 +*}
1.323 +
1.324 +class %quote group = monoidl +
1.325 + fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
1.326 + assumes invl: "x\<div> \<otimes> x = \<one>"
1.327 +
1.328 +instantiation %quote int :: group
1.329 +begin
1.330 +
1.331 +definition %quote
1.332 + inverse_int_def: "i\<div> = - (i\<Colon>int)"
1.333 +
1.334 +instance %quote proof
1.335 + fix i :: int
1.336 + have "-i + i = 0" by simp
1.337 + then show "i\<div> \<otimes> i = \<one>"
1.338 + unfolding mult_int_def neutral_int_def inverse_int_def .
1.339 +qed
1.340 +
1.341 +end %quote
1.342 +
1.343 +
1.344 +section {* Type classes as locales *}
1.345 +
1.346 +subsection {* A look behind the scene *}
1.347 +
1.348 +text {*
1.349 + The example above gives an impression how Isar type classes work
1.350 + in practice. As stated in the introduction, classes also provide
1.351 + a link to Isar's locale system. Indeed, the logical core of a class
1.352 + is nothing else than a locale:
1.353 +*}
1.354 +
1.355 +class %quote idem =
1.356 + fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
1.357 + assumes idem: "f (f x) = f x"
1.358 +
1.359 +text {*
1.360 + \noindent essentially introduces the locale
1.361 +*} setup %invisible {* Sign.add_path "foo" *}
1.362 +
1.363 +locale %quote idem =
1.364 + fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
1.365 + assumes idem: "f (f x) = f x"
1.366 +
1.367 +text {* \noindent together with corresponding constant(s): *}
1.368 +
1.369 +consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
1.370 +
1.371 +text {*
1.372 + \noindent The connection to the type system is done by means
1.373 + of a primitive axclass
1.374 +*} setup %invisible {* Sign.add_path "foo" *}
1.375 +
1.376 +axclass %quote idem < type
1.377 + idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
1.378 +
1.379 +text {* \noindent together with a corresponding interpretation: *}
1.380 +
1.381 +interpretation %quote idem_class:
1.382 + idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
1.383 +proof qed (rule idem)
1.384 +
1.385 +text {*
1.386 + \noindent This gives you at hand the full power of the Isabelle module system;
1.387 + conclusions in locale @{text idem} are implicitly propagated
1.388 + to class @{text idem}.
1.389 +*} setup %invisible {* Sign.parent_path *}
1.390 +
1.391 +subsection {* Abstract reasoning *}
1.392 +
1.393 +text {*
1.394 + Isabelle locales enable reasoning at a general level, while results
1.395 + are implicitly transferred to all instances. For example, we can
1.396 + now establish the @{text "left_cancel"} lemma for groups, which
1.397 + states that the function @{text "(x \<otimes>)"} is injective:
1.398 +*}
1.399 +
1.400 +lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
1.401 +proof
1.402 + assume "x \<otimes> y = x \<otimes> z"
1.403 + then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
1.404 + then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
1.405 + then show "y = z" using neutl and invl by simp
1.406 +next
1.407 + assume "y = z"
1.408 + then show "x \<otimes> y = x \<otimes> z" by simp
1.409 +qed
1.410 +
1.411 +text {*
1.412 + \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
1.413 + indicates that the result is recorded within that context for later
1.414 + use. This local theorem is also lifted to the global one @{fact
1.415 + "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
1.416 + z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
1.417 + @{text "group"} before, we may refer to that fact as well: @{prop
1.418 + [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
1.419 +*}
1.420 +
1.421 +
1.422 +subsection {* Derived definitions *}
1.423 +
1.424 +text {*
1.425 + Isabelle locales support a concept of local definitions
1.426 + in locales:
1.427 +*}
1.428 +
1.429 +primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.430 + "pow_nat 0 x = \<one>"
1.431 + | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
1.432 +
1.433 +text {*
1.434 + \noindent If the locale @{text group} is also a class, this local
1.435 + definition is propagated onto a global definition of
1.436 + @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
1.437 + with corresponding theorems
1.438 +
1.439 + @{thm pow_nat.simps [no_vars]}.
1.440 +
1.441 + \noindent As you can see from this example, for local
1.442 + definitions you may use any specification tool
1.443 + which works together with locales (e.g. \cite{krauss2006}).
1.444 +*}
1.445 +
1.446 +
1.447 +subsection {* A functor analogy *}
1.448 +
1.449 +text {*
1.450 + We introduced Isar classes by analogy to type classes
1.451 + functional programming; if we reconsider this in the
1.452 + context of what has been said about type classes and locales,
1.453 + we can drive this analogy further by stating that type
1.454 + classes essentially correspond to functors which have
1.455 + a canonical interpretation as type classes.
1.456 + Anyway, there is also the possibility of other interpretations.
1.457 + For example, also @{text list}s form a monoid with
1.458 + @{text append} and @{term "[]"} as operations, but it
1.459 + seems inappropriate to apply to lists
1.460 + the same operations as for genuinely algebraic types.
1.461 + In such a case, we simply can do a particular interpretation
1.462 + of monoids for lists:
1.463 +*}
1.464 +
1.465 +interpretation %quote list_monoid!: monoid append "[]"
1.466 + proof qed auto
1.467 +
1.468 +text {*
1.469 + \noindent This enables us to apply facts on monoids
1.470 + to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
1.471 +
1.472 + When using this interpretation pattern, it may also
1.473 + be appropriate to map derived definitions accordingly:
1.474 +*}
1.475 +
1.476 +primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
1.477 + "replicate 0 _ = []"
1.478 + | "replicate (Suc n) xs = xs @ replicate n xs"
1.479 +
1.480 +interpretation %quote list_monoid!: monoid append "[]" where
1.481 + "monoid.pow_nat append [] = replicate"
1.482 +proof -
1.483 + interpret monoid append "[]" ..
1.484 + show "monoid.pow_nat append [] = replicate"
1.485 + proof
1.486 + fix n
1.487 + show "monoid.pow_nat append [] n = replicate n"
1.488 + by (induct n) auto
1.489 + qed
1.490 +qed intro_locales
1.491 +
1.492 +
1.493 +subsection {* Additional subclass relations *}
1.494 +
1.495 +text {*
1.496 + Any @{text "group"} is also a @{text "monoid"}; this
1.497 + can be made explicit by claiming an additional
1.498 + subclass relation,
1.499 + together with a proof of the logical difference:
1.500 +*}
1.501 +
1.502 +subclass %quote (in group) monoid
1.503 +proof
1.504 + fix x
1.505 + from invl have "x\<div> \<otimes> x = \<one>" by simp
1.506 + with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
1.507 + with left_cancel show "x \<otimes> \<one> = x" by simp
1.508 +qed
1.509 +
1.510 +text {*
1.511 + \noindent The logical proof is carried out on the locale level.
1.512 + Afterwards it is propagated
1.513 + to the type system, making @{text group} an instance of
1.514 + @{text monoid} by adding an additional edge
1.515 + to the graph of subclass relations
1.516 + (cf.\ \figref{fig:subclass}).
1.517 +
1.518 + \begin{figure}[htbp]
1.519 + \begin{center}
1.520 + \small
1.521 + \unitlength 0.6mm
1.522 + \begin{picture}(40,60)(0,0)
1.523 + \put(20,60){\makebox(0,0){@{text semigroup}}}
1.524 + \put(20,40){\makebox(0,0){@{text monoidl}}}
1.525 + \put(00,20){\makebox(0,0){@{text monoid}}}
1.526 + \put(40,00){\makebox(0,0){@{text group}}}
1.527 + \put(20,55){\vector(0,-1){10}}
1.528 + \put(15,35){\vector(-1,-1){10}}
1.529 + \put(25,35){\vector(1,-3){10}}
1.530 + \end{picture}
1.531 + \hspace{8em}
1.532 + \begin{picture}(40,60)(0,0)
1.533 + \put(20,60){\makebox(0,0){@{text semigroup}}}
1.534 + \put(20,40){\makebox(0,0){@{text monoidl}}}
1.535 + \put(00,20){\makebox(0,0){@{text monoid}}}
1.536 + \put(40,00){\makebox(0,0){@{text group}}}
1.537 + \put(20,55){\vector(0,-1){10}}
1.538 + \put(15,35){\vector(-1,-1){10}}
1.539 + \put(05,15){\vector(3,-1){30}}
1.540 + \end{picture}
1.541 + \caption{Subclass relationship of monoids and groups:
1.542 + before and after establishing the relationship
1.543 + @{text "group \<subseteq> monoid"}; transitive edges are left out.}
1.544 + \label{fig:subclass}
1.545 + \end{center}
1.546 + \end{figure}
1.547 +7
1.548 + For illustration, a derived definition
1.549 + in @{text group} which uses @{text pow_nat}:
1.550 +*}
1.551 +
1.552 +definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.553 + "pow_int k x = (if k >= 0
1.554 + then pow_nat (nat k) x
1.555 + else (pow_nat (nat (- k)) x)\<div>)"
1.556 +
1.557 +text {*
1.558 + \noindent yields the global definition of
1.559 + @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
1.560 + with the corresponding theorem @{thm pow_int_def [no_vars]}.
1.561 +*}
1.562 +
1.563 +subsection {* A note on syntax *}
1.564 +
1.565 +text {*
1.566 + As a commodity, class context syntax allows to refer
1.567 + to local class operations and their global counterparts
1.568 + uniformly; type inference resolves ambiguities. For example:
1.569 +*}
1.570 +
1.571 +context %quote semigroup
1.572 +begin
1.573 +
1.574 +term %quote "x \<otimes> y" -- {* example 1 *}
1.575 +term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
1.576 +
1.577 +end %quote
1.578 +
1.579 +term %quote "x \<otimes> y" -- {* example 3 *}
1.580 +
1.581 +text {*
1.582 + \noindent Here in example 1, the term refers to the local class operation
1.583 + @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
1.584 + enforces the global class operation @{text "mult [nat]"}.
1.585 + In the global context in example 3, the reference is
1.586 + to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
1.587 +*}
1.588 +
1.589 +section {* Further issues *}
1.590 +
1.591 +subsection {* Type classes and code generation *}
1.592 +
1.593 +text {*
1.594 + Turning back to the first motivation for type classes,
1.595 + namely overloading, it is obvious that overloading
1.596 + stemming from @{command class} statements and
1.597 + @{command instantiation}
1.598 + targets naturally maps to Haskell type classes.
1.599 + The code generator framework \cite{isabelle-codegen}
1.600 + takes this into account. Concerning target languages
1.601 + lacking type classes (e.g.~SML), type classes
1.602 + are implemented by explicit dictionary construction.
1.603 + As example, let's go back to the power function:
1.604 +*}
1.605 +
1.606 +definition %quote example :: int where
1.607 + "example = pow_int 10 (-2)"
1.608 +
1.609 +text {*
1.610 + \noindent This maps to Haskell as:
1.611 +*}
1.612 +
1.613 +text %quote {*@{code_stmts example (Haskell)}*}
1.614 +
1.615 +text {*
1.616 + \noindent The whole code in SML with explicit dictionary passing:
1.617 +*}
1.618 +
1.619 +text %quote {*@{code_stmts example (SML)}*}
1.620 +
1.621 +subsection {* Inspecting the type class universe *}
1.622 +
1.623 +text {*
1.624 + To facilitate orientation in complex subclass structures,
1.625 + two diagnostics commands are provided:
1.626 +
1.627 + \begin{description}
1.628 +
1.629 + \item[@{command "print_classes"}] print a list of all classes
1.630 + together with associated operations etc.
1.631 +
1.632 + \item[@{command "class_deps"}] visualizes the subclass relation
1.633 + between all classes as a Hasse diagram.
1.634 +
1.635 + \end{description}
1.636 +*}
1.637 +
1.638 +end