1.1 --- a/doc-src/Classes/Thy/Classes.thy Wed Jun 17 15:41:49 2009 +0200
1.2 +++ b/doc-src/Classes/Thy/Classes.thy Wed Jun 17 17:07:17 2009 +0100
1.3 @@ -5,8 +5,8 @@
1.4 section {* Introduction *}
1.5
1.6 text {*
1.7 - Type classes were introduces by Wadler and Blott \cite{wadler89how}
1.8 - into the Haskell language, to allow for a reasonable implementation
1.9 + Type classes were introduced by Wadler and Blott \cite{wadler89how}
1.10 + into the Haskell language to allow for a reasonable implementation
1.11 of overloading\footnote{throughout this tutorial, we are referring
1.12 to classical Haskell 1.0 type classes, not considering
1.13 later additions in expressiveness}.
1.14 @@ -43,9 +43,9 @@
1.15
1.16 Indeed, type classes not only allow for simple overloading
1.17 but form a generic calculus, an instance of order-sorted
1.18 - algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
1.19 + algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
1.20
1.21 - From a software engeneering point of view, type classes
1.22 + From a software engineering point of view, type classes
1.23 roughly correspond to interfaces in object-oriented languages like Java;
1.24 so, it is naturally desirable that type classes do not only
1.25 provide functions (class parameters) but also state specifications
1.26 @@ -65,7 +65,7 @@
1.27
1.28 \end{quote}
1.29
1.30 - \noindent From a theoretic point of view, type classes are lightweight
1.31 + \noindent From a theoretical point of view, type classes are lightweight
1.32 modules; Haskell type classes may be emulated by
1.33 SML functors \cite{classes_modules}.
1.34 Isabelle/Isar offers a discipline of type classes which brings
1.35 @@ -77,22 +77,19 @@
1.36 \item instantiating those abstract parameters by a particular
1.37 type
1.38 \item in connection with a ``less ad-hoc'' approach to overloading,
1.39 - \item with a direct link to the Isabelle module system
1.40 - (aka locales \cite{kammueller-locales}).
1.41 + \item with a direct link to the Isabelle module system:
1.42 + locales \cite{kammueller-locales}.
1.43 \end{enumerate}
1.44
1.45 \noindent Isar type classes also directly support code generation
1.46 - in a Haskell like fashion.
1.47 + in a Haskell like fashion. Internally, they are mapped to more primitive
1.48 + Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
1.49
1.50 This tutorial demonstrates common elements of structured specifications
1.51 and abstract reasoning with type classes by the algebraic hierarchy of
1.52 semigroups, monoids and groups. Our background theory is that of
1.53 Isabelle/HOL \cite{isa-tutorial}, for which some
1.54 familiarity is assumed.
1.55 -
1.56 - Here we merely present the look-and-feel for end users.
1.57 - Internally, those are mapped to more primitive Isabelle concepts.
1.58 - See \cite{Haftmann-Wenzel:2006:classes} for more detail.
1.59 *}
1.60
1.61 section {* A simple algebra example \label{sec:example} *}
1.62 @@ -146,22 +143,22 @@
1.63 end %quote
1.64
1.65 text {*
1.66 - \noindent @{command instantiation} allows to define class parameters
1.67 + \noindent @{command instantiation} defines class parameters
1.68 at a particular instance using common specification tools (here,
1.69 @{command definition}). The concluding @{command instance}
1.70 opens a proof that the given parameters actually conform
1.71 to the class specification. Note that the first proof step
1.72 is the @{method default} method,
1.73 which for such instance proofs maps to the @{method intro_classes} method.
1.74 - This boils down an instance judgement to the relevant primitive
1.75 - proof goals and should conveniently always be the first method applied
1.76 + This reduces an instance judgement to the relevant primitive
1.77 + proof goals; typically it is the first method applied
1.78 in an instantiation proof.
1.79
1.80 From now on, the type-checker will consider @{typ int}
1.81 as a @{class semigroup} automatically, i.e.\ any general results
1.82 are immediately available on concrete instances.
1.83
1.84 - \medskip Another instance of @{class semigroup} are the natural numbers:
1.85 + \medskip Another instance of @{class semigroup} yields the natural numbers:
1.86 *}
1.87
1.88 instantiation %quote nat :: semigroup
1.89 @@ -191,7 +188,7 @@
1.90 subsection {* Lifting and parametric types *}
1.91
1.92 text {*
1.93 - Overloaded definitions given on class instantiation
1.94 + Overloaded definitions given at a class instantiation
1.95 may include recursion over the syntactic structure of types.
1.96 As a canonical example, we model product semigroups
1.97 using our simple algebra:
1.98 @@ -201,11 +198,11 @@
1.99 begin
1.100
1.101 definition %quote
1.102 - 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)"
1.103 + mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
1.104
1.105 instance %quote proof
1.106 - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
1.107 - show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
1.108 + fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
1.109 + show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
1.110 unfolding mult_prod_def by (simp add: assoc)
1.111 qed
1.112
1.113 @@ -215,7 +212,7 @@
1.114 \noindent Associativity of product semigroups is established using
1.115 the definition of @{text "(\<otimes>)"} on products and the hypothetical
1.116 associativity of the type components; these hypotheses
1.117 - are facts due to the @{class semigroup} constraints imposed
1.118 + are legitimate due to the @{class semigroup} constraints imposed
1.119 on the type components by the @{command instance} proposition.
1.120 Indeed, this pattern often occurs with parametric types
1.121 and type classes.
1.122 @@ -228,7 +225,7 @@
1.123 We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
1.124 by extending @{class semigroup}
1.125 with one additional parameter @{text neutral} together
1.126 - with its property:
1.127 + with its characteristic property:
1.128 *}
1.129
1.130 class %quote monoidl = semigroup +
1.131 @@ -278,7 +275,7 @@
1.132 end %quote
1.133
1.134 text {*
1.135 - \noindent Fully-fledged monoids are modelled by another subclass
1.136 + \noindent Fully-fledged monoids are modelled by another subclass,
1.137 which does not add new parameters but tightens the specification:
1.138 *}
1.139
1.140 @@ -338,13 +335,13 @@
1.141
1.142 section {* Type classes as locales *}
1.143
1.144 -subsection {* A look behind the scene *}
1.145 +subsection {* A look behind the scenes *}
1.146
1.147 text {*
1.148 The example above gives an impression how Isar type classes work
1.149 in practice. As stated in the introduction, classes also provide
1.150 a link to Isar's locale system. Indeed, the logical core of a class
1.151 - is nothing else than a locale:
1.152 + is nothing other than a locale:
1.153 *}
1.154
1.155 class %quote idem =
1.156 @@ -378,7 +375,7 @@
1.157 proof qed (rule idem)
1.158
1.159 text {*
1.160 - \noindent This gives you at hand the full power of the Isabelle module system;
1.161 + \noindent This gives you the full power of the Isabelle module system;
1.162 conclusions in locale @{text idem} are implicitly propagated
1.163 to class @{text idem}.
1.164 *} (*<*)setup %invisible {* Sign.parent_path *}
1.165 @@ -435,25 +432,26 @@
1.166
1.167 \noindent As you can see from this example, for local
1.168 definitions you may use any specification tool
1.169 - which works together with locales (e.g. \cite{krauss2006}).
1.170 + which works together with locales, such as Krauss's recursive function package
1.171 + \cite{krauss2006}.
1.172 *}
1.173
1.174
1.175 subsection {* A functor analogy *}
1.176
1.177 text {*
1.178 - We introduced Isar classes by analogy to type classes
1.179 + We introduced Isar classes by analogy to type classes in
1.180 functional programming; if we reconsider this in the
1.181 context of what has been said about type classes and locales,
1.182 we can drive this analogy further by stating that type
1.183 - classes essentially correspond to functors which have
1.184 + classes essentially correspond to functors that have
1.185 a canonical interpretation as type classes.
1.186 - Anyway, there is also the possibility of other interpretations.
1.187 - For example, also @{text list}s form a monoid with
1.188 + There is also the possibility of other interpretations.
1.189 + For example, @{text list}s also form a monoid with
1.190 @{text append} and @{term "[]"} as operations, but it
1.191 seems inappropriate to apply to lists
1.192 the same operations as for genuinely algebraic types.
1.193 - In such a case, we simply can do a particular interpretation
1.194 + In such a case, we can simply make a particular interpretation
1.195 of monoids for lists:
1.196 *}
1.197
1.198 @@ -517,7 +515,7 @@
1.199 to the type system, making @{text group} an instance of
1.200 @{text monoid} by adding an additional edge
1.201 to the graph of subclass relations
1.202 - (cf.\ \figref{fig:subclass}).
1.203 + (\figref{fig:subclass}).
1.204
1.205 \begin{figure}[htbp]
1.206 \begin{center}
1.207 @@ -550,7 +548,7 @@
1.208 \end{figure}
1.209
1.210 For illustration, a derived definition
1.211 - in @{text group} which uses @{text pow_nat}:
1.212 + in @{text group} using @{text pow_nat}
1.213 *}
1.214
1.215 definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.216 @@ -567,7 +565,7 @@
1.217 subsection {* A note on syntax *}
1.218
1.219 text {*
1.220 - As a convenience, class context syntax allows to refer
1.221 + As a convenience, class context syntax allows references
1.222 to local class operations and their global counterparts
1.223 uniformly; type inference resolves ambiguities. For example:
1.224 *}
1.225 @@ -601,9 +599,9 @@
1.226 @{command instantiation}
1.227 targets naturally maps to Haskell type classes.
1.228 The code generator framework \cite{isabelle-codegen}
1.229 - takes this into account. Concerning target languages
1.230 - lacking type classes (e.g.~SML), type classes
1.231 - are implemented by explicit dictionary construction.
1.232 + takes this into account. If the target language (e.g.~SML)
1.233 + lacks type classes, then they
1.234 + are implemented by an explicit dictionary construction.
1.235 As example, let's go back to the power function:
1.236 *}
1.237
1.238 @@ -611,13 +609,13 @@
1.239 "example = pow_int 10 (-2)"
1.240
1.241 text {*
1.242 - \noindent This maps to Haskell as:
1.243 + \noindent This maps to Haskell as follows:
1.244 *}
1.245
1.246 text %quote {*@{code_stmts example (Haskell)}*}
1.247
1.248 text {*
1.249 - \noindent The whole code in SML with explicit dictionary passing:
1.250 + \noindent The code in SML has explicit dictionary passing:
1.251 *}
1.252
1.253 text %quote {*@{code_stmts example (SML)}*}