Quelle  Classes.thy

theory Classes
imports Main Setup
begin

section ‹Introduction›

text ‹
 Type classes were introduced 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 ‹eq :: α ==> α ==> bool› which is overloaded on
 different types for ‹α›, which is achieved by splitting
 introduction of the ‹eq› function from its overloaded
 definitions by means of ‹class› and ‹instance›
 declarations: \footnote{syntax here is a kind of isabellized
 Haskell}

 \begin{quote}

 🪙 ‹class eq where› \\
 \hspace*{2ex}‹eq :: α ==> α ==> bool›

 🪙🪙 ‹instance nat :: eq where› \\
 \hspace*{2ex}‹eq 0 0 = True› \\
 \hspace*{2ex}‹eq 0 _ = False› \\
 \hspace*{2ex}‹eq _ 0 = False› \\
 \hspace*{2ex}‹eq (Suc n) (Suc m) = eq n m›

 🪙🪙 ‹instance (α::eq, β::eq) pair :: eq where› \\
 \hspace*{2ex}‹eq (x1, y1) (x2, y2) = eq x1 x2 ∧ eq y1 y2›

 🪙🪙 ‹class ord extends eq where› \\
 \hspace*{2ex}‹less_eq :: α ==> α ==> bool› \\
 \hspace*{2ex}‹less :: α ==> α ==> bool›

 \end{quote}

 🪙 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-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"›.

 From a software engineering 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 ‹class eq›
 above could be given the following specification, demanding that
 ‹class eq› is an equivalence relation obeying reflexivity,
 symmetry and transitivity:

 \begin{quote}

 🪙 ‹class eq where› \\
 \hspace*{2ex}‹eq :: α ==> α ==> bool› \\
 ‹satisfying› \\
 \hspace*{2ex}‹refl: eq x x› \\
 \hspace*{2ex}‹sym: eq x y ⟷ eq x y› \\
 \hspace*{2ex}‹trans: eq x y ∧ eq y z ⟶ eq x z›

 \end{quote}

 🪙 From a theoretical 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:
 locales cite‹"kammueller-locales"›.
 \end{enumerate}

 🪙 Isar type classes also directly support code generation in
 a Haskell like fashion. Internally, they are mapped to more
 primitive Isabelle concepts cite‹"Haftmann-Wenzel:2006:classes"›.

 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.
 ›

section ‹A simple algebra example \label{sec:example}›

subsection ‹Class definition›

text ‹
 Depending on an arbitrary type ‹α›, class ‹semigroup› introduces a binary operator ‹(⊗)› that is
 assumed to be associative:
 ›

class %quote semigroup =
  fixes mult :: ‹α ==> α ==> α›   (infixl ‹⊗› 70)
  assumes assoc: ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›

text ‹
 🪙 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 :: α::semigroup ==> α ==> α›} and the
 global theorem @{fact "semigroup.assoc:"}~@{prop [source] ‹∧x y z ::
 α::semigroup. (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›}.
 ›


subsection ‹Class instantiation \label{sec:class_inst}›

text ‹
 The concrete type 🍋‹int› is made a 🍋‹semigroup› instance
 by providing a suitable definition for the class parameter ‹(⊗)› 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 ⊗ j = i + (j::int)›

instance %quote proof
  fix i j k :: int have ‹(i + j) + k = i + (j + k)› by simp
  then show ‹(i ⊗ j) ⊗ k = i ⊗ (j ⊗ k)›
    unfolding mult_int_def .
qed

end %quote

text ‹
 🪙 @{command instantiation} defines 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
 standard} method, which for such instance proofs maps to the @{method
 intro_classes} method. This reduces an instance judgement to the
 relevant primitive proof goals; typically it is the first method
 applied in an instantiation proof.

 From now on, the type-checker will consider 🍋‹int› as a 🍋‹semigroup› automatically, i.e.\ any general results are immediately
 available on concrete instances.

 🪙 Another instance of 🍋‹semigroup› yields the natural
 numbers:
 ›

instantiation %quote nat :: semigroup
begin

primrec %quote mult_nat where
  ‹(0::nat) ⊗ n = n›
  | ‹Suc m ⊗ n = Suc (m ⊗ n)›

instance %quote proof
  fix m n q :: nat 
  show ‹m ⊗ n ⊗ q = m ⊗ (n ⊗ q)›
    by (induct m) auto
qed

end %quote

text ‹
 🪙 Note the occurrence of the name ‹mult_nat› in the
 primrec declaration; by default, the local name of a class operation
 ‹f› to be instantiated on type constructor ‹κ› is
 mangled as ‹f_κ›. In case of uncertainty, these names may be
 inspected using the @{command "print_context"} command.
 ›

subsection ‹Lifting and parametric types›

text ‹
 Overloaded definitions given at a 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 prod :: (semigroup, semigroup) semigroup
begin

definition %quote
  mult_prod_def: ‹p₁ ⊗ p₂ = (fst p₁ ⊗ fst p₂, snd p₁ ⊗ snd p₂)›

instance %quote proof
  fix p₁ p₂ p₃ :: ‹α::semigroup × β::semigroup›
  show ‹p₁ ⊗ p₂ ⊗ p₃ = p₁ ⊗ (p₂ ⊗ p₃)›
    unfolding mult_prod_def by (simp add: assoc)
qed      

end %quote

text ‹
 🪙 Associativity of product semigroups is established using
 the definition of ‹(⊗)› on products and the hypothetical
 associativity of the type components; these hypotheses are
 legitimate due to the 🍋‹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 ‹monoidl› (a semigroup with a left-hand
 neutral) by extending 🍋‹semigroup› with one additional
 parameter ‹neutral› together with its characteristic property:
 ›

class %quote monoidl = semigroup +
  fixes neutral :: ‹α› (‹1›)
  assumes neutl: ‹1 ⊗ x = x›

text ‹
 🪙 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: ‹1 = (0::nat)›

definition %quote
  neutral_int_def: ‹1 = (0::int)›

instance %quote proof
  fix n :: nat
  show ‹1 ⊗ n = n›
    unfolding neutral_nat_def by simp
next
  fix k :: int
  show ‹1 ⊗ k = k›
    unfolding neutral_int_def mult_int_def by simp
qed

end %quote

instantiation %quote prod :: (monoidl, monoidl) monoidl
begin

definition %quote
  neutral_prod_def: ‹1 = (1, 1)›

instance %quote proof
  fix p :: ‹α::monoidl × β::monoidl›
  show ‹1 ⊗ p = p›
    unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
qed

end %quote

text ‹
 🪙 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 ⊗ 1 = x›

instantiation %quote nat and int :: monoid 
begin

instance %quote proof
  fix n :: nat
  show ‹n ⊗ 1 = n›
    unfolding neutral_nat_def by (induct n) simp_all
next
  fix k :: int
  show ‹k ⊗ 1 = k›
    unfolding neutral_int_def mult_int_def by simp
qed

end %quote

instantiation %quote prod :: (monoid, monoid) monoid
begin

instance %quote proof 
  fix p :: ‹α::monoid × β::monoid›
  show ‹p ⊗ 1 = p›
    unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
qed

end %quote

text ‹
 🪙 To finish our small algebra example, we add a ‹group› class with a corresponding instance:
 ›

class %quote group = monoidl +
  fixes inverse :: ‹α ==> α›    (‹(_÷)› [1000] 999)
  assumes invl: ‹x÷ ⊗ x = 1›

instantiation %quote int :: group
begin

definition %quote
  inverse_int_def: ‹i÷ = - (i::int)›

instance %quote proof
  fix i :: int
  have ‹-i + i = 0› by simp
  then show ‹i÷ ⊗ i = 1›
    unfolding mult_int_def neutral_int_def inverse_int_def .
qed

end %quote


section ‹Type classes as locales›

subsection ‹A look behind the scenes›

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 other than a locale:
 ›

class %quote idem =
  fixes f :: ‹α ==> α›
  assumes idem: ‹f (f x) = f x›

text ‹
 🪙 essentially introduces the locale
 › (*<*)setup %invisible \<open>Sign.add_path "foo"\<close>
(*>*)
locale %quote idem =
  fixes f :: ‹α ==> α›
  assumes idem: ‹f (f x) = f x›

text ‹🪙 together with corresponding constant(s):›

consts %quote f :: ‹α ==> α›

text ‹
 🪙 The connection to the type system is done by means of a
 primitive type class ‹idem›, together with a corresponding
 interpretation:
 ›

interpretation %quote idem_class:
  idem ‹f :: (α::idem) ==> α›
(*<*)sorry(*>*)

text ‹
 🪙 This gives you the full power of the Isabelle module system;
 conclusions in locale ‹idem› are implicitly propagated
 to class ‹idem›.
\<close> (*<*)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 ‹left_cancel› lemma for groups, which
 states that the function ‹(x ⊗)› is injective:
 ›

lemma %quote (in group) left_cancel: ‹x ⊗ y = x ⊗ z ⟷ y = z›
proof
  assume ‹x ⊗ y = x ⊗ z›
  then have ‹x÷ ⊗ (x ⊗ y) = x÷ ⊗ (x ⊗ z)› by simp
  then have ‹(x÷ ⊗ x) ⊗ y = (x÷ ⊗ x) ⊗ z› using assoc by simp
  then show ‹y = z› using neutl and invl by simp
next
  assume ‹y = z›
  then show ‹x ⊗ y = x ⊗ z› by simp
qed

text ‹
 🪙 Here the \qt{@{keyword "in"} 🍋‹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] ‹∧x y z ::
 α::group. x ⊗ y = x ⊗ z ⟷ y = z›}. Since type ‹int› has been
 made an instance of ‹group› before, we may refer to that
 fact as well: @{prop [source] ‹∧x y z :: int. x ⊗ y = x ⊗ z ⟷ y =
 z›}.
 ›


subsection ‹Derived definitions›

text ‹
 Isabelle locales are targets which support local definitions:
 ›

primrec %quote (in monoid) pow_nat :: ‹nat ==> α ==> α› where
  ‹pow_nat 0 x = 1›
  | ‹pow_nat (Suc n) x = x ⊗ pow_nat n x›

text ‹
 🪙 If the locale ‹group› is also a class, this local
 definition is propagated onto a global definition of @{term [source]
 ‹pow_nat :: nat ==> α::monoid ==> α::monoid›} with corresponding theorems

 @{thm pow_nat.simps [no_vars]}.

 🪙 As you can see from this example, for local definitions
 you may use any specification tool which works together with
 locales, such as Krauss's recursive function package
 cite‹krauss2006›.
 ›


subsection ‹A functor analogy›

text ‹
 We introduced Isar classes by analogy to type classes in 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 that have a canonical interpretation as type classes.
 There is also the possibility of other interpretations. For
 example, ‹list›s also form a monoid with ‹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 can simply make a particular interpretation of monoids
 for lists:
 ›

interpretation %quote list_monoid: monoid append ‹[]›
  proof qed auto

text ‹
 🪙 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 ==> α list ==> α list› where
  ‹replicate 0 _ = []›
  | ‹replicate (Suc n) xs = xs @ replicate n xs›

interpretation %quote list_monoid: monoid append ‹[]› rewrites
  ‹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

text ‹
 🪙 This pattern is also helpful to reuse abstract
 specifications on the \emph{same} type. For example, think of a
 class ‹preorder›; for type 🍋‹nat›, there are at least two
 possible instances: the natural order or the order induced by the
 divides relation. But only one of these instances can be used for
 @{command instantiation}; using the locale behind the class ‹preorder›, it is still possible to utilise the same abstract
 specification again using @{command interpretation}.
 ›

subsection ‹Additional subclass relations›

text ‹
 Any ‹group› is also a ‹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÷ ⊗ x = 1› by simp
  with assoc [symmetric] neutl invl have ‹x÷ ⊗ (x ⊗ 1) = x÷ ⊗ x› by simp
  with left_cancel show ‹x ⊗ 1 = x› by simp
qed

text ‹
 The logical proof is carried out on the locale level. Afterwards it
 is propagated to the type system, making ‹group› an instance
 of ‹monoid› by adding an additional edge to the graph of
 subclass relations (\figref{fig:subclass}).

 \begin{figure}[htbp]
 \begin{center}
 \small
 \unitlength 0.6mm
 \begin{picture}(40,60)(0,0)
 \put(20,60){\makebox(0,0){‹semigroup›}}
 \put(20,40){\makebox(0,0){‹monoidl›}}
 \put(00,20){\makebox(0,0){‹monoid›}}
 \put(40,00){\makebox(0,0){‹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){‹semigroup›}}
 \put(20,40){\makebox(0,0){‹monoidl›}}
 \put(00,20){\makebox(0,0){‹monoid›}}
 \put(40,00){\makebox(0,0){‹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
 ‹group ⊆ monoid›; transitive edges are left out.}
 \label{fig:subclass}
 \end{center}
 \end{figure}

 For illustration, a derived definition in ‹group› using ‹pow_nat›
 ›

definition %quote (in group) pow_int :: ‹int ==> α ==> α› where
  ‹pow_int k x = (if k ≥ 0
 then pow_nat (nat k) x
 else (pow_nat (nat (- k)) x)÷)›

text ‹
 🪙 yields the global definition of @{term [source] ‹pow_int ::
 int ==> α::group ==> α::group›} with the corresponding theorem @{thm
 pow_int_def [no_vars]}.
 ›

subsection ‹A note on syntax›

text ‹
 As a convenience, class context syntax allows references to local
 class operations and their global counterparts uniformly; type
 inference resolves ambiguities. For example:
 ›

context %quote semigroup
begin

term %quote ‹x ⊗ y› ― ‹example 1›
term %quote ‹(x::nat) ⊗ y› ― ‹example 2›

end  %quote

term %quote ‹x ⊗ y› ― ‹example 3›

text ‹
 🪙 Here in example 1, the term refers to the local class
 operation ‹mult [α]›, whereas in example 2 the type
 constraint enforces the global class operation ‹mult [nat]›.
 In the global context in example 3, the reference is to the
 polymorphic global class operation ‹mult [?α :: 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. If the target
 language (e.g.~SML) lacks type classes, then they are implemented by
 an explicit dictionary construction. As example, let's go back to
 the power function:
 ›

definition %quote example :: int where
  ‹example = pow_int 10 (-2)›

text ‹
 🪙 This maps to Haskell as follows:
 ›
text %quote ‹
 @{code_stmts example (Haskell)}
 ›

text ‹
 🪙 The code in SML has explicit dictionary passing:
 ›
text %quote ‹
 @{code_stmts example (SML)}
 ›


text ‹
 🪙 In Scala, implicits are used as dictionaries:
 ›
text %quote ‹
 @{code_stmts example (Scala)}
 ›


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. An optional first sort argument
 constrains the set of classes to all subclasses of this sort,
 an optional second sort argument to all superclasses of this sort.

 \end{description}
 ›

end