diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Mon Mar 02 16:58:39 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,635 +0,0 @@ -theory Classes -imports Main Setup -begin - -chapter {* Haskell-style classes with Isabelle/Isar *} - -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 \ \ \ \ \ bool"} which is overloaded on different - types for @{text "\"}, which is achieved by splitting introduction - of the @{text eq} function from its overloaded definitions by means - of @{text class} and @{text instance} declarations: - - \begin{quote} - - \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\ - \hspace*{2ex}@{text "eq \ \ \ \ \ bool"} - - \medskip\noindent@{text "instance nat \ 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 (\\eq, \\eq) pair \ eq where"} \\ - \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \ eq y1 y2"} - - \medskip\noindent@{text "class ord extends eq where"} \\ - \hspace*{2ex}@{text "less_eq \ \ \ \ \ bool"} \\ - \hspace*{2ex}@{text "less \ \ \ \ \ 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 \ \ \ \ \ bool"} \\ - @{text "satisfying"} \\ - \hspace*{2ex}@{text "refl: eq x x"} \\ - \hspace*{2ex}@{text "sym: eq x y \ eq x y"} \\ - \hspace*{2ex}@{text "trans: eq x y \ eq y z \ 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 "\"}, class @{text - "semigroup"} introduces a binary operator @{text "(\)"} that is - assumed to be associative: -*} - -class %quote semigroup = - fixes mult :: "\ \ \ \ \" (infixl "\" 70) - assumes assoc: "(x \ y) \ z = x \ (y \ 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 \ \\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 @{typ int} is made a @{class semigroup} - instance by providing a suitable definition for the class parameter - @{text "(\)"} 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 {* - \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\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 {* - \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 \} are mangled as @{text f_\}. 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 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" - -instance %quote proof - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" - show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ 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 "(\)"} 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 :: "\" ("\") - assumes neutl: "\ \ 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: "\ = (0\nat)" - -definition %quote - neutral_int_def: "\ = (0\int)" - -instance %quote proof - fix n :: nat - show "\ \ n = n" - unfolding neutral_nat_def by simp -next - fix k :: int - show "\ \ 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: "\ = (\, \)" - -instance %quote proof - fix p :: "\\monoidl \ \\monoidl" - show "\ \ 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 \ \ = x" - -instantiation %quote nat and int :: monoid -begin - -instance %quote proof - fix n :: nat - show "n \ \ = n" - unfolding neutral_nat_def by (induct n) simp_all -next - fix k :: int - show "k \ \ = k" - unfolding neutral_int_def mult_int_def by simp -qed - -end %quote - -instantiation %quote * :: (monoid, monoid) monoid -begin - -instance %quote proof - fix p :: "\\monoid \ \\monoid" - show "p \ \ = 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 :: "\ \ \" ("(_\
)" [1000] 999) - assumes invl: "x\
\ x = \" - -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 = \" - 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 :: "\ \ \" - assumes idem: "f (f x) = f x" - -text {* - \noindent essentially introduces the locale -*} setup %invisible {* Sign.add_path "foo" *} - -locale %quote idem = - fixes f :: "\ \ \" - assumes idem: "f (f x) = f x" - -text {* \noindent together with corresponding constant(s): *} - -consts %quote f :: "\ \ \" - -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 \ (\\idem) \ \" -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 \)"} 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 {* - \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] "\x y z \ \\group. x \ y = x \ - z \ 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] "\x y z \ int. x \ y = x \ z \ y = z"}. -*} - - -subsection {* Derived definitions *} - -text {* - Isabelle locales support a concept of local definitions - in locales: -*} - -primrec %quote (in monoid) pow_nat :: "nat \ \ \ \" where - "pow_nat 0 x = \" - | "pow_nat (Suc n) x = x \ 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 \ nat \ \\monoid \ \\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 \ \ list \ \ 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\
\ x = \" by simp - with assoc [symmetric] neutl invl have "x\
\ (x \ \) = x\
\ x" by simp - with left_cancel show "x \ \ = x" by simp -qed - -text {* - \noindent 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 \ monoid"}; transitive edges are left out.} - \label{fig:subclass} - \end{center} - \end{figure} -7 - For illustration, a derived definition - in @{text group} which uses @{text 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 {* - \noindent 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 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 \ y" -- {* example 1 *} -term %quote "(x\nat) \ y" -- {* example 2 *} - -end %quote - -term %quote "x \ y" -- {* example 3 *} - -text {* - \noindent Here in example 1, the term refers to the local class operation - @{text "mult [\]"}, 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 [?\ \ 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