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)}*}