# HG changeset patch # User paulson # Date 1245254837 -3600 # Node ID 7d50527dc0088b70eb4ba938da85b7b12f73173d # Parent cc37bf07f9bb375cd372b8b50a9b1db2f28972b5 Polishing the English diff -r cc37bf07f9bb -r 7d50527dc008 doc-src/Classes/Thy/Classes.thy --- 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 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" + mult_prod_def: "p1 \ p2 = (fst p1 \ fst p2, snd p1 \ snd p2)" instance %quote proof - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" - show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ p\<^isub>3)" + fix p1 p2 p3 :: "\\semigroup \ \\semigroup" + show "p1 \ p2 \ p3 = p1 \ (p2 \ 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 "(\)"} 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 \ \ \ \" 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)}*} diff -r cc37bf07f9bb -r 7d50527dc008 doc-src/Classes/Thy/document/Classes.tex --- 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})\\ diff -r cc37bf07f9bb -r 7d50527dc008 doc-src/Classes/classes.tex --- 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.