--- a/doc-src/Classes/Thy/Classes.thy Fri Aug 27 14:22:15 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Fri Aug 27 14:22:33 2010 +0200
@@ -8,14 +8,14 @@
Type classes were introduced by Wadler and Blott \cite{wadler89how}
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
- @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
- types for @{text "\<alpha>"}, which is achieved by splitting introduction
- of the @{text eq} function from its overloaded definitions by means
- of @{text class} and @{text instance} declarations:
- \footnote{syntax here is a kind of isabellized Haskell}
+ to classical Haskell 1.0 type classes, not considering later
+ additions in expressiveness}. As a canonical example, a polymorphic
+ equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
+ different types for @{text "\<alpha>"}, which is achieved by splitting
+ introduction of the @{text eq} function from its overloaded
+ definitions by means of @{text class} and @{text instance}
+ declarations: \footnote{syntax here is a kind of isabellized
+ Haskell}
\begin{quote}
@@ -41,14 +41,14 @@
these annotations are assertions that a particular polymorphic type
provides definitions for overloaded functions.
- Indeed, type classes not only allow for simple overloading
- but form a generic calculus, an instance of order-sorted
- algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+ Indeed, type classes not only allow for simple overloading but form
+ a generic calculus, an instance of order-sorted algebra
+ \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- 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
+ 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 @{text "class eq"}
above could be given the following specification, demanding that
@{text "class eq"} is an equivalence relation obeying reflexivity,
@@ -65,11 +65,10 @@
\end{quote}
- \noindent From a theoretical point of view, type classes are lightweight
- modules; Haskell type classes may be emulated by
- SML functors \cite{classes_modules}.
- Isabelle/Isar offers a discipline of type classes which brings
- all those aspects together:
+ \noindent From a theoretical point of view, type classes are
+ lightweight modules; Haskell type classes may be emulated by SML
+ functors \cite{classes_modules}. Isabelle/Isar offers a discipline
+ of type classes which brings all those aspects together:
\begin{enumerate}
\item specifying abstract parameters together with
@@ -81,15 +80,15 @@
locales \cite{kammueller-locales}.
\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{Haftmann-Wenzel:2006:classes}.
+ \noindent Isar type classes also directly support code generation in
+ a Haskell like fashion. Internally, they are mapped to more
+ primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
- This tutorial demonstrates common elements of structured specifications
- and abstract reasoning with type classes by the algebraic hierarchy of
- semigroups, monoids and groups. Our background theory is that of
- Isabelle/HOL \cite{isa-tutorial}, for which some
- familiarity is assumed.
+ This tutorial demonstrates common elements of structured
+ specifications and abstract reasoning with type classes by the
+ algebraic hierarchy of semigroups, monoids and groups. Our
+ background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
+ which some familiarity is assumed.
*}
section {* A simple algebra example \label{sec:example} *}
@@ -107,25 +106,24 @@
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
text {*
- \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
+ \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] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
- global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
- z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+ global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
+ \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
*}
subsection {* Class instantiation \label{sec:class_inst} *}
text {*
- The concrete type @{typ int} is made a @{class semigroup}
- instance by providing a suitable definition for the class parameter
- @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
- This is accomplished by the @{command instantiation} target:
+ The concrete type @{typ int} is made a @{class semigroup} instance
+ by providing a suitable definition for the class parameter @{text
+ "(\<otimes>)"} and a proof for the specification of @{fact assoc}. This is
+ accomplished by the @{command instantiation} target:
*}
instantiation %quote int :: semigroup
@@ -143,22 +141,22 @@
end %quote
text {*
- \noindent @{command instantiation} defines class parameters
- at a particular instance using 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 default} 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 instantiation proof.
+ \noindent @{command instantiation} defines class parameters at a
+ particular instance using 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
+ default} 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 instantiation proof.
- From now on, the type-checker will consider @{typ int}
- as a @{class semigroup} automatically, i.e.\ any general results
- are immediately available on concrete instances.
+ From now on, the type-checker will consider @{typ int} as a @{class
+ semigroup} automatically, i.e.\ any general results are immediately
+ available on concrete instances.
- \medskip Another instance of @{class semigroup} yields the natural numbers:
+ \medskip Another instance of @{class semigroup} yields the natural
+ numbers:
*}
instantiation %quote nat :: semigroup
@@ -177,21 +175,20 @@
end %quote
text {*
- \noindent Note the occurence of the name @{text mult_nat}
- in the primrec declaration; by default, the local name of
- a class operation @{text f} to be instantiated on type constructor
- @{text \<kappa>} is mangled as @{text f_\<kappa>}. In case of uncertainty,
- these names may be inspected using the @{command "print_context"} command
- or the corresponding ProofGeneral button.
+ \noindent Note the occurence of the name @{text mult_nat} in the
+ primrec declaration; by default, the local name of a class operation
+ @{text f} to be instantiated on type constructor @{text \<kappa>} is
+ mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
+ inspected using the @{command "print_context"} command or the
+ corresponding ProofGeneral button.
*}
subsection {* Lifting and parametric types *}
text {*
- Overloaded definitions given at a class instantiation
- may include recursion over the syntactic structure of types.
- As a canonical example, we model product semigroups
- using our simple algebra:
+ Overloaded definitions given at a class instantiation may include
+ recursion over the syntactic structure of types. As a canonical
+ example, we model product semigroups using our simple algebra:
*}
instantiation %quote prod :: (semigroup, semigroup) semigroup
@@ -211,21 +208,19 @@
text {*
\noindent Associativity of product semigroups is established using
the definition of @{text "(\<otimes>)"} on products and the hypothetical
- associativity of the type components; these hypotheses
- are legitimate due to the @{class semigroup} constraints imposed
- on the type components by the @{command instance} proposition.
- Indeed, this pattern often occurs with parametric types
- and type classes.
+ associativity of the type components; these hypotheses are
+ legitimate due to the @{class semigroup} constraints imposed on the
+ type components by the @{command instance} proposition. Indeed,
+ this pattern often occurs with parametric types and type classes.
*}
subsection {* Subclassing *}
text {*
- We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
- by extending @{class semigroup}
- with one additional parameter @{text neutral} together
- with its characteristic property:
+ We define a subclass @{text monoidl} (a semigroup with a left-hand
+ neutral) by extending @{class semigroup} with one additional
+ parameter @{text neutral} together with its characteristic property:
*}
class %quote monoidl = semigroup +
@@ -233,10 +228,10 @@
assumes neutl: "\<one> \<otimes> x = x"
text {*
- \noindent Again, we prove some instances, by
- providing suitable parameter definitions and proofs for the
- additional specifications. Observe that instantiations
- for types with the same arity may be simultaneous:
+ \noindent Again, we prove some instances, by providing suitable
+ parameter definitions and proofs for the additional specifications.
+ Observe that instantiations for types with the same arity may be
+ simultaneous:
*}
instantiation %quote nat and int :: monoidl
@@ -309,8 +304,8 @@
end %quote
text {*
- \noindent To finish our small algebra example, we add a @{text group} class
- with a corresponding instance:
+ \noindent To finish our small algebra example, we add a @{text
+ group} class with a corresponding instance:
*}
class %quote group = monoidl +
@@ -338,9 +333,9 @@
subsection {* A look behind the scenes *}
text {*
- The example above gives an impression how Isar type classes work
- in practice. As stated in the introduction, classes also provide
- a link to Isar's locale system. Indeed, the logical core of a class
+ The example above gives an impression how Isar type classes work in
+ practice. As stated in the introduction, classes also provide a
+ link to Isar's locale system. Indeed, the logical core of a class
is nothing other than a locale:
*}
@@ -402,13 +397,14 @@
qed
text {*
- \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
- indicates that the result is recorded within that context for later
- use. This local theorem is also lifted to the global one @{fact
- "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
- z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
- @{text "group"} before, we may refer to that fact as well: @{prop
- [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
+ \noindent Here the \qt{@{keyword "in"} @{class group}} target
+ specification indicates that the result is recorded within that
+ context for later use. This local theorem is also lifted to the
+ global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
+ \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been
+ made an instance of @{text "group"} before, we may refer to that
+ fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
+ z"}.
*}
@@ -424,15 +420,14 @@
text {*
\noindent If the locale @{text group} is also a class, this local
- definition is propagated onto a global definition of
- @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
- with corresponding theorems
+ definition is propagated onto a global definition of @{term [source]
+ "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} 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
+ \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{krauss2006}.
*}
@@ -440,19 +435,17 @@
subsection {* A functor analogy *}
text {*
- We introduced Isar classes by analogy to type classes in
- functional programming; if we reconsider this in the
- context of what has been said about type classes and 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 is also the possibility of other interpretations.
- For example, @{text list}s also form a monoid with
- @{text append} and @{term "[]"} 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:
+ We introduced Isar classes by analogy to type classes in functional
+ programming; if we reconsider this in the context of what has been
+ said about type classes and 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 is also the possibility of other interpretations. For
+ example, @{text list}s also form a monoid with @{text append} and
+ @{term "[]"} 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:
*}
interpretation %quote list_monoid: monoid append "[]"
@@ -510,12 +503,10 @@
qed
text {*
- The logical proof is carried out on the locale level.
- Afterwards it is propagated
- to the type system, making @{text group} an instance of
- @{text monoid} by adding an additional edge
- to the graph of subclass relations
- (\figref{fig:subclass}).
+ The logical proof is carried out on the locale level. Afterwards it
+ is propagated to the type system, making @{text group} an instance
+ of @{text monoid} by adding an additional edge to the graph of
+ subclass relations (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -547,8 +538,8 @@
\end{center}
\end{figure}
- For illustration, a derived definition
- in @{text group} using @{text pow_nat}
+ For illustration, a derived definition in @{text group} using @{text
+ pow_nat}
*}
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -557,17 +548,17 @@
else (pow_nat (nat (- k)) x)\<div>)"
text {*
- \noindent yields the global definition of
- @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
- with the corresponding theorem @{thm pow_int_def [no_vars]}.
+ \noindent yields the global definition of @{term [source] "pow_int \<Colon>
+ int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
+ pow_int_def [no_vars]}.
*}
subsection {* A note on syntax *}
text {*
- As a convenience, class context syntax allows references
- to local class operations and their global counterparts
- uniformly; type inference resolves ambiguities. For example:
+ As a convenience, class context syntax allows references to local
+ class operations and their global counterparts uniformly; type
+ inference resolves ambiguities. For example:
*}
context %quote semigroup
@@ -581,11 +572,11 @@
term %quote "x \<otimes> y" -- {* example 3 *}
text {*
- \noindent Here in example 1, the term refers to the local class operation
- @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
- enforces the global class operation @{text "mult [nat]"}.
- In the global context in example 3, the reference is
- to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+ \noindent Here in example 1, the term refers to the local class
+ operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
+ constraint enforces the global class operation @{text "mult [nat]"}.
+ In the global context in example 3, the reference is to the
+ polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
*}
section {* Further issues *}
@@ -593,16 +584,14 @@
subsection {* Type classes and code generation *}
text {*
- Turning back to 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{isabelle-codegen}
- 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:
+ Turning back to 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{isabelle-codegen} 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:
*}
definition %quote example :: int where
@@ -619,11 +608,18 @@
*}
text %quote {*@{code_stmts example (SML)}*}
+text {*
+ \noindent In Scala, implicts are used as dictionaries:
+*}
+(*<*)code_include %invisible Scala "Natural" -(*>*)
+text %quote {*@{code_stmts example (Scala)}*}
+
+
subsection {* Inspecting the type class universe *}
text {*
- To facilitate orientation in complex subclass structures,
- two diagnostics commands are provided:
+ To facilitate orientation in complex subclass structures, two
+ diagnostics commands are provided:
\begin{description}