--- a/doc-src/Classes/Thy/Classes.thy Wed Jun 17 15:41:49 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Wed Jun 17 17:07:17 2009 +0100
@@ -5,8 +5,8 @@
section {* Introduction *}
text {*
- Type classes were introduces by Wadler and Blott \cite{wadler89how}
- into the Haskell language, to allow for a reasonable implementation
+ 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}.
@@ -43,9 +43,9 @@
Indeed, type classes not only allow for simple overloading
but form a generic calculus, an instance of order-sorted
- algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+ algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- From a software engeneering point of view, type classes
+ 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
@@ -65,7 +65,7 @@
\end{quote}
- \noindent From a theoretic point of view, type classes are lightweight
+ \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
@@ -77,22 +77,19 @@
\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
- (aka locales \cite{kammueller-locales}).
+ \item with a direct link to the Isabelle module system:
+ locales \cite{kammueller-locales}.
\end{enumerate}
\noindent Isar type classes also directly support code generation
- in a Haskell like fashion.
+ 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.
-
- Here we merely present the look-and-feel for end users.
- Internally, those are mapped to more primitive Isabelle concepts.
- See \cite{Haftmann-Wenzel:2006:classes} for more detail.
*}
section {* A simple algebra example \label{sec:example} *}
@@ -146,22 +143,22 @@
end %quote
text {*
- \noindent @{command instantiation} allows to define class parameters
+ \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 boils down an instance judgement to the relevant primitive
- proof goals and should conveniently always be the first method applied
+ 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.
- \medskip Another instance of @{class semigroup} are the natural numbers:
+ \medskip Another instance of @{class semigroup} yields the natural numbers:
*}
instantiation %quote nat :: semigroup
@@ -191,7 +188,7 @@
subsection {* Lifting and parametric types *}
text {*
- Overloaded definitions given on class instantiation
+ 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:
@@ -201,11 +198,11 @@
begin
definition %quote
- 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)"
+ mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
instance %quote proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
- show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+ fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+ show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
unfolding mult_prod_def by (simp add: assoc)
qed
@@ -215,7 +212,7 @@
\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 facts due to the @{class semigroup} constraints imposed
+ 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.
@@ -228,7 +225,7 @@
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 property:
+ with its characteristic property:
*}
class %quote monoidl = semigroup +
@@ -278,7 +275,7 @@
end %quote
text {*
- \noindent Fully-fledged monoids are modelled by another subclass
+ \noindent Fully-fledged monoids are modelled by another subclass,
which does not add new parameters but tightens the specification:
*}
@@ -338,13 +335,13 @@
section {* Type classes as locales *}
-subsection {* A look behind the scene *}
+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
- is nothing else than a locale:
+ is nothing other than a locale:
*}
class %quote idem =
@@ -378,7 +375,7 @@
proof qed (rule idem)
text {*
- \noindent This gives you at hand the full power of the Isabelle module system;
+ \noindent This gives you the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
to class @{text idem}.
*} (*<*)setup %invisible {* Sign.parent_path *}
@@ -435,25 +432,26 @@
\noindent As you can see from this example, for local
definitions you may use any specification tool
- which works together with locales (e.g. \cite{krauss2006}).
+ which works together with locales, such as Krauss's recursive function package
+ \cite{krauss2006}.
*}
subsection {* A functor analogy *}
text {*
- We introduced Isar classes by analogy to type classes
+ 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 which have
+ classes essentially correspond to functors that have
a canonical interpretation as type classes.
- Anyway, there is also the possibility of other interpretations.
- For example, also @{text list}s form a monoid with
+ 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 simply can do a particular interpretation
+ In such a case, we can simply make a particular interpretation
of monoids for lists:
*}
@@ -517,7 +515,7 @@
to the type system, making @{text group} an instance of
@{text monoid} by adding an additional edge
to the graph of subclass relations
- (cf.\ \figref{fig:subclass}).
+ (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -550,7 +548,7 @@
\end{figure}
For illustration, a derived definition
- in @{text group} which uses @{text pow_nat}:
+ in @{text group} using @{text pow_nat}
*}
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -567,7 +565,7 @@
subsection {* A note on syntax *}
text {*
- As a convenience, class context syntax allows to refer
+ As a convenience, class context syntax allows references
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:
*}
@@ -601,9 +599,9 @@
@{command instantiation}
targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
- takes this into account. Concerning target languages
- lacking type classes (e.g.~SML), type classes
- are implemented by explicit dictionary construction.
+ 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:
*}
@@ -611,13 +609,13 @@
"example = pow_int 10 (-2)"
text {*
- \noindent This maps to Haskell as:
+ \noindent This maps to Haskell as follows:
*}
text %quote {*@{code_stmts example (Haskell)}*}
text {*
- \noindent The whole code in SML with explicit dictionary passing:
+ \noindent The code in SML has explicit dictionary passing:
*}
text %quote {*@{code_stmts example (SML)}*}