)" [1000] 999) assumes invl: "x\<^loc>\

\<^loc>\ x = \<^loc>\" instance int :: group - "i\

\ - i" + inverse_int_def: "i\

\ - i" proof fix i :: int have "-i + i = 0" by simp then show "i\

\ i = \" unfolding mult_int_def and neutral_int_def and inverse_int_def . qed +section {* Type classes as locales *} + +subsection {* A look behind the scene *} + +(* write here: locale *) + +text {* + +*} subsection {* Abstract reasoning *} @@ -305,8 +368,61 @@ text {* *}*) +section {* Further issues *} -subsection {* Additional subclass relations *} +subsection {* Code generation *} + +text {* + Turning back to the first motivation for type classes, + namely overloading, it is obvious that overloading + stemming from @{text "\"} and @{text "\"} + statements 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, the natural power function on groups: +*} + + fun + pow_nat :: "nat \ 'a\monoidl \ 'a\monoidl" where + "pow_nat 0 x = \" + "pow_nat (Suc n) x = x \ pow_nat n x" + + definition + pow_int :: "int \ 'a\group \ 'a\group" where + "pow_int k x = (if k >= 0 + then pow_nat (nat k) x + else (pow_nat (nat (- k)) x)\

)" + + definition + example :: int where + "example = pow_int 10 (-2)" + +text {* + \noindent This maps to Haskell as: +*} + +code_gen example (Haskell "code_examples/") + (* NOTE: you may use Haskell only once in this document, otherwise + you have to work in distinct subdirectories *) + +text {* + \lsthaskell{Thy/code_examples/Classes.hs} + + \noindent (we have left out all other modules). + + \noindent The whole code in SML with explicit dictionary passing: +*} + +code_gen example (*<*)(SML #)(*>*)(SML "code_examples/classes.ML") + +text {* + \lstsml{Thy/code_examples/classes.ML} +*} + + +(* subsection {* Additional subclass relations *} text {* Any @{text "group"} is also a @{text "monoid"}; this @@ -320,54 +436,15 @@ from invl have "x\<^loc>\

\<^loc>\ x = \<^loc>\" by simp with assoc [symmetric] neutl invl have "x\<^loc>\

\<^loc>\ (x \<^loc>\ \<^loc>\) = x\<^loc>\

\<^loc>\ x" by simp with left_cancel show "x \<^loc>\ \<^loc>\ = x" by simp - qed + qed *) - -(* subsection {* Same logical content -- different syntax *} +(* subsection {* Different syntax for same specifications *} text {* +(* subsection {* Syntactic classes *} +*) + *} *) - -section {* Code generation *} - -text {* - Code generation takes account of type classes, - resulting either in Haskell type classes or SML dictionaries. - As example, we define the natural power function on groups: -*} - - function - pow_nat :: "nat \ 'a\monoidl \ 'a\monoidl" where - "pow_nat 0 x = \" - "pow_nat (Suc n) x = x \ pow_nat n x" - by pat_completeness auto - termination pow_nat by (auto_term "measure fst") - declare pow_nat.simps [code func] - - definition - pow_int :: "int \ 'a\group \ 'a\group" - "pow_int k x = (if k >= 0 - then pow_nat (nat k) x - else (pow_nat (nat (- k)) x)\

)" - - definition - example :: int - "example = pow_int 10 (-2)" - -text {* - \noindent Now we generate and compile code for SML: -*} - - code_gen example (SML -) - -text {* - \noindent The result is as expected: -*} - - ML {* - if ROOT.Classes.example = ~20 then () else error "Wrong result" - *} - end diff -r f662831459de -r b550d2c6ca90 doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Wed Feb 14 10:06:13 2007 +0100 @@ -0,0 +1,51 @@ +module Classes where { + +import Nat; +import Integer; + +class Semigroup a where { + mult :: a -> a -> a; +}; + +class (Semigroup a) => Monoidl a where { + neutral :: a; +}; + +class (Monoidl a) => Group a where { + inverse :: a -> a; +}; + +inverse_int :: Integer -> Integer; +inverse_int i = negate i; + +neutral_int :: Integer; +neutral_int = 0; + +mult_int :: Integer -> Integer -> Integer; +mult_int i j = i + j; + +instance Semigroup Integer where { + mult = mult_int; +}; + +instance Monoidl Integer where { + neutral = neutral_int; +}; + +instance Group Integer where { + inverse = inverse_int; +}; + +pow_nat :: (Monoidl a) => Nat -> a -> a; +pow_nat (Suc n) x = mult x (pow_nat n x); +pow_nat Zero_nat x = neutral; + +pow_int :: (Group a) => Integer -> a -> a; +pow_int k x = + (if 0 <= k then pow_nat (nat k) x + else inverse (pow_nat (nat (negate k)) x)); + +example :: Integer; +example = pow_int 10 (-2); + +} diff -r f662831459de -r b550d2c6ca90 doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Wed Feb 14 10:06:13 2007 +0100 @@ -0,0 +1,75 @@ +structure ROOT = +struct + +structure Nat = +struct + +datatype nat = Zero_nat | Suc of nat; + +end; (*struct Nat*) + +structure Integer = +struct + +fun nat_aux n i = + (if IntInf.<= (i, (0 : IntInf.int)) then n + else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int)))); + +fun nat i = nat_aux Nat.Zero_nat i; + +fun op_eq_bit false false = true + | op_eq_bit true true = true + | op_eq_bit false true = false + | op_eq_bit true false = false; + +end; (*struct Integer*) + +structure Classes = +struct + +type 'a semigroup = {Classes__mult : 'a -> 'a -> 'a}; +fun mult (A_:'a semigroup) = #Classes__mult A_; + +type 'a monoidl = + {Classes__monoidl_semigroup : 'a semigroup, Classes__neutral : 'a}; +fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_; +fun neutral (A_:'a monoidl) = #Classes__neutral A_; + +type 'a group = + {Classes__group_monoidl : 'a monoidl, Classes__inverse : 'a -> 'a}; +fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_; +fun inverse (A_:'a group) = #Classes__inverse A_; + +fun inverse_int i = IntInf.~ i; + +val neutral_int : IntInf.int = (0 : IntInf.int); + +fun mult_int i j = IntInf.+ (i, j); + +val semigroup_int = {Classes__mult = mult_int} : IntInf.int semigroup; + +val monoidl_int = + {Classes__monoidl_semigroup = semigroup_int, + Classes__neutral = neutral_int} + : IntInf.int monoidl; + +val group_int = + {Classes__group_monoidl = monoidl_int, Classes__inverse = inverse_int} : + IntInf.int group; + +fun pow_nat A_ (Nat.Suc n) x = + mult (monoidl_semigroup A_) x (pow_nat A_ n x) + | pow_nat A_ Nat.Zero_nat x = neutral A_; + +fun pow_int A_ k x = + (if IntInf.<= ((0 : IntInf.int), k) + then pow_nat (group_monoidl A_) (Integer.nat k) x + else inverse A_ + (pow_nat (group_monoidl A_) (Integer.nat (IntInf.~ k)) x)); + +val example : IntInf.int = + pow_int group_int (10 : IntInf.int) (~2 : IntInf.int); + +end; (*struct Classes*) + +end; (*struct ROOT*) diff -r f662831459de -r b550d2c6ca90 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Feb 14 10:06:12 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Feb 14 10:06:13 2007 +0100 @@ -13,16 +13,34 @@ \isacommand{theory}\isamarkupfalse% \ Classes\isanewline \isakeyword{imports}\ Main\isanewline -\isakeyword{begin}\isanewline -% +\isakeyword{begin}% \endisatagtheory {\isafoldtheory}% % \isadelimtheory +\isanewline % \endisadelimtheory % \isadelimML +\isanewline +% +\endisadelimML +% +\isatagML +\isacommand{ML}\isamarkupfalse% +\ {\isacharverbatimopen}\isanewline +CodegenSerializer{\isachardot}code{\isacharunderscore}width\ {\isacharcolon}{\isacharequal}\ {\isadigit{7}}{\isadigit{4}}{\isacharsemicolon}\isanewline +{\isacharverbatimclose}\isanewline +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimML % \endisadelimML % @@ -44,18 +62,82 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The well-known concept of type classes - \cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997} - offers a useful structuring mechanism for programs and proofs, which - is more light-weight than a fully featured module mechanism. Type - classes are able to qualify types by associating operations and - logical properties. For example, class \isa{eq} could provide - an equivalence relation \isa{{\isacharequal}} on type \isa{{\isasymalpha}}, and class - \isa{ord} could extend \isa{eq} by providing a strict order - \isa{{\isacharless}} etc. +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 + \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different + types for \isa{{\isasymalpha}}, which is achieves by splitting introduction + of the \isa{eq} function from its overloaded definitions by means + of \isa{class} and \isa{instance} declarations: + + \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\ + \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} + + \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\ + \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\ + \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\ + \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\ + \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m} + + \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\ + \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isacharampersand}{\isacharampersand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}} + + \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\ + \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ + \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} + + \medskip Type variables are annotated with (finitly 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:1993,Wenzel:1997}. - Isabelle/Isar offers Haskell-style type classes, combining operational - and logical specifications.% + From a software enigineering point of view, type classes + correspond to interfaces in object-oriented languages like Java; + so, it is naturally desirable that type classes do not only + provide functions (class operations) but also state specifications + implementations must obey. For example, the \isa{class\ eq} + above could be given the following specification: + + \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\ + \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ + \hspace*{2ex}\isa{satisfying} \\ + \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\ + \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\ + \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z} + + \medskip From a theoretic point of view, type classes are leightweight + modules; indeed, 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 operations togehter with + corresponding specifications, + \item instantating those abstract operations 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). + \end{enumerate} + + Isar type classes also directly support code generation + in as 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{Nipkow-et-al:2002: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_wenzel2006classes} for more detail.% \end{isamarkuptext}% \isamarkuptrue% % @@ -63,28 +145,6 @@ } \isamarkuptrue% % -\begin{isamarkuptext}% -We demonstrate 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{Nipkow-et-al:2002:tutorial}, which uses fairly - standard notation from mathematics and functional programming. We - also refer to basic vernacular commands for definitions and - statements, e.g.\ \isa{{\isasymDEFINITION}} and \isa{{\isasymLEMMA}}; - proofs will be recorded using structured elements of Isabelle/Isar - \cite{Wenzel-PhD,Nipkow:2002}, notably \isa{{\isasymPROOF}}/\isa{{\isasymQED}} and \isa{{\isasymFIX}}/\isa{{\isasymASSUME}}/\isa{{\isasymSHOW}}. - - Our main concern are the new \isa{{\isasymCLASS}} - and \isa{{\isasymINSTANCE}} elements used below. - Here we merely present the - look-and-feel for end users, which is quite similar to Haskell's - \texttt{class} and \texttt{instance} \cite{hall96type}, but - augmented by logical specifications and proofs; - Internally, those are mapped to more primitive Isabelle concepts. - See \cite{haftmann_wenzel2006classes} for more detail.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsubsection{Class definition% } \isamarkuptrue% @@ -119,7 +179,7 @@ \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline -\ \ \ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -128,11 +188,11 @@ \isatagproof \isacommand{proof}\isamarkupfalse% \isanewline -\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% @@ -151,12 +211,18 @@ as a \isa{semigroup} automatically, i.e.\ any general results are immediately available on concrete instances. + Note that the first proof step is the \isa{default} method, + which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method. + This boils down an instantiation judgement to the relevant primitive + proof goals and should conveniently always be the first method applied + in an instantiation proof. + Another instance of \isa{semigroup} are the natural numbers:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -169,7 +235,7 @@ \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% -\ semigroup{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% % @@ -187,7 +253,7 @@ \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -203,7 +269,7 @@ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% -\ semigroup{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% +\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse% @@ -225,7 +291,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -We define a subclass \isa{monoidl} (a semigroup with an left-hand neutral) +We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral) by extending \isa{semigroup} with one additional operation \isa{neutral} together with its property:% @@ -243,7 +309,7 @@ \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% \ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -270,7 +336,7 @@ \isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% \ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -297,7 +363,7 @@ \isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -337,16 +403,20 @@ \endisadelimproof % \begin{isamarkuptext}% -To finish our small algebra example, we add \isa{monoid} - and \isa{group} classes with corresponding instances% +\noindent Fully-fledged monoids are modelled by another subclass + which does not add new operations but tightens the specification:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{class}\isamarkupfalse% \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline -\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\isanewline +\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent Instantiations may also be given simultaneously for different + type constructors:% +\end{isamarkuptext}% +\isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline % \isadelimproof \ \ \ \ % @@ -361,25 +431,7 @@ \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\ \ \ \ \isacommand{instance}\isamarkupfalse% -\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline -% -\isadelimproof -\ \ \ \ % -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% +\ \ \ \ \isacommand{next}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline @@ -387,25 +439,7 @@ \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\ \ \ \ \isacommand{instance}\isamarkupfalse% -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline -% -\isadelimproof -\ \ \ \ % -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% +\ \ \ \ \isacommand{next}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline @@ -434,10 +468,14 @@ {\isafoldproof}% % \isadelimproof -\ \ \isanewline % \endisadelimproof -\isanewline +% +\begin{isamarkuptext}% +\noindent To finish our small algebra example, we add a \isa{group} class + with a corresponding instance:% +\end{isamarkuptext}% +\isamarkuptrue% \ \ \ \ \isacommand{class}\isamarkupfalse% \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline \ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline @@ -445,7 +483,7 @@ \isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -473,6 +511,19 @@ % \endisadelimproof % +\isamarkupsection{Type classes as locales% +} +\isamarkuptrue% +% +\isamarkupsubsection{A look behind the scene% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Abstract reasoning% } \isamarkuptrue% @@ -535,139 +586,65 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Additional subclass relations% +\isamarkupsection{Further issues% } \isamarkuptrue% % -\begin{isamarkuptext}% -Any \isa{group} is also a \isa{monoid}; this - can be made explicit by claiming an additional subclass relation, - together with a proof of the logical difference:% -\end{isamarkuptext}% -\isamarkuptrue% -\ \ \ \ \isacommand{instance}\isamarkupfalse% -\ group\ {\isacharless}\ monoid\isanewline -% -\isadelimproof -\ \ \ \ % -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ x\isanewline -\ \ \ \ \ \ \isacommand{from}\isamarkupfalse% -\ invl\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\isamarkupsection{Code generation% +\isamarkupsubsection{Code generation% } \isamarkuptrue% % \begin{isamarkuptext}% -Code generation takes account of type classes, - resulting either in Haskell type classes or SML dictionaries. - As example, we define the natural power function on groups:% +Turning back to the first motivation for type classes, + namely overloading, it is obvious that overloading + stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}} + statements 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, the natural power function on groups:% \end{isamarkuptext}% \isamarkuptrue% -\ \ \ \ \isacommand{function}\isamarkupfalse% +\ \ \ \ \isacommand{fun}\isamarkupfalse% \isanewline \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline -% -\isadelimproof -\ \ \ \ \ \ % -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ pat{\isacharunderscore}completeness\ auto% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\ \ \ \ \isacommand{termination}\isamarkupfalse% -\ pow{\isacharunderscore}nat% -\isadelimproof -\ % -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ fst{\isachardoublequoteclose}{\isacharparenright}% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -\isanewline -\ \ \ \ \isacommand{declare}\isamarkupfalse% -\ pow{\isacharunderscore}nat{\isachardot}simps\ {\isacharbrackleft}code\ func{\isacharbrackright}\isanewline \isanewline \ \ \ \ \isacommand{definition}\isamarkupfalse% \isanewline -\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline \isanewline \ \ \ \ \isacommand{definition}\isamarkupfalse% \isanewline -\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\isanewline +\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% -\noindent Now we generate and compile code for SML:% +\noindent This maps to Haskell as:% \end{isamarkuptext}% \isamarkuptrue% -\ \ \ \ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ example\ {\isacharparenleft}SML\ {\isacharminus}{\isacharparenright}% +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% +\ example\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\noindent The result is as expected:% +\lsthaskell{Thy/code_examples/Classes.hs} + + \noindent (we have left out all other modules). + + \noindent The whole code in SML with explicit dictionary passing:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% +\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptext}% +\lstsml{Thy/code_examples/classes.ML}% \end{isamarkuptext}% \isamarkuptrue% % -\isadelimML -\ \ \ \ % -\endisadelimML -% -\isatagML -\isacommand{ML}\isamarkupfalse% -\ {\isacharverbatimopen}\isanewline -\ \ \ \ \ \ if\ ROOT{\isachardot}Classes{\isachardot}example\ {\isacharequal}\ {\isachartilde}{\isadigit{2}}{\isadigit{0}}\ then\ {\isacharparenleft}{\isacharparenright}\ else\ error\ {\isachardoublequote}Wrong\ result{\isachardoublequote}\isanewline -\ \ \ \ {\isacharverbatimclose}% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -\isanewline -% \isadelimtheory -\isanewline % \endisadelimtheory % diff -r f662831459de -r b550d2c6ca90 doc-src/IsarAdvanced/Classes/classes.tex --- a/doc-src/IsarAdvanced/Classes/classes.tex Wed Feb 14 10:06:12 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Wed Feb 14 10:06:13 2007 +0100 @@ -3,6 +3,7 @@ \documentclass[12pt,a4paper,fleqn]{report} \usepackage{latexsym,graphicx} +\usepackage{listings} \usepackage[refpage]{nomencl} \usepackage{../../iman,../../extra,../../isar,../../proof} \usepackage{Thy/document/isabelle,Thy/document/isabellesym} @@ -38,6 +39,10 @@ \newcommand{\strong}[1]{{\bfseries #1}} \newcommand{\fixme}[1][!]{\strong{FIXME: #1}} +\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single} +\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}} +\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}} + \hyphenation{Isabelle} \hyphenation{Isar} diff -r f662831459de -r b550d2c6ca90 doc-src/manual.bib --- a/doc-src/manual.bib Wed Feb 14 10:06:12 2007 +0100 +++ b/doc-src/manual.bib Wed Feb 14 10:06:13 2007 +0100 @@ -1507,3 +1507,8 @@ series = LNCS, volume = 2152, year = 2001} + +@unpublished{classes_modules, + title = {ML Modules and Haskell Type Classes: A Constructive Comparison}, + author = {Stefan Wehr et. al.} +}