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