--- 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)}*}
--- a/doc-src/Classes/Thy/document/Classes.tex Wed Jun 17 15:41:49 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Jun 17 17:07:17 2009 +0100
@@ -23,8 +23,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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}.
@@ -61,9 +61,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
@@ -83,7 +83,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
@@ -95,22 +95,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.%
+ familiarity is assumed.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -207,22 +204,22 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
at a particular instance using common specification tools (here,
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
opens a proof that the given parameters actually conform
to the class specification. Note that the first proof step
is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}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 \isa{int}
as a \isa{semigroup} automatically, i.e.\ any general results
are immediately available on concrete instances.
- \medskip Another instance of \isa{semigroup} are the natural numbers:%
+ \medskip Another instance of \isa{semigroup} yields the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -264,8 +261,8 @@
\begin{isamarkuptext}%
\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
in the primrec declaration; by default, the local name of
- a class operation \isa{f} to instantiate on type constructor
- \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
+ a class operation \isa{f} to be instantiated on type constructor
+ \isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
or the corresponding ProofGeneral button.%
\end{isamarkuptext}%
@@ -276,7 +273,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Overloaded definitions giving 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:%
@@ -294,15 +291,15 @@
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
@@ -319,11 +316,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Associativity from product semigroups is
- established using
+\noindent Associativity of product semigroups is established using
the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
associativity of the type components; these hypotheses
- are facts due to the \isa{semigroup} constraints imposed
+ are legitimate due to the \isa{semigroup} constraints imposed
on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
Indeed, this pattern often occurs with parametric types
and type classes.%
@@ -338,7 +334,7 @@
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
by extending \isa{semigroup}
with one additional parameter \isa{neutral} together
- with its property:%
+ with its characteristic property:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -439,7 +435,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\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:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -562,7 +558,7 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{A look behind the scene%
+\isamarkupsubsection{A look behind the scenes%
}
\isamarkuptrue%
%
@@ -570,7 +566,7 @@
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:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -714,7 +710,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\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 \isa{idem} are implicitly propagated
to class \isa{idem}.%
\end{isamarkuptext}%
@@ -832,7 +828,8 @@
\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}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -841,18 +838,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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 \isa{list}s form a monoid with
+ There is also the possibility of other interpretations.
+ For example, \isa{list}s also form a monoid with
\isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} 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:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -982,7 +979,7 @@
to the type system, making \isa{group} an instance of
\isa{monoid} by adding an additional edge
to the graph of subclass relations
- (cf.\ \figref{fig:subclass}).
+ (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -1015,7 +1012,7 @@
\end{figure}
For illustration, a derived definition
- in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
+ in \isa{group} using \isa{pow{\isacharunderscore}nat}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1048,7 +1045,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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:%
\end{isamarkuptext}%
@@ -1113,9 +1110,9 @@
\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{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:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1136,7 +1133,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This maps to Haskell as:%
+\noindent This maps to Haskell as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1223,7 +1220,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The whole code in SML with explicit dictionary passing:%
+\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1250,16 +1247,15 @@
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoidl =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
+\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}semigroup{\char95}monoidl A{\char95};\\
\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
-\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
+\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}monoidl{\char95}monoid A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
-\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
+\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
+\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}monoid{\char95}group A{\char95};\\
\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
\hspace*{0pt}\\
\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
@@ -1271,14 +1267,12 @@
\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
\hspace*{0pt}\\
\hspace*{0pt}val monoidl{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
+\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int monoidl;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int monoid;\\
+\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
\hspace*{0pt}\\
-\hspace*{0pt}val group{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
+\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
--- a/doc-src/Classes/classes.tex Wed Jun 17 15:41:49 2009 +0200
+++ b/doc-src/Classes/classes.tex Wed Jun 17 17:07:17 2009 +0100
@@ -21,8 +21,7 @@
\maketitle
\begin{abstract}
- \noindent This tutorial introduces the look-and-feel of
- Isar type classes to the end-user. Isar type classes
+ \noindent This tutorial introduces Isar type classes, which
are a convenient mechanism for organizing specifications.
Essentially, they combine an operational aspect (in the
manner of Haskell) with a logical aspect, both managed uniformly.