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.5    into the Haskell language to allow for a reasonable implementation
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.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.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.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.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.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