
haftmann@20946: theory Classes
haftmann@28565: imports Main Setup
haftmann@20946: begin
haftmann@20946: 
haftmann@20946: section {* Introduction *}
haftmann@20946: 
haftmann@20946: text {*
paulson@31684:   Type classes were introduced by Wadler and Blott \cite{wadler89how}
paulson@31684:   into the Haskell language to allow for a reasonable implementation
haftmann@22317:   of overloading\footnote{throughout this tutorial, we are referring
haftmann@22317:   to classical Haskell 1.0 type classes, not considering
haftmann@22317:   later additions in expressiveness}.
haftmann@22317:   As a canonical example, a polymorphic equality function
haftmann@22317:   @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
haftmann@22550:   types for @{text "\<alpha>"}, which is achieved by splitting introduction
haftmann@22317:   of the @{text eq} function from its overloaded definitions by means
haftmann@22317:   of @{text class} and @{text instance} declarations:
haftmann@30210:   \footnote{syntax here is a kind of isabellized Haskell}
haftmann@20946: 
haftmann@28565:   \begin{quote}
haftmann@20946: 
haftmann@30210:   \noindent@{text "class eq where"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
haftmann@20946: 
haftmann@28565:   \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq 0 0 = True"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq 0 _ = False"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq _ 0 = False"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
haftmann@22317: 
haftmann@28948:   \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
haftmann@22317: 
haftmann@28565:   \medskip\noindent@{text "class ord extends eq where"} \\
haftmann@28565:   \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
haftmann@28565:   \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
haftmann@28565: 
haftmann@28565:   \end{quote}
haftmann@28565: 
haftmann@28565:   \noindent Type variables are annotated with (finitely many) classes;
haftmann@22317:   these annotations are assertions that a particular polymorphic type
haftmann@22317:   provides definitions for overloaded functions.
haftmann@22317: 
haftmann@22317:   Indeed, type classes not only allow for simple overloading
haftmann@22317:   but form a generic calculus, an instance of order-sorted
paulson@31684:   algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
haftmann@22317: 
paulson@31684:   From a software engineering point of view, type classes
haftmann@28540:   roughly correspond to interfaces in object-oriented languages like Java;
haftmann@22317:   so, it is naturally desirable that type classes do not only
haftmann@24991:   provide functions (class parameters) but also state specifications
haftmann@22317:   implementations must obey.  For example, the @{text "class eq"}
haftmann@22550:   above could be given the following specification, demanding that
haftmann@22550:   @{text "class eq"} is an equivalence relation obeying reflexivity,
haftmann@22550:   symmetry and transitivity:
haftmann@22317: 
haftmann@28565:   \begin{quote}
haftmann@22317: 
haftmann@28565:   \noindent@{text "class eq where"} \\
haftmann@28565:   \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
haftmann@28565:   @{text "satisfying"} \\
haftmann@28565:   \hspace*{2ex}@{text "refl: eq x x"} \\
haftmann@28565:   \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
haftmann@28565:   \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
haftmann@28565: 
haftmann@28565:   \end{quote}
haftmann@28565: 
paulson@31684:   \noindent From a theoretical point of view, type classes are lightweight
haftmann@22347:   modules; Haskell type classes may be emulated by
haftmann@22317:   SML functors \cite{classes_modules}. 
haftmann@22317:   Isabelle/Isar offers a discipline of type classes which brings
haftmann@22317:   all those aspects together:
haftmann@22317: 
haftmann@22317:   \begin{enumerate}
haftmann@24991:     \item specifying abstract parameters together with
haftmann@22317:        corresponding specifications,
haftmann@28540:     \item instantiating those abstract parameters by a particular
haftmann@22317:        type
haftmann@22317:     \item in connection with a ``less ad-hoc'' approach to overloading,
paulson@31684:     \item with a direct link to the Isabelle module system:
paulson@31684:       locales \cite{kammueller-locales}.
haftmann@22317:   \end{enumerate}
haftmann@22317: 
haftmann@22550:   \noindent Isar type classes also directly support code generation
paulson@31684:   in a Haskell like fashion. Internally, they are mapped to more primitive 
paulson@31684:   Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
haftmann@22317: 
haftmann@22317:   This tutorial demonstrates common elements of structured specifications
haftmann@22317:   and abstract reasoning with type classes by the algebraic hierarchy of
haftmann@20946:   semigroups, monoids and groups.  Our background theory is that of
haftmann@23956:   Isabelle/HOL \cite{isa-tutorial}, for which some
haftmann@22317:   familiarity is assumed.
haftmann@20946: *}
haftmann@20946: 
haftmann@22317: section {* A simple algebra example \label{sec:example} *}
haftmann@20946: 
haftmann@20946: subsection {* Class definition *}
haftmann@20946: 
haftmann@20946: text {*
haftmann@20946:   Depending on an arbitrary type @{text "\<alpha>"}, class @{text
haftmann@28565:   "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
haftmann@20946:   assumed to be associative:
haftmann@20946: *}
haftmann@20946: 
haftmann@29705: class %quote semigroup =
haftmann@28565:   fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
haftmann@28565:   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
haftmann@20946: 
haftmann@20946: text {*
haftmann@28565:   \noindent This @{command class} specification consists of two
haftmann@28565:   parts: the \qn{operational} part names the class parameter
haftmann@28565:   (@{element "fixes"}), the \qn{logical} part specifies properties on them
haftmann@28565:   (@{element "assumes"}).  The local @{element "fixes"} and
haftmann@28565:   @{element "assumes"} are lifted to the theory toplevel,
haftmann@28565:   yielding the global
haftmann@24991:   parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
haftmann@28565:   global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
haftmann@22479:   z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
haftmann@20946: *}
haftmann@20946: 
haftmann@20946: 
haftmann@20946: subsection {* Class instantiation \label{sec:class_inst} *}
haftmann@20946: 
haftmann@20946: text {*
haftmann@28565:   The concrete type @{typ int} is made a @{class semigroup}
haftmann@24991:   instance by providing a suitable definition for the class parameter
haftmann@28565:   @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
haftmann@28565:   This is accomplished by the @{command instantiation} target:
haftmann@20946: *}
haftmann@20946: 
haftmann@28565: instantiation %quote int :: semigroup
haftmann@28565: begin
haftmann@25533: 
haftmann@28565: definition %quote
haftmann@28565:   mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
haftmann@25533: 
haftmann@28565: instance %quote proof
haftmann@28565:   fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
haftmann@28565:   then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
haftmann@28566:     unfolding mult_int_def .
haftmann@28565: qed
haftmann@20946: 
haftmann@28565: end %quote
haftmann@25533: 
haftmann@20946: text {*
paulson@31684:   \noindent @{command instantiation} defines class parameters
haftmann@25533:   at a particular instance using common specification tools (here,
haftmann@28565:   @{command definition}).  The concluding @{command instance}
haftmann@25533:   opens a proof that the given parameters actually conform
haftmann@25533:   to the class specification.  Note that the first proof step
haftmann@28565:   is the @{method default} method,
haftmann@28565:   which for such instance proofs maps to the @{method intro_classes} method.
paulson@31684:   This reduces an instance judgement to the relevant primitive
paulson@31684:   proof goals; typically it is the first method applied
haftmann@22317:   in an instantiation proof.
haftmann@22317: 
haftmann@28565:   From now on, the type-checker will consider @{typ int}
haftmann@28565:   as a @{class semigroup} automatically, i.e.\ any general results
haftmann@25533:   are immediately available on concrete instances.
haftmann@28565: 
paulson@31684:   \medskip Another instance of @{class semigroup} yields the natural numbers:
haftmann@20946: *}
haftmann@20946: 
haftmann@28565: instantiation %quote nat :: semigroup
haftmann@28565: begin
haftmann@25533: 
haftmann@28565: primrec %quote mult_nat where
haftmann@28565:   "(0\<Colon>nat) \<otimes> n = n"
haftmann@28565:   | "Suc m \<otimes> n = Suc (m \<otimes> n)"
haftmann@25533: 
haftmann@28565: instance %quote proof
haftmann@28565:   fix m n q :: nat 
haftmann@28565:   show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
haftmann@28565:     by (induct m) auto
haftmann@28565: qed
haftmann@20946: 
haftmann@28565: end %quote
haftmann@25247: 
haftmann@25871: text {*
haftmann@25871:   \noindent Note the occurence of the name @{text mult_nat}
haftmann@25871:   in the primrec declaration;  by default, the local name of
haftmann@31675:   a class operation @{text f} to be instantiated on type constructor
haftmann@31675:   @{text \<kappa>} is mangled as @{text f_\<kappa>}.  In case of uncertainty,
haftmann@28565:   these names may be inspected using the @{command "print_context"} command
haftmann@25871:   or the corresponding ProofGeneral button.
haftmann@25871: *}
haftmann@25871: 
haftmann@25247: subsection {* Lifting and parametric types *}
haftmann@25247: 
haftmann@20946: text {*
paulson@31684:   Overloaded definitions given at a class instantiation
haftmann@25247:   may include recursion over the syntactic structure of types.
haftmann@25247:   As a canonical example, we model product semigroups
haftmann@25247:   using our simple algebra:
haftmann@20946: *}
haftmann@20946: 
haftmann@28565: instantiation %quote * :: (semigroup, semigroup) semigroup
haftmann@28565: begin
haftmann@25533: 
haftmann@28565: definition %quote
haftmann@31930:   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)"
haftmann@25533: 
haftmann@28565: instance %quote proof
haftmann@31930:   fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
haftmann@31930:   show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
haftmann@28566:     unfolding mult_prod_def by (simp add: assoc)
haftmann@28565: qed      
haftmann@20946: 
haftmann@28565: end %quote
haftmann@25533: 
haftmann@25247: text {*
haftmann@31675:   \noindent Associativity of product semigroups is established using
haftmann@28565:   the definition of @{text "(\<otimes>)"} on products and the hypothetical
huffman@27505:   associativity of the type components;  these hypotheses
paulson@31684:   are legitimate due to the @{class semigroup} constraints imposed
haftmann@28565:   on the type components by the @{command instance} proposition.
haftmann@25247:   Indeed, this pattern often occurs with parametric types
haftmann@25247:   and type classes.
haftmann@25247: *}
haftmann@20946: 
haftmann@25247: 
haftmann@25247: subsection {* Subclassing *}
haftmann@20946: 
haftmann@20946: text {*
haftmann@28565:   We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
haftmann@28565:   by extending @{class semigroup}
haftmann@28565:   with one additional parameter @{text neutral} together
paulson@31684:   with its characteristic property:
haftmann@20946: *}
haftmann@20946: 
haftmann@28565: class %quote monoidl = semigroup +
haftmann@28565:   fixes neutral :: "\<alpha>" ("\<one>")
haftmann@28565:   assumes neutl: "\<one> \<otimes> x = x"
haftmann@20946: 
haftmann@20946: text {*
haftmann@25247:   \noindent Again, we prove some instances, by
haftmann@24991:   providing suitable parameter definitions and proofs for the
huffman@27505:   additional specifications.  Observe that instantiations
haftmann@25533:   for types with the same arity may be simultaneous:
haftmann@20946: *}
haftmann@20946: 
haftmann@28566: instantiation %quote nat and int :: monoidl
haftmann@28566: begin
haftmann@25533: 
haftmann@28566: definition %quote
haftmann@28566:   neutral_nat_def: "\<one> = (0\<Colon>nat)"
haftmann@25533: 
haftmann@28566: definition %quote
haftmann@28566:   neutral_int_def: "\<one> = (0\<Colon>int)"
haftmann@25533: 
haftmann@28566: instance %quote proof
haftmann@28566:   fix n :: nat
haftmann@28566:   show "\<one> \<otimes> n = n"
haftmann@28566:     unfolding neutral_nat_def by simp
haftmann@28566: next
haftmann@28566:   fix k :: int
haftmann@28566:   show "\<one> \<otimes> k = k"
haftmann@28566:     unfolding neutral_int_def mult_int_def by simp
haftmann@28566: qed
haftmann@20946: 
haftmann@28566: end %quote
haftmann@25533: 
haftmann@28566: instantiation %quote * :: (monoidl, monoidl) monoidl
haftmann@28566: begin
haftmann@25533: 
haftmann@28566: definition %quote
haftmann@28566:   neutral_prod_def: "\<one> = (\<one>, \<one>)"
haftmann@25533: 
haftmann@28566: instance %quote proof
haftmann@28566:   fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
haftmann@28566:   show "\<one> \<otimes> p = p"
haftmann@28566:     unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
haftmann@28566: qed
haftmann@20946: 
haftmann@28566: end %quote
haftmann@25533: 
haftmann@20946: text {*
paulson@31684:   \noindent Fully-fledged monoids are modelled by another subclass,
haftmann@24991:   which does not add new parameters but tightens the specification:
haftmann@20946: *}
haftmann@20946: 
haftmann@28566: class %quote monoid = monoidl +
haftmann@28566:   assumes neutr: "x \<otimes> \<one> = x"
haftmann@20946: 
haftmann@28566: instantiation %quote nat and int :: monoid 
haftmann@28566: begin
haftmann@25533: 
haftmann@28566: instance %quote proof
haftmann@28566:   fix n :: nat
haftmann@28566:   show "n \<otimes> \<one> = n"
haftmann@28566:     unfolding neutral_nat_def by (induct n) simp_all
haftmann@28566: next
haftmann@28566:   fix k :: int
haftmann@28566:   show "k \<otimes> \<one> = k"
haftmann@28566:     unfolding neutral_int_def mult_int_def by simp
haftmann@28566: qed
haftmann@25247: 
haftmann@28566: end %quote
haftmann@25533: 
haftmann@28566: instantiation %quote * :: (monoid, monoid) monoid
haftmann@28566: begin
haftmann@25533: 
haftmann@28566: instance %quote proof 
haftmann@28566:   fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
haftmann@28566:   show "p \<otimes> \<one> = p"
haftmann@28566:     unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
haftmann@28566: qed
haftmann@22317: 
haftmann@28566: end %quote
haftmann@25533: 
haftmann@22317: text {*
haftmann@28565:   \noindent To finish our small algebra example, we add a @{text group} class
haftmann@22317:   with a corresponding instance:
haftmann@22317: *}
haftmann@20946: 
haftmann@28566: class %quote group = monoidl +
haftmann@28566:   fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
haftmann@28566:   assumes invl: "x\<div> \<otimes> x = \<one>"
haftmann@20946: 
haftmann@28566: instantiation %quote int :: group
haftmann@28566: begin
haftmann@25533: 
haftmann@28566: definition %quote
haftmann@28566:   inverse_int_def: "i\<div> = - (i\<Colon>int)"
haftmann@25533: 
haftmann@28566: instance %quote proof
haftmann@28566:   fix i :: int
haftmann@28566:   have "-i + i = 0" by simp
haftmann@28566:   then show "i\<div> \<otimes> i = \<one>"
haftmann@28566:     unfolding mult_int_def neutral_int_def inverse_int_def .
haftmann@28566: qed
haftmann@20946: 
haftmann@28566: end %quote
haftmann@28566: 
haftmann@25533: 
haftmann@22317: section {* Type classes as locales *}
haftmann@22317: 
paulson@31684: subsection {* A look behind the scenes *}
haftmann@22317: 
haftmann@22347: text {*
haftmann@22347:   The example above gives an impression how Isar type classes work
haftmann@22347:   in practice.  As stated in the introduction, classes also provide
haftmann@22347:   a link to Isar's locale system.  Indeed, the logical core of a class
paulson@31684:   is nothing other than a locale:
haftmann@22347: *}
haftmann@22347: 
haftmann@29705: class %quote idem =
haftmann@22347:   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
haftmann@22347:   assumes idem: "f (f x) = f x"
haftmann@22317: 
haftmann@22317: text {*
haftmann@22347:   \noindent essentially introduces the locale
haftmann@30210: *} (*<*)setup %invisible {* Sign.add_path "foo" *}
haftmann@30210: (*>*)
haftmann@28566: locale %quote idem =
haftmann@22347:   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
haftmann@22347:   assumes idem: "f (f x) = f x"
haftmann@22347: 
haftmann@22550: text {* \noindent together with corresponding constant(s): *}
haftmann@22347: 
haftmann@28566: consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
haftmann@22347: 
haftmann@22550: text {*
haftmann@22550:   \noindent The connection to the type system is done by means
haftmann@35282:   of a primitive type class
haftmann@30210: *} (*<*)setup %invisible {* Sign.add_path "foo" *}
haftmann@30210: (*>*)
haftmann@35282: classes %quote idem < type
haftmann@35282: (*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
haftmann@35282: setup %invisible {* Sign.parent_path *}(*>*)
haftmann@22347: 
haftmann@22550: text {* \noindent together with a corresponding interpretation: *}
haftmann@22347: 
haftmann@29513: interpretation %quote idem_class:
wenzelm@29294:   idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
haftmann@35282: (*<*)proof qed (rule idem)(*>*)
haftmann@28565: 
haftmann@22347: text {*
paulson@31684:   \noindent This gives you the full power of the Isabelle module system;
haftmann@22347:   conclusions in locale @{text idem} are implicitly propagated
haftmann@22479:   to class @{text idem}.
haftmann@30210: *} (*<*)setup %invisible {* Sign.parent_path *}
haftmann@30210: (*>*)
haftmann@20946: subsection {* Abstract reasoning *}
haftmann@20946: 
haftmann@20946: text {*
haftmann@22347:   Isabelle locales enable reasoning at a general level, while results
haftmann@20946:   are implicitly transferred to all instances.  For example, we can
haftmann@20946:   now establish the @{text "left_cancel"} lemma for groups, which
haftmann@25247:   states that the function @{text "(x \<otimes>)"} is injective:
haftmann@20946: *}
haftmann@20946: 
haftmann@28566: lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
haftmann@28566: proof
haftmann@28566:   assume "x \<otimes> y = x \<otimes> z"
haftmann@28566:   then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
haftmann@28566:   then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
haftmann@28566:   then show "y = z" using neutl and invl by simp
haftmann@28566: next
haftmann@28566:   assume "y = z"
haftmann@28566:   then show "x \<otimes> y = x \<otimes> z" by simp
haftmann@28566: qed
haftmann@20946: 
haftmann@20946: text {*
haftmann@28565:   \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
haftmann@20946:   indicates that the result is recorded within that context for later
haftmann@28565:   use.  This local theorem is also lifted to the global one @{fact
haftmann@22479:   "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
haftmann@20946:   z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been made an instance of
haftmann@20946:   @{text "group"} before, we may refer to that fact as well: @{prop
haftmann@22479:   [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
haftmann@20946: *}
haftmann@20946: 
haftmann@20946: 
haftmann@23956: subsection {* Derived definitions *}
haftmann@20946: 
haftmann@20946: text {*
haftmann@35282:   Isabelle locales are targets which support local definitions:
haftmann@23956: *}
haftmann@20946: 
haftmann@28566: primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
haftmann@28566:   "pow_nat 0 x = \<one>"
haftmann@28566:   | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
haftmann@23956: 
haftmann@23956: text {*
haftmann@23956:   \noindent If the locale @{text group} is also a class, this local
haftmann@23956:   definition is propagated onto a global definition of
haftmann@23956:   @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
haftmann@23956:   with corresponding theorems
haftmann@23956: 
haftmann@23956:   @{thm pow_nat.simps [no_vars]}.
haftmann@23956: 
haftmann@23956:   \noindent As you can see from this example, for local
haftmann@23956:   definitions you may use any specification tool
paulson@31684:   which works together with locales, such as Krauss's recursive function package
paulson@31684:   \cite{krauss2006}.
haftmann@23956: *}
haftmann@23956: 
haftmann@23956: 
haftmann@25247: subsection {* A functor analogy *}
haftmann@25247: 
haftmann@25247: text {*
paulson@31684:   We introduced Isar classes by analogy to type classes in
haftmann@25247:   functional programming;  if we reconsider this in the
haftmann@25247:   context of what has been said about type classes and locales,
haftmann@25247:   we can drive this analogy further by stating that type
paulson@31684:   classes essentially correspond to functors that have
haftmann@25247:   a canonical interpretation as type classes.
paulson@31684:   There is also the possibility of other interpretations.
paulson@31684:   For example, @{text list}s also form a monoid with
haftmann@28565:   @{text append} and @{term "[]"} as operations, but it
haftmann@25247:   seems inappropriate to apply to lists
huffman@27505:   the same operations as for genuinely algebraic types.
paulson@31684:   In such a case, we can simply make a particular interpretation
haftmann@25247:   of monoids for lists:
haftmann@25247: *}
haftmann@25247: 
wenzelm@30732: interpretation %quote list_monoid: monoid append "[]"
haftmann@28947:   proof qed auto
haftmann@25247: 
haftmann@25247: text {*
haftmann@25247:   \noindent This enables us to apply facts on monoids
haftmann@25247:   to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
haftmann@25247: 
haftmann@25247:   When using this interpretation pattern, it may also
haftmann@25247:   be appropriate to map derived definitions accordingly:
haftmann@25247: *}
haftmann@25247: 
haftmann@28566: primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
haftmann@28566:   "replicate 0 _ = []"
haftmann@28566:   | "replicate (Suc n) xs = xs @ replicate n xs"
haftmann@25247: 
wenzelm@30732: interpretation %quote list_monoid: monoid append "[]" where
haftmann@28566:   "monoid.pow_nat append [] = replicate"
haftmann@28566: proof -
haftmann@29513:   interpret monoid append "[]" ..
haftmann@28566:   show "monoid.pow_nat append [] = replicate"
haftmann@28566:   proof
haftmann@28566:     fix n
haftmann@28566:     show "monoid.pow_nat append [] n = replicate n"
haftmann@28566:       by (induct n) auto
haftmann@28566:   qed
haftmann@28566: qed intro_locales
haftmann@25247: 
haftmann@31249: text {*
haftmann@31249:   \noindent This pattern is also helpful to reuse abstract
haftmann@31249:   specifications on the \emph{same} type.  For example, think of a
haftmann@31249:   class @{text preorder}; for type @{typ nat}, there are at least two
haftmann@31249:   possible instances: the natural order or the order induced by the
haftmann@31249:   divides relation.  But only one of these instances can be used for
haftmann@31249:   @{command instantiation}; using the locale behind the class @{text
haftmann@31249:   preorder}, it is still possible to utilise the same abstract
haftmann@31249:   specification again using @{command interpretation}.
haftmann@31249: *}
haftmann@25247: 
haftmann@24991: subsection {* Additional subclass relations *}
haftmann@22347: 
haftmann@22347: text {*
haftmann@31249:   Any @{text "group"} is also a @{text "monoid"}; this can be made
haftmann@31249:   explicit by claiming an additional subclass relation, together with
haftmann@31249:   a proof of the logical difference:
haftmann@22347: *}
haftmann@22347: 
haftmann@28566: subclass %quote (in group) monoid
haftmann@28947: proof
haftmann@28566:   fix x
haftmann@28566:   from invl have "x\<div> \<otimes> x = \<one>" by simp
haftmann@28566:   with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
haftmann@28566:   with left_cancel show "x \<otimes> \<one> = x" by simp
haftmann@28566: qed
haftmann@23956: 
haftmann@23956: text {*
haftmann@30210:   The logical proof is carried out on the locale level.
haftmann@28947:   Afterwards it is propagated
haftmann@23956:   to the type system, making @{text group} an instance of
haftmann@25247:   @{text monoid} by adding an additional edge
haftmann@25247:   to the graph of subclass relations
paulson@31684:   (\figref{fig:subclass}).
haftmann@25247: 
haftmann@25247:   \begin{figure}[htbp]
haftmann@25247:    \begin{center}
haftmann@25247:      \small
haftmann@25247:      \unitlength 0.6mm
haftmann@25247:      \begin{picture}(40,60)(0,0)
haftmann@25247:        \put(20,60){\makebox(0,0){@{text semigroup}}}
haftmann@25247:        \put(20,40){\makebox(0,0){@{text monoidl}}}
haftmann@25247:        \put(00,20){\makebox(0,0){@{text monoid}}}
haftmann@25247:        \put(40,00){\makebox(0,0){@{text group}}}
haftmann@25247:        \put(20,55){\vector(0,-1){10}}
haftmann@25247:        \put(15,35){\vector(-1,-1){10}}
haftmann@25247:        \put(25,35){\vector(1,-3){10}}
haftmann@25247:      \end{picture}
haftmann@25247:      \hspace{8em}
haftmann@25247:      \begin{picture}(40,60)(0,0)
haftmann@25247:        \put(20,60){\makebox(0,0){@{text semigroup}}}
haftmann@25247:        \put(20,40){\makebox(0,0){@{text monoidl}}}
haftmann@25247:        \put(00,20){\makebox(0,0){@{text monoid}}}
haftmann@25247:        \put(40,00){\makebox(0,0){@{text group}}}
haftmann@25247:        \put(20,55){\vector(0,-1){10}}
haftmann@25247:        \put(15,35){\vector(-1,-1){10}}
haftmann@25247:        \put(05,15){\vector(3,-1){30}}
haftmann@25247:      \end{picture}
haftmann@25247:      \caption{Subclass relationship of monoids and groups:
haftmann@25247:         before and after establishing the relationship
haftmann@30134:         @{text "group \<subseteq> monoid"};  transitive edges are left out.}
haftmann@25247:      \label{fig:subclass}
haftmann@25247:    \end{center}
haftmann@25247:   \end{figure}
haftmann@30210: 
haftmann@25247:   For illustration, a derived definition
paulson@31684:   in @{text group} using @{text pow_nat}
haftmann@23956: *}
haftmann@23956: 
haftmann@28565: definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
haftmann@28565:   "pow_int k x = (if k >= 0
haftmann@28565:     then pow_nat (nat k) x
haftmann@28565:     else (pow_nat (nat (- k)) x)\<div>)"
haftmann@23956: 
haftmann@23956: text {*
haftmann@25247:   \noindent yields the global definition of
haftmann@23956:   @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
haftmann@23956:   with the corresponding theorem @{thm pow_int_def [no_vars]}.
haftmann@24991: *}
haftmann@23956: 
haftmann@25868: subsection {* A note on syntax *}
haftmann@25868: 
haftmann@25868: text {*
paulson@31684:   As a convenience, class context syntax allows references
huffman@27505:   to local class operations and their global counterparts
haftmann@25868:   uniformly;  type inference resolves ambiguities.  For example:
haftmann@25868: *}
haftmann@25868: 
haftmann@28565: context %quote semigroup
haftmann@25868: begin
haftmann@25868: 
haftmann@28565: term %quote "x \<otimes> y" -- {* example 1 *}
haftmann@28565: term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
haftmann@25868: 
haftmann@28566: end  %quote
haftmann@25868: 
haftmann@28565: term %quote "x \<otimes> y" -- {* example 3 *}
haftmann@25868: 
haftmann@25868: text {*
haftmann@25868:   \noindent Here in example 1, the term refers to the local class operation
haftmann@25868:   @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
haftmann@25868:   enforces the global class operation @{text "mult [nat]"}.
haftmann@25868:   In the global context in example 3, the reference is
haftmann@25868:   to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
haftmann@25868: *}
haftmann@22347: 
haftmann@29705: section {* Further issues *}
haftmann@29705: 
haftmann@29705: subsection {* Type classes and code generation *}
haftmann@22317: 
haftmann@22317: text {*
haftmann@22317:   Turning back to the first motivation for type classes,
haftmann@22317:   namely overloading, it is obvious that overloading
haftmann@28565:   stemming from @{command class} statements and
haftmann@28565:   @{command instantiation}
haftmann@25533:   targets naturally maps to Haskell type classes.
haftmann@22317:   The code generator framework \cite{isabelle-codegen} 
paulson@31684:   takes this into account.  If the target language (e.g.~SML)
paulson@31684:   lacks type classes, then they
paulson@31684:   are implemented by an explicit dictionary construction.
haftmann@28540:   As example, let's go back to the power function:
haftmann@22317: *}
haftmann@22317: 
haftmann@28565: definition %quote example :: int where
haftmann@28565:   "example = pow_int 10 (-2)"
haftmann@22317: 
haftmann@22317: text {*
paulson@31684:   \noindent This maps to Haskell as follows:
haftmann@22317: *}
haftmann@22317: 
haftmann@28565: text %quote {*@{code_stmts example (Haskell)}*}
haftmann@22317: 
haftmann@22317: text {*
paulson@31684:   \noindent The code in SML has explicit dictionary passing:
haftmann@22317: *}
haftmann@22317: 
haftmann@28565: text %quote {*@{code_stmts example (SML)}*}
haftmann@20946: 
haftmann@29705: subsection {* Inspecting the type class universe *}
haftmann@29705: 
haftmann@29705: text {*
haftmann@29705:   To facilitate orientation in complex subclass structures,
haftmann@29705:   two diagnostics commands are provided:
haftmann@29705: 
haftmann@29705:   \begin{description}
haftmann@29705: 
haftmann@29705:     \item[@{command "print_classes"}] print a list of all classes
haftmann@29705:       together with associated operations etc.
haftmann@29705: 
haftmann@29705:     \item[@{command "class_deps"}] visualizes the subclass relation
haftmann@29705:       between all classes as a Hasse diagram.
haftmann@29705: 
haftmann@29705:   \end{description}
haftmann@29705: *}
haftmann@29705: 
haftmann@20946: end




