author | haftmann |

Fri Aug 27 14:22:33 2010 +0200 (2010-08-27) | |

changeset 38812 | e527a34bf69d |

parent 38811 | c3511b112595 |

child 38813 | f50f0802ba99 |

tuned whitespace

1.1 --- a/doc-src/Classes/Thy/Classes.thy Fri Aug 27 14:22:15 2010 +0200 1.2 +++ b/doc-src/Classes/Thy/Classes.thy Fri Aug 27 14:22:33 2010 +0200 1.3 @@ -8,14 +8,14 @@ 1.4 Type classes were introduced by Wadler and Blott \cite{wadler89how} 1.5 into the Haskell language to allow for a reasonable implementation 1.6 of overloading\footnote{throughout this tutorial, we are referring 1.7 - to classical Haskell 1.0 type classes, not considering 1.8 - later additions in expressiveness}. 1.9 - As a canonical example, a polymorphic equality function 1.10 - @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different 1.11 - types for @{text "\<alpha>"}, which is achieved by splitting introduction 1.12 - of the @{text eq} function from its overloaded definitions by means 1.13 - of @{text class} and @{text instance} declarations: 1.14 - \footnote{syntax here is a kind of isabellized Haskell} 1.15 + to classical Haskell 1.0 type classes, not considering later 1.16 + additions in expressiveness}. As a canonical example, a polymorphic 1.17 + equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on 1.18 + different types for @{text "\<alpha>"}, which is achieved by splitting 1.19 + introduction of the @{text eq} function from its overloaded 1.20 + definitions by means of @{text class} and @{text instance} 1.21 + declarations: \footnote{syntax here is a kind of isabellized 1.22 + Haskell} 1.23 1.24 \begin{quote} 1.25 1.26 @@ -41,14 +41,14 @@ 1.27 these annotations are assertions that a particular polymorphic type 1.28 provides definitions for overloaded functions. 1.29 1.30 - Indeed, type classes not only allow for simple overloading 1.31 - but form a generic calculus, an instance of order-sorted 1.32 - algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}. 1.33 + Indeed, type classes not only allow for simple overloading but form 1.34 + a generic calculus, an instance of order-sorted algebra 1.35 + \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}. 1.36 1.37 - From a software engineering point of view, type classes 1.38 - roughly correspond to interfaces in object-oriented languages like Java; 1.39 - so, it is naturally desirable that type classes do not only 1.40 - provide functions (class parameters) but also state specifications 1.41 + From a software engineering point of view, type classes roughly 1.42 + correspond to interfaces in object-oriented languages like Java; so, 1.43 + it is naturally desirable that type classes do not only provide 1.44 + functions (class parameters) but also state specifications 1.45 implementations must obey. For example, the @{text "class eq"} 1.46 above could be given the following specification, demanding that 1.47 @{text "class eq"} is an equivalence relation obeying reflexivity, 1.48 @@ -65,11 +65,10 @@ 1.49 1.50 \end{quote} 1.51 1.52 - \noindent From a theoretical point of view, type classes are lightweight 1.53 - modules; Haskell type classes may be emulated by 1.54 - SML functors \cite{classes_modules}. 1.55 - Isabelle/Isar offers a discipline of type classes which brings 1.56 - all those aspects together: 1.57 + \noindent From a theoretical point of view, type classes are 1.58 + lightweight modules; Haskell type classes may be emulated by SML 1.59 + functors \cite{classes_modules}. Isabelle/Isar offers a discipline 1.60 + of type classes which brings all those aspects together: 1.61 1.62 \begin{enumerate} 1.63 \item specifying abstract parameters together with 1.64 @@ -81,15 +80,15 @@ 1.65 locales \cite{kammueller-locales}. 1.66 \end{enumerate} 1.67 1.68 - \noindent Isar type classes also directly support code generation 1.69 - in a Haskell like fashion. Internally, they are mapped to more primitive 1.70 - Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}. 1.71 + \noindent Isar type classes also directly support code generation in 1.72 + a Haskell like fashion. Internally, they are mapped to more 1.73 + primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}. 1.74 1.75 - This tutorial demonstrates common elements of structured specifications 1.76 - and abstract reasoning with type classes by the algebraic hierarchy of 1.77 - semigroups, monoids and groups. Our background theory is that of 1.78 - Isabelle/HOL \cite{isa-tutorial}, for which some 1.79 - familiarity is assumed. 1.80 + This tutorial demonstrates common elements of structured 1.81 + specifications and abstract reasoning with type classes by the 1.82 + algebraic hierarchy of semigroups, monoids and groups. Our 1.83 + background theory is that of Isabelle/HOL \cite{isa-tutorial}, for 1.84 + which some familiarity is assumed. 1.85 *} 1.86 1.87 section {* A simple algebra example \label{sec:example} *} 1.88 @@ -107,25 +106,24 @@ 1.89 assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 1.90 1.91 text {* 1.92 - \noindent This @{command class} specification consists of two 1.93 - parts: the \qn{operational} part names the class parameter 1.94 - (@{element "fixes"}), the \qn{logical} part specifies properties on them 1.95 - (@{element "assumes"}). The local @{element "fixes"} and 1.96 - @{element "assumes"} are lifted to the theory toplevel, 1.97 - yielding the global 1.98 + \noindent This @{command class} specification consists of two parts: 1.99 + the \qn{operational} part names the class parameter (@{element 1.100 + "fixes"}), the \qn{logical} part specifies properties on them 1.101 + (@{element "assumes"}). The local @{element "fixes"} and @{element 1.102 + "assumes"} are lifted to the theory toplevel, yielding the global 1.103 parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the 1.104 - global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y 1.105 - z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}. 1.106 + global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon> 1.107 + \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}. 1.108 *} 1.109 1.110 1.111 subsection {* Class instantiation \label{sec:class_inst} *} 1.112 1.113 text {* 1.114 - The concrete type @{typ int} is made a @{class semigroup} 1.115 - instance by providing a suitable definition for the class parameter 1.116 - @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}. 1.117 - This is accomplished by the @{command instantiation} target: 1.118 + The concrete type @{typ int} is made a @{class semigroup} instance 1.119 + by providing a suitable definition for the class parameter @{text 1.120 + "(\<otimes>)"} and a proof for the specification of @{fact assoc}. This is 1.121 + accomplished by the @{command instantiation} target: 1.122 *} 1.123 1.124 instantiation %quote int :: semigroup 1.125 @@ -143,22 +141,22 @@ 1.126 end %quote 1.127 1.128 text {* 1.129 - \noindent @{command instantiation} defines class parameters 1.130 - at a particular instance using common specification tools (here, 1.131 - @{command definition}). The concluding @{command instance} 1.132 - opens a proof that the given parameters actually conform 1.133 - to the class specification. Note that the first proof step 1.134 - is the @{method default} method, 1.135 - which for such instance proofs maps to the @{method intro_classes} method. 1.136 - This reduces an instance judgement to the relevant primitive 1.137 - proof goals; typically it is the first method applied 1.138 - in an instantiation proof. 1.139 + \noindent @{command instantiation} defines class parameters at a 1.140 + particular instance using common specification tools (here, 1.141 + @{command definition}). The concluding @{command instance} opens a 1.142 + proof that the given parameters actually conform to the class 1.143 + specification. Note that the first proof step is the @{method 1.144 + default} method, which for such instance proofs maps to the @{method 1.145 + intro_classes} method. This reduces an instance judgement to the 1.146 + relevant primitive proof goals; typically it is the first method 1.147 + applied in an instantiation proof. 1.148 1.149 - From now on, the type-checker will consider @{typ int} 1.150 - as a @{class semigroup} automatically, i.e.\ any general results 1.151 - are immediately available on concrete instances. 1.152 + From now on, the type-checker will consider @{typ int} as a @{class 1.153 + semigroup} automatically, i.e.\ any general results are immediately 1.154 + available on concrete instances. 1.155 1.156 - \medskip Another instance of @{class semigroup} yields the natural numbers: 1.157 + \medskip Another instance of @{class semigroup} yields the natural 1.158 + numbers: 1.159 *} 1.160 1.161 instantiation %quote nat :: semigroup 1.162 @@ -177,21 +175,20 @@ 1.163 end %quote 1.164 1.165 text {* 1.166 - \noindent Note the occurence of the name @{text mult_nat} 1.167 - in the primrec declaration; by default, the local name of 1.168 - a class operation @{text f} to be instantiated on type constructor 1.169 - @{text \<kappa>} is mangled as @{text f_\<kappa>}. In case of uncertainty, 1.170 - these names may be inspected using the @{command "print_context"} command 1.171 - or the corresponding ProofGeneral button. 1.172 + \noindent Note the occurence of the name @{text mult_nat} in the 1.173 + primrec declaration; by default, the local name of a class operation 1.174 + @{text f} to be instantiated on type constructor @{text \<kappa>} is 1.175 + mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be 1.176 + inspected using the @{command "print_context"} command or the 1.177 + corresponding ProofGeneral button. 1.178 *} 1.179 1.180 subsection {* Lifting and parametric types *} 1.181 1.182 text {* 1.183 - Overloaded definitions given at a class instantiation 1.184 - may include recursion over the syntactic structure of types. 1.185 - As a canonical example, we model product semigroups 1.186 - using our simple algebra: 1.187 + Overloaded definitions given at a class instantiation may include 1.188 + recursion over the syntactic structure of types. As a canonical 1.189 + example, we model product semigroups using our simple algebra: 1.190 *} 1.191 1.192 instantiation %quote prod :: (semigroup, semigroup) semigroup 1.193 @@ -211,21 +208,19 @@ 1.194 text {* 1.195 \noindent Associativity of product semigroups is established using 1.196 the definition of @{text "(\<otimes>)"} on products and the hypothetical 1.197 - associativity of the type components; these hypotheses 1.198 - are legitimate due to the @{class semigroup} constraints imposed 1.199 - on the type components by the @{command instance} proposition. 1.200 - Indeed, this pattern often occurs with parametric types 1.201 - and type classes. 1.202 + associativity of the type components; these hypotheses are 1.203 + legitimate due to the @{class semigroup} constraints imposed on the 1.204 + type components by the @{command instance} proposition. Indeed, 1.205 + this pattern often occurs with parametric types and type classes. 1.206 *} 1.207 1.208 1.209 subsection {* Subclassing *} 1.210 1.211 text {* 1.212 - We define a subclass @{text monoidl} (a semigroup with a left-hand neutral) 1.213 - by extending @{class semigroup} 1.214 - with one additional parameter @{text neutral} together 1.215 - with its characteristic property: 1.216 + We define a subclass @{text monoidl} (a semigroup with a left-hand 1.217 + neutral) by extending @{class semigroup} with one additional 1.218 + parameter @{text neutral} together with its characteristic property: 1.219 *} 1.220 1.221 class %quote monoidl = semigroup + 1.222 @@ -233,10 +228,10 @@ 1.223 assumes neutl: "\<one> \<otimes> x = x" 1.224 1.225 text {* 1.226 - \noindent Again, we prove some instances, by 1.227 - providing suitable parameter definitions and proofs for the 1.228 - additional specifications. Observe that instantiations 1.229 - for types with the same arity may be simultaneous: 1.230 + \noindent Again, we prove some instances, by providing suitable 1.231 + parameter definitions and proofs for the additional specifications. 1.232 + Observe that instantiations for types with the same arity may be 1.233 + simultaneous: 1.234 *} 1.235 1.236 instantiation %quote nat and int :: monoidl 1.237 @@ -309,8 +304,8 @@ 1.238 end %quote 1.239 1.240 text {* 1.241 - \noindent To finish our small algebra example, we add a @{text group} class 1.242 - with a corresponding instance: 1.243 + \noindent To finish our small algebra example, we add a @{text 1.244 + group} class with a corresponding instance: 1.245 *} 1.246 1.247 class %quote group = monoidl + 1.248 @@ -338,9 +333,9 @@ 1.249 subsection {* A look behind the scenes *} 1.250 1.251 text {* 1.252 - The example above gives an impression how Isar type classes work 1.253 - in practice. As stated in the introduction, classes also provide 1.254 - a link to Isar's locale system. Indeed, the logical core of a class 1.255 + The example above gives an impression how Isar type classes work in 1.256 + practice. As stated in the introduction, classes also provide a 1.257 + link to Isar's locale system. Indeed, the logical core of a class 1.258 is nothing other than a locale: 1.259 *} 1.260 1.261 @@ -402,13 +397,14 @@ 1.262 qed 1.263 1.264 text {* 1.265 - \noindent Here the \qt{@{keyword "in"} @{class group}} target specification 1.266 - indicates that the result is recorded within that context for later 1.267 - use. This local theorem is also lifted to the global one @{fact 1.268 - "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> 1.269 - z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of 1.270 - @{text "group"} before, we may refer to that fact as well: @{prop 1.271 - [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. 1.272 + \noindent Here the \qt{@{keyword "in"} @{class group}} target 1.273 + specification indicates that the result is recorded within that 1.274 + context for later use. This local theorem is also lifted to the 1.275 + global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> 1.276 + \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been 1.277 + made an instance of @{text "group"} before, we may refer to that 1.278 + fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = 1.279 + z"}. 1.280 *} 1.281 1.282 1.283 @@ -424,15 +420,14 @@ 1.284 1.285 text {* 1.286 \noindent If the locale @{text group} is also a class, this local 1.287 - definition is propagated onto a global definition of 1.288 - @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} 1.289 - with corresponding theorems 1.290 + definition is propagated onto a global definition of @{term [source] 1.291 + "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems 1.292 1.293 @{thm pow_nat.simps [no_vars]}. 1.294 1.295 - \noindent As you can see from this example, for local 1.296 - definitions you may use any specification tool 1.297 - which works together with locales, such as Krauss's recursive function package 1.298 + \noindent As you can see from this example, for local definitions 1.299 + you may use any specification tool which works together with 1.300 + locales, such as Krauss's recursive function package 1.301 \cite{krauss2006}. 1.302 *} 1.303 1.304 @@ -440,19 +435,17 @@ 1.305 subsection {* A functor analogy *} 1.306 1.307 text {* 1.308 - We introduced Isar classes by analogy to type classes in 1.309 - functional programming; if we reconsider this in the 1.310 - context of what has been said about type classes and locales, 1.311 - we can drive this analogy further by stating that type 1.312 - classes essentially correspond to functors that have 1.313 - a canonical interpretation as type classes. 1.314 - There is also the possibility of other interpretations. 1.315 - For example, @{text list}s also form a monoid with 1.316 - @{text append} and @{term "[]"} as operations, but it 1.317 - seems inappropriate to apply to lists 1.318 - the same operations as for genuinely algebraic types. 1.319 - In such a case, we can simply make a particular interpretation 1.320 - of monoids for lists: 1.321 + We introduced Isar classes by analogy to type classes in functional 1.322 + programming; if we reconsider this in the context of what has been 1.323 + said about type classes and locales, we can drive this analogy 1.324 + further by stating that type classes essentially correspond to 1.325 + functors that have a canonical interpretation as type classes. 1.326 + There is also the possibility of other interpretations. For 1.327 + example, @{text list}s also form a monoid with @{text append} and 1.328 + @{term "[]"} as operations, but it seems inappropriate to apply to 1.329 + lists the same operations as for genuinely algebraic types. In such 1.330 + a case, we can simply make a particular interpretation of monoids 1.331 + for lists: 1.332 *} 1.333 1.334 interpretation %quote list_monoid: monoid append "[]" 1.335 @@ -510,12 +503,10 @@ 1.336 qed 1.337 1.338 text {* 1.339 - The logical proof is carried out on the locale level. 1.340 - Afterwards it is propagated 1.341 - to the type system, making @{text group} an instance of 1.342 - @{text monoid} by adding an additional edge 1.343 - to the graph of subclass relations 1.344 - (\figref{fig:subclass}). 1.345 + The logical proof is carried out on the locale level. Afterwards it 1.346 + is propagated to the type system, making @{text group} an instance 1.347 + of @{text monoid} by adding an additional edge to the graph of 1.348 + subclass relations (\figref{fig:subclass}). 1.349 1.350 \begin{figure}[htbp] 1.351 \begin{center} 1.352 @@ -547,8 +538,8 @@ 1.353 \end{center} 1.354 \end{figure} 1.355 1.356 - For illustration, a derived definition 1.357 - in @{text group} using @{text pow_nat} 1.358 + For illustration, a derived definition in @{text group} using @{text 1.359 + pow_nat} 1.360 *} 1.361 1.362 definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where 1.363 @@ -557,17 +548,17 @@ 1.364 else (pow_nat (nat (- k)) x)\<div>)" 1.365 1.366 text {* 1.367 - \noindent yields the global definition of 1.368 - @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} 1.369 - with the corresponding theorem @{thm pow_int_def [no_vars]}. 1.370 + \noindent yields the global definition of @{term [source] "pow_int \<Colon> 1.371 + int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm 1.372 + pow_int_def [no_vars]}. 1.373 *} 1.374 1.375 subsection {* A note on syntax *} 1.376 1.377 text {* 1.378 - As a convenience, class context syntax allows references 1.379 - to local class operations and their global counterparts 1.380 - uniformly; type inference resolves ambiguities. For example: 1.381 + As a convenience, class context syntax allows references to local 1.382 + class operations and their global counterparts uniformly; type 1.383 + inference resolves ambiguities. For example: 1.384 *} 1.385 1.386 context %quote semigroup 1.387 @@ -581,11 +572,11 @@ 1.388 term %quote "x \<otimes> y" -- {* example 3 *} 1.389 1.390 text {* 1.391 - \noindent Here in example 1, the term refers to the local class operation 1.392 - @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint 1.393 - enforces the global class operation @{text "mult [nat]"}. 1.394 - In the global context in example 3, the reference is 1.395 - to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}. 1.396 + \noindent Here in example 1, the term refers to the local class 1.397 + operation @{text "mult [\<alpha>]"}, whereas in example 2 the type 1.398 + constraint enforces the global class operation @{text "mult [nat]"}. 1.399 + In the global context in example 3, the reference is to the 1.400 + polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}. 1.401 *} 1.402 1.403 section {* Further issues *} 1.404 @@ -593,16 +584,14 @@ 1.405 subsection {* Type classes and code generation *} 1.406 1.407 text {* 1.408 - Turning back to the first motivation for type classes, 1.409 - namely overloading, it is obvious that overloading 1.410 - stemming from @{command class} statements and 1.411 - @{command instantiation} 1.412 - targets naturally maps to Haskell type classes. 1.413 - The code generator framework \cite{isabelle-codegen} 1.414 - takes this into account. If the target language (e.g.~SML) 1.415 - lacks type classes, then they 1.416 - are implemented by an explicit dictionary construction. 1.417 - As example, let's go back to the power function: 1.418 + Turning back to the first motivation for type classes, namely 1.419 + overloading, it is obvious that overloading stemming from @{command 1.420 + class} statements and @{command instantiation} targets naturally 1.421 + maps to Haskell type classes. The code generator framework 1.422 + \cite{isabelle-codegen} takes this into account. If the target 1.423 + language (e.g.~SML) lacks type classes, then they are implemented by 1.424 + an explicit dictionary construction. As example, let's go back to 1.425 + the power function: 1.426 *} 1.427 1.428 definition %quote example :: int where 1.429 @@ -619,11 +608,18 @@ 1.430 *} 1.431 text %quote {*@{code_stmts example (SML)}*} 1.432 1.433 +text {* 1.434 + \noindent In Scala, implicts are used as dictionaries: 1.435 +*} 1.436 +(*<*)code_include %invisible Scala "Natural" -(*>*) 1.437 +text %quote {*@{code_stmts example (Scala)}*} 1.438 + 1.439 + 1.440 subsection {* Inspecting the type class universe *} 1.441 1.442 text {* 1.443 - To facilitate orientation in complex subclass structures, 1.444 - two diagnostics commands are provided: 1.445 + To facilitate orientation in complex subclass structures, two 1.446 + diagnostics commands are provided: 1.447 1.448 \begin{description} 1.449