--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Feb 14 10:06:12 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Feb 14 10:06:13 2007 +0100
@@ -1,11 +1,15 @@
(* $Id$ *)
+(*<*)
theory Classes
imports Main
begin
-(*<*)
+ML {*
+CodegenSerializer.code_width := 74;
+*}
+
syntax
"_alpha" :: "type" ("\<alpha>")
"_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()::_" [0] 1000)
@@ -69,45 +73,85 @@
section {* Introduction *}
text {*
- 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 @{text "eq"} could provide
- an equivalence relation @{text "="} on type @{text "\<alpha>"}, and class
- @{text "ord"} could extend @{text "eq"} by providing a strict order
- @{text "<"} 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
+ @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
+ types for @{text "\<alpha>"}, which is achieves by splitting introduction
+ of the @{text eq} function from its overloaded definitions by means
+ of @{text class} and @{text instance} declarations:
+
+ \medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
+ \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
- Isabelle/Isar offers Haskell-style type classes, combining operational
- and logical specifications.
-*}
+ \medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\
+ \hspace*{4ex}@{text "eq 0 0 = True"} \\
+ \hspace*{4ex}@{text "eq 0 _ = False"} \\
+ \hspace*{4ex}@{text "eq _ 0 = False"} \\
+ \hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}
+
+ \medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+ \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 && eq y1 y2"}
-section {* A simple algebra example \label{sec:example} *}
+ \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
+ \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+ \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> 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}.
-text {*
- We demonstrate common elements of structured specifications and
- abstract reasoning with type classes by the algebraic hierarchy of
+ 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 @{text "class eq"}
+ above could be given the following specification:
+
+ \medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
+ \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+ \hspace*{2ex}@{text "satisfying"} \\
+ \hspace*{4ex}@{text "refl: eq x x"} \\
+ \hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
+ \hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> 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}, which uses fairly
- standard notation from mathematics and functional programming. We
- also refer to basic vernacular commands for definitions and
- statements, e.g.\ @{text "\<DEFINITION>"} and @{text "\<LEMMA>"};
- proofs will be recorded using structured elements of Isabelle/Isar
- \cite{Wenzel-PhD,Nipkow:2002}, notably @{text "\<PROOF>"}/@{text
- "\<QED>"} and @{text "\<FIX>"}/@{text "\<ASSUME>"}/@{text
- "\<SHOW>"}.
+ Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
+ familiarity is assumed.
- Our main concern are the new @{text "\<CLASS>"}
- and @{text "\<INSTANCE>"} 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;
+ 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.
*}
+section {* A simple algebra example \label{sec:example} *}
subsection {* Class definition *}
@@ -142,10 +186,10 @@
*}
instance int :: semigroup
- mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
+ mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
proof
- fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
- then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
+ fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
+ then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
qed
text {*
@@ -153,14 +197,20 @@
as a @{text "semigroup"} automatically, i.e.\ any general results
are immediately available on concrete instances.
+ Note that the first proof step is the @{text default} method,
+ which for instantiation proofs maps to the @{text intro_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 @{text "semigroup"} are the natural numbers:
*}
instance nat :: semigroup
- "m \<otimes> n \<equiv> m + n"
+ mult_nat_def: "m \<otimes> n \<equiv> m + n"
proof
fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding semigroup_nat_def by simp
+ show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding mult_nat_def by simp
qed
text {*
@@ -169,12 +219,12 @@
*}
instance list :: (type) semigroup
- "xs \<otimes> ys \<equiv> xs @ ys"
+ mult_list_def: "xs \<otimes> ys \<equiv> xs @ ys"
proof
fix xs ys zs :: "\<alpha> list"
show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
proof -
- from semigroup_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
+ from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
thus ?thesis by simp
qed
qed
@@ -183,7 +233,7 @@
subsection {* Subclasses *}
text {*
- We define a subclass @{text "monoidl"} (a semigroup with an left-hand neutral)
+ We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
by extending @{text "semigroup"}
with one additional operation @{text "neutral"} together
with its property:
@@ -200,21 +250,21 @@
*}
instance nat :: monoidl
- "\<one> \<equiv> 0"
+ neutral_nat_def: "\<one> \<equiv> 0"
proof
fix n :: nat
show "\<one> \<otimes> n = n" unfolding neutral_nat_def mult_nat_def by simp
qed
instance int :: monoidl
- "\<one> \<equiv> 0"
+ neutral_int_def: "\<one> \<equiv> 0"
proof
fix k :: int
show "\<one> \<otimes> k = k" unfolding neutral_int_def mult_int_def by simp
qed
instance list :: (type) monoidl
- "\<one> \<equiv> []"
+ neutral_list_def: "\<one> \<equiv> []"
proof
fix xs :: "\<alpha> list"
show "\<one> \<otimes> xs = xs"
@@ -226,27 +276,26 @@
qed
text {*
- To finish our small algebra example, we add @{text "monoid"}
- and @{text "group"} classes with corresponding instances
+ \noindent Fully-fledged monoids are modelled by another subclass
+ which does not add new operations but tightens the specification:
*}
class monoid = monoidl +
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
- instance nat :: monoid
+text {*
+ \noindent Instantiations may also be given simultaneously for different
+ type constructors:
+*}
+
+ instance nat :: monoid and int :: monoid and list :: (type) monoid
proof
fix n :: nat
show "n \<otimes> \<one> = n" unfolding neutral_nat_def mult_nat_def by simp
- qed
-
- instance int :: monoid
- proof
+ next
fix k :: int
show "k \<otimes> \<one> = k" unfolding neutral_int_def mult_int_def by simp
- qed
-
- instance list :: (type) monoid
- proof
+ next
fix xs :: "\<alpha> list"
show "xs \<otimes> \<one> = xs"
proof -
@@ -254,20 +303,34 @@
moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
ultimately show ?thesis by simp
qed
- qed
+ qed
+
+text {*
+ \noindent To finish our small algebra example, we add a @{text "group"} class
+ with a corresponding instance:
+*}
class group = monoidl +
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<^loc>\<div>)" [1000] 999)
assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
instance int :: group
- "i\<div> \<equiv> - i"
+ inverse_int_def: "i\<div> \<equiv> - i"
proof
fix i :: int
have "-i + i = 0" by simp
then show "i\<div> \<otimes> i = \<one>" 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 "\<CLASS>"} and @{text "\<INSTANCE>"}
+ 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 \<Rightarrow> 'a\<Colon>monoidl \<Rightarrow> 'a\<Colon>monoidl" where
+ "pow_nat 0 x = \<one>"
+ "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+
+ definition
+ pow_int :: "int \<Rightarrow> 'a\<Colon>group \<Rightarrow> 'a\<Colon>group" where
+ "pow_int k x = (if k >= 0
+ then pow_nat (nat k) x
+ else (pow_nat (nat (- k)) x)\<div>)"
+
+ 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>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = 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 \<Rightarrow> 'a\<Colon>monoidl \<Rightarrow> 'a\<Colon>monoidl" where
- "pow_nat 0 x = \<one>"
- "pow_nat (Suc n) x = x \<otimes> 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 \<Rightarrow> 'a\<Colon>group \<Rightarrow> 'a\<Colon>group"
- "pow_int k x = (if k >= 0
- then pow_nat (nat k) x
- else (pow_nat (nat (- k)) x)\<div>)"
-
- 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
--- /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);
+
+}
--- /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*)
--- 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
%
--- 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}
--- 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.}
+}