doc-src/Classes/Thy/Classes.thy

+theory Classes
+imports Main Setup
+begin
+
+section {* Introduction *}
+
+text {*
+  Type classes were introduces 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}.
+  As a canonical example, a polymorphic equality function
+  @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
+  types for @{text "\<alpha>"}, which is achieved by splitting introduction
+  of the @{text eq} function from its overloaded definitions by means
+  of @{text class} and @{text instance} declarations:
+  \footnote{syntax here is a kind of isabellized Haskell}
+
+  \begin{quote}
+
+  \noindent@{text "class eq where"} \\
+  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+
+  \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
+  \hspace*{2ex}@{text "eq 0 0 = True"} \\
+  \hspace*{2ex}@{text "eq 0 _ = False"} \\
+  \hspace*{2ex}@{text "eq _ 0 = False"} \\
+  \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
+
+  \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+  \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
+
+  \medskip\noindent@{text "class ord extends eq where"} \\
+  \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+  \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+
+  \end{quote}
+
+  \noindent Type variables are annotated with (finitely many) classes;
+  these annotations are assertions that a particular polymorphic type
+  provides definitions for overloaded functions.
+
+  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}.
+
+  From a software engeneering 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
+  implementations must obey.  For example, the @{text "class eq"}
+  above could be given the following specification, demanding that
+  @{text "class eq"} is an equivalence relation obeying reflexivity,
+  symmetry and transitivity:
+
+  \begin{quote}
+
+  \noindent@{text "class eq where"} \\
+  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+  @{text "satisfying"} \\
+  \hspace*{2ex}@{text "refl: eq x x"} \\
+  \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
+  \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
+
+  \end{quote}
+
+  \noindent From a theoretic 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
+  all those aspects together:
+
+  \begin{enumerate}
+    \item specifying abstract parameters together with
+       corresponding specifications,
+    \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}).
+  \end{enumerate}
+
+  \noindent Isar type classes also directly support code generation
+  in a Haskell like fashion.
+
+  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} *}
+
+subsection {* Class definition *}
+
+text {*
+  Depending on an arbitrary type @{text "\<alpha>"}, class @{text
+  "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
+  assumed to be associative:
+*}
+
+class %quote semigroup =
+  fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
+  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+
+text {*
+  \noindent This @{command class} specification consists of two
+  parts: the \qn{operational} part names the class parameter
+  (@{element "fixes"}), the \qn{logical} part specifies properties on them
+  (@{element "assumes"}).  The local @{element "fixes"} and
+  @{element "assumes"} are lifted to the theory toplevel,
+  yielding the global
+  parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
+  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
+  z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+*}
+
+
+subsection {* Class instantiation \label{sec:class_inst} *}
+
+text {*
+  The concrete type @{typ int} is made a @{class semigroup}
+  instance by providing a suitable definition for the class parameter
+  @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
+  This is accomplished by the @{command instantiation} target:
+*}
+
+instantiation %quote int :: semigroup
+begin
+
+definition %quote
+  mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
+
+instance %quote proof
+  fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
+  then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
+    unfolding mult_int_def .
+qed
+
+end %quote
+
+text {*
+  \noindent @{command instantiation} allows to define 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
+  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:
+*}
+
+instantiation %quote nat :: semigroup
+begin
+
+primrec %quote mult_nat where
+  "(0\<Colon>nat) \<otimes> n = n"
+  | "Suc m \<otimes> n = Suc (m \<otimes> n)"
+
+instance %quote proof
+  fix m n q :: nat 
+  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+    by (induct m) auto
+qed
+
+end %quote
+
+text {*
+  \noindent Note the occurence of the name @{text mult_nat}
+  in the primrec declaration;  by default, the local name of
+  a class operation @{text f} to instantiate on type constructor
+  @{text \<kappa>} are mangled as @{text f_\<kappa>}.  In case of uncertainty,
+  these names may be inspected using the @{command "print_context"} command
+  or the corresponding ProofGeneral button.
+*}
+
+subsection {* Lifting and parametric types *}
+
+text {*
+  Overloaded definitions giving on class instantiation
+  may include recursion over the syntactic structure of types.
+  As a canonical example, we model product semigroups
+  using our simple algebra:
+*}
+
+instantiation %quote * :: (semigroup, semigroup) semigroup
+begin
+
+definition %quote
+  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)"
+
+instance %quote proof
+  fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+  show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+    unfolding mult_prod_def by (simp add: assoc)
+qed      
+
+end %quote
+
+text {*
+  \noindent Associativity from product semigroups is
+  established using
+  the definition of @{text "(\<otimes>)"} on products and the hypothetical
+  associativity of the type components;  these hypotheses
+  are facts 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.
+*}
+
+
+subsection {* Subclassing *}
+
+text {*
+  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:
+*}
+
+class %quote monoidl = semigroup +
+  fixes neutral :: "\<alpha>" ("\<one>")
+  assumes neutl: "\<one> \<otimes> x = x"
+
+text {*
+  \noindent Again, we prove some instances, by
+  providing suitable parameter definitions and proofs for the
+  additional specifications.  Observe that instantiations
+  for types with the same arity may be simultaneous:
+*}
+
+instantiation %quote nat and int :: monoidl
+begin
+
+definition %quote
+  neutral_nat_def: "\<one> = (0\<Colon>nat)"
+
+definition %quote
+  neutral_int_def: "\<one> = (0\<Colon>int)"
+
+instance %quote proof
+  fix n :: nat
+  show "\<one> \<otimes> n = n"
+    unfolding neutral_nat_def by simp
+next
+  fix k :: int
+  show "\<one> \<otimes> k = k"
+    unfolding neutral_int_def mult_int_def by simp
+qed
+
+end %quote
+
+instantiation %quote * :: (monoidl, monoidl) monoidl
+begin
+
+definition %quote
+  neutral_prod_def: "\<one> = (\<one>, \<one>)"
+
+instance %quote proof
+  fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
+  show "\<one> \<otimes> p = p"
+    unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
+qed
+
+end %quote
+
+text {*
+  \noindent Fully-fledged monoids are modelled by another subclass
+  which does not add new parameters but tightens the specification:
+*}
+
+class %quote monoid = monoidl +
+  assumes neutr: "x \<otimes> \<one> = x"
+
+instantiation %quote nat and int :: monoid 
+begin
+
+instance %quote proof
+  fix n :: nat
+  show "n \<otimes> \<one> = n"
+    unfolding neutral_nat_def by (induct n) simp_all
+next
+  fix k :: int
+  show "k \<otimes> \<one> = k"
+    unfolding neutral_int_def mult_int_def by simp
+qed
+
+end %quote
+
+instantiation %quote * :: (monoid, monoid) monoid
+begin
+
+instance %quote proof 
+  fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
+  show "p \<otimes> \<one> = p"
+    unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
+qed
+
+end %quote
+
+text {*
+  \noindent To finish our small algebra example, we add a @{text group} class
+  with a corresponding instance:
+*}
+
+class %quote group = monoidl +
+  fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
+  assumes invl: "x\<div> \<otimes> x = \<one>"
+
+instantiation %quote int :: group
+begin
+
+definition %quote
+  inverse_int_def: "i\<div> = - (i\<Colon>int)"
+
+instance %quote proof
+  fix i :: int
+  have "-i + i = 0" by simp
+  then show "i\<div> \<otimes> i = \<one>"
+    unfolding mult_int_def neutral_int_def inverse_int_def .
+qed
+
+end %quote
+
+
+section {* Type classes as locales *}
+
+subsection {* A look behind the scene *}
+
+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:
+*}
+
+class %quote idem =
+  fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
+  assumes idem: "f (f x) = f x"
+
+text {*
+  \noindent essentially introduces the locale
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
+locale %quote idem =
+  fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
+  assumes idem: "f (f x) = f x"
+
+text {* \noindent together with corresponding constant(s): *}
+
+consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
+
+text {*
+  \noindent The connection to the type system is done by means
+  of a primitive axclass
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
+axclass %quote idem < type
+  idem: "f (f x) = f x" (*<*)setup %invisible {* Sign.parent_path *}(*>*)
+
+text {* \noindent together with a corresponding interpretation: *}
+
+interpretation %quote idem_class:
+  idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
+proof qed (rule idem)
+
+text {*
+  \noindent This gives you at hand 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 *}
+(*>*)
+subsection {* Abstract reasoning *}
+
+text {*
+  Isabelle locales enable reasoning at a general level, while results
+  are implicitly transferred to all instances.  For example, we can
+  now establish the @{text "left_cancel"} lemma for groups, which
+  states that the function @{text "(x \<otimes>)"} is injective:
+*}
+
+lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
+proof
+  assume "x \<otimes> y = x \<otimes> z"
+  then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
+  then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
+  then show "y = z" using neutl and invl by simp
+next
+  assume "y = z"
+  then show "x \<otimes> y = x \<otimes> z" by simp
+qed
+
+text {*
+  \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
+  indicates that the result is recorded within that context for later
+  use.  This local theorem is also lifted to the global one @{fact
+  "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
+  z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been made an instance of
+  @{text "group"} before, we may refer to that fact as well: @{prop
+  [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
+*}
+
+
+subsection {* Derived definitions *}
+
+text {*
+  Isabelle locales support a concept of local definitions
+  in locales:
+*}
+
+primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+  "pow_nat 0 x = \<one>"
+  | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+
+text {*
+  \noindent If the locale @{text group} is also a class, this local
+  definition is propagated onto a global definition of
+  @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
+  with corresponding theorems
+
+  @{thm pow_nat.simps [no_vars]}.
+
+  \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}).
+*}
+
+
+subsection {* A functor analogy *}
+
+text {*
+  We introduced Isar classes by analogy to type classes
+  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
+  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
+  @{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
+  of monoids for lists:
+*}
+
+interpretation %quote list_monoid!: monoid append "[]"
+  proof qed auto
+
+text {*
+  \noindent This enables us to apply facts on monoids
+  to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
+
+  When using this interpretation pattern, it may also
+  be appropriate to map derived definitions accordingly:
+*}
+
+primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
+  "replicate 0 _ = []"
+  | "replicate (Suc n) xs = xs @ replicate n xs"
+
+interpretation %quote list_monoid!: monoid append "[]" where
+  "monoid.pow_nat append [] = replicate"
+proof -
+  interpret monoid append "[]" ..
+  show "monoid.pow_nat append [] = replicate"
+  proof
+    fix n
+    show "monoid.pow_nat append [] n = replicate n"
+      by (induct n) auto
+  qed
+qed intro_locales
+
+
+subsection {* Additional subclass relations *}
+
+text {*
+  Any @{text "group"} is also a @{text "monoid"};  this
+  can be made explicit by claiming an additional
+  subclass relation,
+  together with a proof of the logical difference:
+*}
+
+subclass %quote (in group) monoid
+proof
+  fix x
+  from invl have "x\<div> \<otimes> x = \<one>" by simp
+  with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
+  with left_cancel show "x \<otimes> \<one> = x" by simp
+qed
+
+text {*
+  The logical proof is carried out on the locale level.
+  Afterwards it is propagated
+  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}).
+
+  \begin{figure}[htbp]
+   \begin{center}
+     \small
+     \unitlength 0.6mm
+     \begin{picture}(40,60)(0,0)
+       \put(20,60){\makebox(0,0){@{text semigroup}}}
+       \put(20,40){\makebox(0,0){@{text monoidl}}}
+       \put(00,20){\makebox(0,0){@{text monoid}}}
+       \put(40,00){\makebox(0,0){@{text group}}}
+       \put(20,55){\vector(0,-1){10}}
+       \put(15,35){\vector(-1,-1){10}}
+       \put(25,35){\vector(1,-3){10}}
+     \end{picture}
+     \hspace{8em}
+     \begin{picture}(40,60)(0,0)
+       \put(20,60){\makebox(0,0){@{text semigroup}}}
+       \put(20,40){\makebox(0,0){@{text monoidl}}}
+       \put(00,20){\makebox(0,0){@{text monoid}}}
+       \put(40,00){\makebox(0,0){@{text group}}}
+       \put(20,55){\vector(0,-1){10}}
+       \put(15,35){\vector(-1,-1){10}}
+       \put(05,15){\vector(3,-1){30}}
+     \end{picture}
+     \caption{Subclass relationship of monoids and groups:
+        before and after establishing the relationship
+        @{text "group \<subseteq> monoid"};  transitive edges are left out.}
+     \label{fig:subclass}
+   \end{center}
+  \end{figure}
+
+  For illustration, a derived definition
+  in @{text group} which uses @{text pow_nat}:
+*}
+
+definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+  "pow_int k x = (if k >= 0
+    then pow_nat (nat k) x
+    else (pow_nat (nat (- k)) x)\<div>)"
+
+text {*
+  \noindent yields the global definition of
+  @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
+  with the corresponding theorem @{thm pow_int_def [no_vars]}.
+*}
+
+subsection {* A note on syntax *}
+
+text {*
+  As a commodity, class context syntax allows to refer
+  to local class operations and their global counterparts
+  uniformly;  type inference resolves ambiguities.  For example:
+*}
+
+context %quote semigroup
+begin
+
+term %quote "x \<otimes> y" -- {* example 1 *}
+term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
+
+end  %quote
+
+term %quote "x \<otimes> y" -- {* example 3 *}
+
+text {*
+  \noindent Here in example 1, the term refers to the local class operation
+  @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
+  enforces the global class operation @{text "mult [nat]"}.
+  In the global context in example 3, the reference is
+  to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+*}
+
+section {* Further issues *}
+
+subsection {* Type classes and code generation *}
+
+text {*
+  Turning back to the first motivation for type classes,
+  namely overloading, it is obvious that overloading
+  stemming from @{command class} statements and
+  @{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.
+  As example, let's go back to the power function:
+*}
+
+definition %quote example :: int where
+  "example = pow_int 10 (-2)"
+
+text {*
+  \noindent This maps to Haskell as:
+*}
+
+text %quote {*@{code_stmts example (Haskell)}*}
+
+text {*
+  \noindent The whole code in SML with explicit dictionary passing:
+*}
+
+text %quote {*@{code_stmts example (SML)}*}
+
+subsection {* Inspecting the type class universe *}
+
+text {*
+  To facilitate orientation in complex subclass structures,
+  two diagnostics commands are provided:
+
+  \begin{description}
+
+    \item[@{command "print_classes"}] print a list of all classes
+      together with associated operations etc.
+
+    \item[@{command "class_deps"}] visualizes the subclass relation
+      between all classes as a Hasse diagram.
+
+  \end{description}
+*}
+
+end