1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Feb 14 10:06:12 2007 +0100
1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Feb 14 10:06:13 2007 +0100
1.3 @@ -1,11 +1,15 @@
1.4
1.5 (* $Id$ *)
1.6
1.7 +(*<*)
1.8 theory Classes
1.9 imports Main
1.10 begin
1.11
1.12 -(*<*)
1.13 +ML {*
1.14 +CodegenSerializer.code_width := 74;
1.15 +*}
1.16 +
1.17 syntax
1.18 "_alpha" :: "type" ("\<alpha>")
1.19 "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()::_" [0] 1000)
1.20 @@ -69,45 +73,85 @@
1.21 section {* Introduction *}
1.22
1.23 text {*
1.24 - The well-known concept of type classes
1.25 - \cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}
1.26 - offers a useful structuring mechanism for programs and proofs, which
1.27 - is more light-weight than a fully featured module mechanism. Type
1.28 - classes are able to qualify types by associating operations and
1.29 - logical properties. For example, class @{text "eq"} could provide
1.30 - an equivalence relation @{text "="} on type @{text "\<alpha>"}, and class
1.31 - @{text "ord"} could extend @{text "eq"} by providing a strict order
1.32 - @{text "<"} etc.
1.33 + Type classes were introduces by Wadler and Blott \cite{wadler89how}
1.34 + into the Haskell language, to allow for a reasonable implementation
1.35 + of overloading\footnote{throughout this tutorial, we are referring
1.36 + to classical Haskell 1.0 type classes, not considering
1.37 + later additions in expressiveness}.
1.38 + As a canonical example, a polymorphic equality function
1.39 + @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
1.40 + types for @{text "\<alpha>"}, which is achieves by splitting introduction
1.41 + of the @{text eq} function from its overloaded definitions by means
1.42 + of @{text class} and @{text instance} declarations:
1.43
1.44 - Isabelle/Isar offers Haskell-style type classes, combining operational
1.45 - and logical specifications.
1.46 -*}
1.47 + \medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
1.48 + \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
1.49
1.50 -section {* A simple algebra example \label{sec:example} *}
1.51 + \medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\
1.52 + \hspace*{4ex}@{text "eq 0 0 = True"} \\
1.53 + \hspace*{4ex}@{text "eq 0 _ = False"} \\
1.54 + \hspace*{4ex}@{text "eq _ 0 = False"} \\
1.55 + \hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}
1.56
1.57 -text {*
1.58 - We demonstrate common elements of structured specifications and
1.59 - abstract reasoning with type classes by the algebraic hierarchy of
1.60 + \medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
1.61 + \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 && eq y1 y2"}
1.62 +
1.63 + \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
1.64 + \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
1.65 + \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
1.66 +
1.67 + \medskip Type variables are annotated with (finitly many) classes;
1.68 + these annotations are assertions that a particular polymorphic type
1.69 + provides definitions for overloaded functions.
1.70 +
1.71 + Indeed, type classes not only allow for simple overloading
1.72 + but form a generic calculus, an instance of order-sorted
1.73 + algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
1.74 +
1.75 + From a software enigineering point of view, type classes
1.76 + correspond to interfaces in object-oriented languages like Java;
1.77 + so, it is naturally desirable that type classes do not only
1.78 + provide functions (class operations) but also state specifications
1.79 + implementations must obey. For example, the @{text "class eq"}
1.80 + above could be given the following specification:
1.81 +
1.82 + \medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
1.83 + \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
1.84 + \hspace*{2ex}@{text "satisfying"} \\
1.85 + \hspace*{4ex}@{text "refl: eq x x"} \\
1.86 + \hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
1.87 + \hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
1.88 +
1.89 + \medskip From a theoretic point of view, type classes are leightweight
1.90 + modules; indeed, Haskell type classes may be emulated by
1.91 + SML functors \cite{classes_modules}.
1.92 + Isabelle/Isar offers a discipline of type classes which brings
1.93 + all those aspects together:
1.94 +
1.95 + \begin{enumerate}
1.96 + \item specifying abstract operations togehter with
1.97 + corresponding specifications,
1.98 + \item instantating those abstract operations by a particular
1.99 + type
1.100 + \item in connection with a ``less ad-hoc'' approach to overloading,
1.101 + \item with a direct link to the Isabelle module system (aka locales).
1.102 + \end{enumerate}
1.103 +
1.104 + Isar type classes also directly support code generation
1.105 + in as Haskell like fashion.
1.106 +
1.107 + This tutorial demonstrates common elements of structured specifications
1.108 + and abstract reasoning with type classes by the algebraic hierarchy of
1.109 semigroups, monoids and groups. Our background theory is that of
1.110 - Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, which uses fairly
1.111 - standard notation from mathematics and functional programming. We
1.112 - also refer to basic vernacular commands for definitions and
1.113 - statements, e.g.\ @{text "\<DEFINITION>"} and @{text "\<LEMMA>"};
1.114 - proofs will be recorded using structured elements of Isabelle/Isar
1.115 - \cite{Wenzel-PhD,Nipkow:2002}, notably @{text "\<PROOF>"}/@{text
1.116 - "\<QED>"} and @{text "\<FIX>"}/@{text "\<ASSUME>"}/@{text
1.117 - "\<SHOW>"}.
1.118 + Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
1.119 + familiarity is assumed.
1.120
1.121 - Our main concern are the new @{text "\<CLASS>"}
1.122 - and @{text "\<INSTANCE>"} elements used below.
1.123 - Here we merely present the
1.124 - look-and-feel for end users, which is quite similar to Haskell's
1.125 - \texttt{class} and \texttt{instance} \cite{hall96type}, but
1.126 - augmented by logical specifications and proofs;
1.127 + Here we merely present the look-and-feel for end users.
1.128 Internally, those are mapped to more primitive Isabelle concepts.
1.129 See \cite{haftmann_wenzel2006classes} for more detail.
1.130 *}
1.131
1.132 +section {* A simple algebra example \label{sec:example} *}
1.133
1.134 subsection {* Class definition *}
1.135
1.136 @@ -142,10 +186,10 @@
1.137 *}
1.138
1.139 instance int :: semigroup
1.140 - mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
1.141 + mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
1.142 proof
1.143 - fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
1.144 - then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
1.145 + fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
1.146 + then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
1.147 qed
1.148
1.149 text {*
1.150 @@ -153,14 +197,20 @@
1.151 as a @{text "semigroup"} automatically, i.e.\ any general results
1.152 are immediately available on concrete instances.
1.153
1.154 + Note that the first proof step is the @{text default} method,
1.155 + which for instantiation proofs maps to the @{text intro_classes} method.
1.156 + This boils down an instantiation judgement to the relevant primitive
1.157 + proof goals and should conveniently always be the first method applied
1.158 + in an instantiation proof.
1.159 +
1.160 Another instance of @{text "semigroup"} are the natural numbers:
1.161 *}
1.162
1.163 instance nat :: semigroup
1.164 - "m \<otimes> n \<equiv> m + n"
1.165 + mult_nat_def: "m \<otimes> n \<equiv> m + n"
1.166 proof
1.167 fix m n q :: nat
1.168 - show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding semigroup_nat_def by simp
1.169 + show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding mult_nat_def by simp
1.170 qed
1.171
1.172 text {*
1.173 @@ -169,12 +219,12 @@
1.174 *}
1.175
1.176 instance list :: (type) semigroup
1.177 - "xs \<otimes> ys \<equiv> xs @ ys"
1.178 + mult_list_def: "xs \<otimes> ys \<equiv> xs @ ys"
1.179 proof
1.180 fix xs ys zs :: "\<alpha> list"
1.181 show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
1.182 proof -
1.183 - from semigroup_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
1.184 + from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
1.185 thus ?thesis by simp
1.186 qed
1.187 qed
1.188 @@ -183,7 +233,7 @@
1.189 subsection {* Subclasses *}
1.190
1.191 text {*
1.192 - We define a subclass @{text "monoidl"} (a semigroup with an left-hand neutral)
1.193 + We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
1.194 by extending @{text "semigroup"}
1.195 with one additional operation @{text "neutral"} together
1.196 with its property:
1.197 @@ -200,21 +250,21 @@
1.198 *}
1.199
1.200 instance nat :: monoidl
1.201 - "\<one> \<equiv> 0"
1.202 + neutral_nat_def: "\<one> \<equiv> 0"
1.203 proof
1.204 fix n :: nat
1.205 show "\<one> \<otimes> n = n" unfolding neutral_nat_def mult_nat_def by simp
1.206 qed
1.207
1.208 instance int :: monoidl
1.209 - "\<one> \<equiv> 0"
1.210 + neutral_int_def: "\<one> \<equiv> 0"
1.211 proof
1.212 fix k :: int
1.213 show "\<one> \<otimes> k = k" unfolding neutral_int_def mult_int_def by simp
1.214 qed
1.215
1.216 instance list :: (type) monoidl
1.217 - "\<one> \<equiv> []"
1.218 + neutral_list_def: "\<one> \<equiv> []"
1.219 proof
1.220 fix xs :: "\<alpha> list"
1.221 show "\<one> \<otimes> xs = xs"
1.222 @@ -226,27 +276,26 @@
1.223 qed
1.224
1.225 text {*
1.226 - To finish our small algebra example, we add @{text "monoid"}
1.227 - and @{text "group"} classes with corresponding instances
1.228 + \noindent Fully-fledged monoids are modelled by another subclass
1.229 + which does not add new operations but tightens the specification:
1.230 *}
1.231
1.232 class monoid = monoidl +
1.233 assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
1.234
1.235 - instance nat :: monoid
1.236 +text {*
1.237 + \noindent Instantiations may also be given simultaneously for different
1.238 + type constructors:
1.239 +*}
1.240 +
1.241 + instance nat :: monoid and int :: monoid and list :: (type) monoid
1.242 proof
1.243 fix n :: nat
1.244 show "n \<otimes> \<one> = n" unfolding neutral_nat_def mult_nat_def by simp
1.245 - qed
1.246 -
1.247 - instance int :: monoid
1.248 - proof
1.249 + next
1.250 fix k :: int
1.251 show "k \<otimes> \<one> = k" unfolding neutral_int_def mult_int_def by simp
1.252 - qed
1.253 -
1.254 - instance list :: (type) monoid
1.255 - proof
1.256 + next
1.257 fix xs :: "\<alpha> list"
1.258 show "xs \<otimes> \<one> = xs"
1.259 proof -
1.260 @@ -254,20 +303,34 @@
1.261 moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
1.262 ultimately show ?thesis by simp
1.263 qed
1.264 - qed
1.265 + qed
1.266 +
1.267 +text {*
1.268 + \noindent To finish our small algebra example, we add a @{text "group"} class
1.269 + with a corresponding instance:
1.270 +*}
1.271
1.272 class group = monoidl +
1.273 fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<^loc>\<div>)" [1000] 999)
1.274 assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
1.275
1.276 instance int :: group
1.277 - "i\<div> \<equiv> - i"
1.278 + inverse_int_def: "i\<div> \<equiv> - i"
1.279 proof
1.280 fix i :: int
1.281 have "-i + i = 0" by simp
1.282 then show "i\<div> \<otimes> i = \<one>" unfolding mult_int_def and neutral_int_def and inverse_int_def .
1.283 qed
1.284
1.285 +section {* Type classes as locales *}
1.286 +
1.287 +subsection {* A look behind the scene *}
1.288 +
1.289 +(* write here: locale *)
1.290 +
1.291 +text {*
1.292 +
1.293 +*}
1.294
1.295 subsection {* Abstract reasoning *}
1.296
1.297 @@ -305,8 +368,61 @@
1.298 text {*
1.299 *}*)
1.300
1.301 +section {* Further issues *}
1.302
1.303 -subsection {* Additional subclass relations *}
1.304 +subsection {* Code generation *}
1.305 +
1.306 +text {*
1.307 + Turning back to the first motivation for type classes,
1.308 + namely overloading, it is obvious that overloading
1.309 + stemming from @{text "\<CLASS>"} and @{text "\<INSTANCE>"}
1.310 + statements naturally maps to Haskell type classes.
1.311 + The code generator framework \cite{isabelle-codegen}
1.312 + takes this into account. Concerning target languages
1.313 + lacking type classes (e.g.~SML), type classes
1.314 + are implemented by explicit dictionary construction.
1.315 + As example, the natural power function on groups:
1.316 +*}
1.317 +
1.318 + fun
1.319 + pow_nat :: "nat \<Rightarrow> 'a\<Colon>monoidl \<Rightarrow> 'a\<Colon>monoidl" where
1.320 + "pow_nat 0 x = \<one>"
1.321 + "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
1.322 +
1.323 + definition
1.324 + pow_int :: "int \<Rightarrow> 'a\<Colon>group \<Rightarrow> 'a\<Colon>group" where
1.325 + "pow_int k x = (if k >= 0
1.326 + then pow_nat (nat k) x
1.327 + else (pow_nat (nat (- k)) x)\<div>)"
1.328 +
1.329 + definition
1.330 + example :: int where
1.331 + "example = pow_int 10 (-2)"
1.332 +
1.333 +text {*
1.334 + \noindent This maps to Haskell as:
1.335 +*}
1.336 +
1.337 +code_gen example (Haskell "code_examples/")
1.338 + (* NOTE: you may use Haskell only once in this document, otherwise
1.339 + you have to work in distinct subdirectories *)
1.340 +
1.341 +text {*
1.342 + \lsthaskell{Thy/code_examples/Classes.hs}
1.343 +
1.344 + \noindent (we have left out all other modules).
1.345 +
1.346 + \noindent The whole code in SML with explicit dictionary passing:
1.347 +*}
1.348 +
1.349 +code_gen example (*<*)(SML #)(*>*)(SML "code_examples/classes.ML")
1.350 +
1.351 +text {*
1.352 + \lstsml{Thy/code_examples/classes.ML}
1.353 +*}
1.354 +
1.355 +
1.356 +(* subsection {* Additional subclass relations *}
1.357
1.358 text {*
1.359 Any @{text "group"} is also a @{text "monoid"}; this
1.360 @@ -320,54 +436,15 @@
1.361 from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
1.362 with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
1.363 with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
1.364 - qed
1.365 + qed *)
1.366
1.367 -
1.368 -(* subsection {* Same logical content -- different syntax *}
1.369 +(* subsection {* Different syntax for same specifications *}
1.370
1.371 text {*
1.372
1.373 +(* subsection {* Syntactic classes *}
1.374 +*)
1.375 +
1.376 *} *)
1.377
1.378 -
1.379 -section {* Code generation *}
1.380 -
1.381 -text {*
1.382 - Code generation takes account of type classes,
1.383 - resulting either in Haskell type classes or SML dictionaries.
1.384 - As example, we define the natural power function on groups:
1.385 -*}
1.386 -
1.387 - function
1.388 - pow_nat :: "nat \<Rightarrow> 'a\<Colon>monoidl \<Rightarrow> 'a\<Colon>monoidl" where
1.389 - "pow_nat 0 x = \<one>"
1.390 - "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
1.391 - by pat_completeness auto
1.392 - termination pow_nat by (auto_term "measure fst")
1.393 - declare pow_nat.simps [code func]
1.394 -
1.395 - definition
1.396 - pow_int :: "int \<Rightarrow> 'a\<Colon>group \<Rightarrow> 'a\<Colon>group"
1.397 - "pow_int k x = (if k >= 0
1.398 - then pow_nat (nat k) x
1.399 - else (pow_nat (nat (- k)) x)\<div>)"
1.400 -
1.401 - definition
1.402 - example :: int
1.403 - "example = pow_int 10 (-2)"
1.404 -
1.405 -text {*
1.406 - \noindent Now we generate and compile code for SML:
1.407 -*}
1.408 -
1.409 - code_gen example (SML -)
1.410 -
1.411 -text {*
1.412 - \noindent The result is as expected:
1.413 -*}
1.414 -
1.415 - ML {*
1.416 - if ROOT.Classes.example = ~20 then () else error "Wrong result"
1.417 - *}
1.418 -
1.419 end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Wed Feb 14 10:06:13 2007 +0100
2.3 @@ -0,0 +1,51 @@
2.4 +module Classes where {
2.5 +
2.6 +import Nat;
2.7 +import Integer;
2.8 +
2.9 +class Semigroup a where {
2.10 + mult :: a -> a -> a;
2.11 +};
2.12 +
2.13 +class (Semigroup a) => Monoidl a where {
2.14 + neutral :: a;
2.15 +};
2.16 +
2.17 +class (Monoidl a) => Group a where {
2.18 + inverse :: a -> a;
2.19 +};
2.20 +
2.21 +inverse_int :: Integer -> Integer;
2.22 +inverse_int i = negate i;
2.23 +
2.24 +neutral_int :: Integer;
2.25 +neutral_int = 0;
2.26 +
2.27 +mult_int :: Integer -> Integer -> Integer;
2.28 +mult_int i j = i + j;
2.29 +
2.30 +instance Semigroup Integer where {
2.31 + mult = mult_int;
2.32 +};
2.33 +
2.34 +instance Monoidl Integer where {
2.35 + neutral = neutral_int;
2.36 +};
2.37 +
2.38 +instance Group Integer where {
2.39 + inverse = inverse_int;
2.40 +};
2.41 +
2.42 +pow_nat :: (Monoidl a) => Nat -> a -> a;
2.43 +pow_nat (Suc n) x = mult x (pow_nat n x);
2.44 +pow_nat Zero_nat x = neutral;
2.45 +
2.46 +pow_int :: (Group a) => Integer -> a -> a;
2.47 +pow_int k x =
2.48 + (if 0 <= k then pow_nat (nat k) x
2.49 + else inverse (pow_nat (nat (negate k)) x));
2.50 +
2.51 +example :: Integer;
2.52 +example = pow_int 10 (-2);
2.53 +
2.54 +}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Wed Feb 14 10:06:13 2007 +0100
3.3 @@ -0,0 +1,75 @@
3.4 +structure ROOT =
3.5 +struct
3.6 +
3.7 +structure Nat =
3.8 +struct
3.9 +
3.10 +datatype nat = Zero_nat | Suc of nat;
3.11 +
3.12 +end; (*struct Nat*)
3.13 +
3.14 +structure Integer =
3.15 +struct
3.16 +
3.17 +fun nat_aux n i =
3.18 + (if IntInf.<= (i, (0 : IntInf.int)) then n
3.19 + else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
3.20 +
3.21 +fun nat i = nat_aux Nat.Zero_nat i;
3.22 +
3.23 +fun op_eq_bit false false = true
3.24 + | op_eq_bit true true = true
3.25 + | op_eq_bit false true = false
3.26 + | op_eq_bit true false = false;
3.27 +
3.28 +end; (*struct Integer*)
3.29 +
3.30 +structure Classes =
3.31 +struct
3.32 +
3.33 +type 'a semigroup = {Classes__mult : 'a -> 'a -> 'a};
3.34 +fun mult (A_:'a semigroup) = #Classes__mult A_;
3.35 +
3.36 +type 'a monoidl =
3.37 + {Classes__monoidl_semigroup : 'a semigroup, Classes__neutral : 'a};
3.38 +fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_;
3.39 +fun neutral (A_:'a monoidl) = #Classes__neutral A_;
3.40 +
3.41 +type 'a group =
3.42 + {Classes__group_monoidl : 'a monoidl, Classes__inverse : 'a -> 'a};
3.43 +fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_;
3.44 +fun inverse (A_:'a group) = #Classes__inverse A_;
3.45 +
3.46 +fun inverse_int i = IntInf.~ i;
3.47 +
3.48 +val neutral_int : IntInf.int = (0 : IntInf.int);
3.49 +
3.50 +fun mult_int i j = IntInf.+ (i, j);
3.51 +
3.52 +val semigroup_int = {Classes__mult = mult_int} : IntInf.int semigroup;
3.53 +
3.54 +val monoidl_int =
3.55 + {Classes__monoidl_semigroup = semigroup_int,
3.56 + Classes__neutral = neutral_int}
3.57 + : IntInf.int monoidl;
3.58 +
3.59 +val group_int =
3.60 + {Classes__group_monoidl = monoidl_int, Classes__inverse = inverse_int} :
3.61 + IntInf.int group;
3.62 +
3.63 +fun pow_nat A_ (Nat.Suc n) x =
3.64 + mult (monoidl_semigroup A_) x (pow_nat A_ n x)
3.65 + | pow_nat A_ Nat.Zero_nat x = neutral A_;
3.66 +
3.67 +fun pow_int A_ k x =
3.68 + (if IntInf.<= ((0 : IntInf.int), k)
3.69 + then pow_nat (group_monoidl A_) (Integer.nat k) x
3.70 + else inverse A_
3.71 + (pow_nat (group_monoidl A_) (Integer.nat (IntInf.~ k)) x));
3.72 +
3.73 +val example : IntInf.int =
3.74 + pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);
3.75 +
3.76 +end; (*struct Classes*)
3.77 +
3.78 +end; (*struct ROOT*)
4.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Feb 14 10:06:12 2007 +0100
4.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Feb 14 10:06:13 2007 +0100
4.3 @@ -13,16 +13,34 @@
4.4 \isacommand{theory}\isamarkupfalse%
4.5 \ Classes\isanewline
4.6 \isakeyword{imports}\ Main\isanewline
4.7 -\isakeyword{begin}\isanewline
4.8 -%
4.9 +\isakeyword{begin}%
4.10 \endisatagtheory
4.11 {\isafoldtheory}%
4.12 %
4.13 \isadelimtheory
4.14 +\isanewline
4.15 %
4.16 \endisadelimtheory
4.17 %
4.18 \isadelimML
4.19 +\isanewline
4.20 +%
4.21 +\endisadelimML
4.22 +%
4.23 +\isatagML
4.24 +\isacommand{ML}\isamarkupfalse%
4.25 +\ {\isacharverbatimopen}\isanewline
4.26 +CodegenSerializer{\isachardot}code{\isacharunderscore}width\ {\isacharcolon}{\isacharequal}\ {\isadigit{7}}{\isadigit{4}}{\isacharsemicolon}\isanewline
4.27 +{\isacharverbatimclose}\isanewline
4.28 +%
4.29 +\endisatagML
4.30 +{\isafoldML}%
4.31 +%
4.32 +\isadelimML
4.33 +%
4.34 +\endisadelimML
4.35 +%
4.36 +\isadelimML
4.37 %
4.38 \endisadelimML
4.39 %
4.40 @@ -44,18 +62,82 @@
4.41 \isamarkuptrue%
4.42 %
4.43 \begin{isamarkuptext}%
4.44 -The well-known concept of type classes
4.45 - \cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}
4.46 - offers a useful structuring mechanism for programs and proofs, which
4.47 - is more light-weight than a fully featured module mechanism. Type
4.48 - classes are able to qualify types by associating operations and
4.49 - logical properties. For example, class \isa{eq} could provide
4.50 - an equivalence relation \isa{{\isacharequal}} on type \isa{{\isasymalpha}}, and class
4.51 - \isa{ord} could extend \isa{eq} by providing a strict order
4.52 - \isa{{\isacharless}} etc.
4.53 +Type classes were introduces by Wadler and Blott \cite{wadler89how}
4.54 + into the Haskell language, to allow for a reasonable implementation
4.55 + of overloading\footnote{throughout this tutorial, we are referring
4.56 + to classical Haskell 1.0 type classes, not considering
4.57 + later additions in expressiveness}.
4.58 + As a canonical example, a polymorphic equality function
4.59 + \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
4.60 + types for \isa{{\isasymalpha}}, which is achieves by splitting introduction
4.61 + of the \isa{eq} function from its overloaded definitions by means
4.62 + of \isa{class} and \isa{instance} declarations:
4.63
4.64 - Isabelle/Isar offers Haskell-style type classes, combining operational
4.65 - and logical specifications.%
4.66 + \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
4.67 + \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
4.68 +
4.69 + \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
4.70 + \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
4.71 + \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
4.72 + \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
4.73 + \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
4.74 +
4.75 + \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
4.76 + \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}}}
4.77 +
4.78 + \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
4.79 + \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
4.80 + \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
4.81 +
4.82 + \medskip Type variables are annotated with (finitly many) classes;
4.83 + these annotations are assertions that a particular polymorphic type
4.84 + provides definitions for overloaded functions.
4.85 +
4.86 + Indeed, type classes not only allow for simple overloading
4.87 + but form a generic calculus, an instance of order-sorted
4.88 + algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
4.89 +
4.90 + From a software enigineering point of view, type classes
4.91 + correspond to interfaces in object-oriented languages like Java;
4.92 + so, it is naturally desirable that type classes do not only
4.93 + provide functions (class operations) but also state specifications
4.94 + implementations must obey. For example, the \isa{class\ eq}
4.95 + above could be given the following specification:
4.96 +
4.97 + \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
4.98 + \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
4.99 + \hspace*{2ex}\isa{satisfying} \\
4.100 + \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
4.101 + \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
4.102 + \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
4.103 +
4.104 + \medskip From a theoretic point of view, type classes are leightweight
4.105 + modules; indeed, Haskell type classes may be emulated by
4.106 + SML functors \cite{classes_modules}.
4.107 + Isabelle/Isar offers a discipline of type classes which brings
4.108 + all those aspects together:
4.109 +
4.110 + \begin{enumerate}
4.111 + \item specifying abstract operations togehter with
4.112 + corresponding specifications,
4.113 + \item instantating those abstract operations by a particular
4.114 + type
4.115 + \item in connection with a ``less ad-hoc'' approach to overloading,
4.116 + \item with a direct link to the Isabelle module system (aka locales).
4.117 + \end{enumerate}
4.118 +
4.119 + Isar type classes also directly support code generation
4.120 + in as Haskell like fashion.
4.121 +
4.122 + This tutorial demonstrates common elements of structured specifications
4.123 + and abstract reasoning with type classes by the algebraic hierarchy of
4.124 + semigroups, monoids and groups. Our background theory is that of
4.125 + Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
4.126 + familiarity is assumed.
4.127 +
4.128 + Here we merely present the look-and-feel for end users.
4.129 + Internally, those are mapped to more primitive Isabelle concepts.
4.130 + See \cite{haftmann_wenzel2006classes} for more detail.%
4.131 \end{isamarkuptext}%
4.132 \isamarkuptrue%
4.133 %
4.134 @@ -63,28 +145,6 @@
4.135 }
4.136 \isamarkuptrue%
4.137 %
4.138 -\begin{isamarkuptext}%
4.139 -We demonstrate common elements of structured specifications and
4.140 - abstract reasoning with type classes by the algebraic hierarchy of
4.141 - semigroups, monoids and groups. Our background theory is that of
4.142 - Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, which uses fairly
4.143 - standard notation from mathematics and functional programming. We
4.144 - also refer to basic vernacular commands for definitions and
4.145 - statements, e.g.\ \isa{{\isasymDEFINITION}} and \isa{{\isasymLEMMA}};
4.146 - proofs will be recorded using structured elements of Isabelle/Isar
4.147 - \cite{Wenzel-PhD,Nipkow:2002}, notably \isa{{\isasymPROOF}}/\isa{{\isasymQED}} and \isa{{\isasymFIX}}/\isa{{\isasymASSUME}}/\isa{{\isasymSHOW}}.
4.148 -
4.149 - Our main concern are the new \isa{{\isasymCLASS}}
4.150 - and \isa{{\isasymINSTANCE}} elements used below.
4.151 - Here we merely present the
4.152 - look-and-feel for end users, which is quite similar to Haskell's
4.153 - \texttt{class} and \texttt{instance} \cite{hall96type}, but
4.154 - augmented by logical specifications and proofs;
4.155 - Internally, those are mapped to more primitive Isabelle concepts.
4.156 - See \cite{haftmann_wenzel2006classes} for more detail.%
4.157 -\end{isamarkuptext}%
4.158 -\isamarkuptrue%
4.159 -%
4.160 \isamarkupsubsection{Class definition%
4.161 }
4.162 \isamarkuptrue%
4.163 @@ -119,7 +179,7 @@
4.164 \isamarkuptrue%
4.165 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.166 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
4.167 -\ \ \ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
4.168 +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
4.169 %
4.170 \isadelimproof
4.171 \ \ \ \ %
4.172 @@ -128,11 +188,11 @@
4.173 \isatagproof
4.174 \isacommand{proof}\isamarkupfalse%
4.175 \isanewline
4.176 -\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
4.177 +\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
4.178 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
4.179 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
4.180 \ simp\isanewline
4.181 -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
4.182 +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
4.183 \ \isacommand{show}\isamarkupfalse%
4.184 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
4.185 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
4.186 @@ -151,12 +211,18 @@
4.187 as a \isa{semigroup} automatically, i.e.\ any general results
4.188 are immediately available on concrete instances.
4.189
4.190 + Note that the first proof step is the \isa{default} method,
4.191 + which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.
4.192 + This boils down an instantiation judgement to the relevant primitive
4.193 + proof goals and should conveniently always be the first method applied
4.194 + in an instantiation proof.
4.195 +
4.196 Another instance of \isa{semigroup} are the natural numbers:%
4.197 \end{isamarkuptext}%
4.198 \isamarkuptrue%
4.199 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.200 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
4.201 -\ \ \ \ \ \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
4.202 +\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
4.203 %
4.204 \isadelimproof
4.205 \ \ \ \ %
4.206 @@ -169,7 +235,7 @@
4.207 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
4.208 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
4.209 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
4.210 -\ semigroup{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
4.211 +\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
4.212 \ simp\isanewline
4.213 \ \ \ \ \isacommand{qed}\isamarkupfalse%
4.214 %
4.215 @@ -187,7 +253,7 @@
4.216 \isamarkuptrue%
4.217 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.218 \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
4.219 -\ \ \ \ \ \ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
4.220 +\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
4.221 %
4.222 \isadelimproof
4.223 \ \ \ \ %
4.224 @@ -203,7 +269,7 @@
4.225 \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
4.226 \ {\isacharminus}\isanewline
4.227 \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
4.228 -\ semigroup{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
4.229 +\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
4.230 \ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
4.231 \isanewline
4.232 \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
4.233 @@ -225,7 +291,7 @@
4.234 \isamarkuptrue%
4.235 %
4.236 \begin{isamarkuptext}%
4.237 -We define a subclass \isa{monoidl} (a semigroup with an left-hand neutral)
4.238 +We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
4.239 by extending \isa{semigroup}
4.240 with one additional operation \isa{neutral} together
4.241 with its property:%
4.242 @@ -243,7 +309,7 @@
4.243 \isamarkuptrue%
4.244 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.245 \ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
4.246 -\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
4.247 +\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
4.248 %
4.249 \isadelimproof
4.250 \ \ \ \ %
4.251 @@ -270,7 +336,7 @@
4.252 \isanewline
4.253 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.254 \ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
4.255 -\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
4.256 +\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
4.257 %
4.258 \isadelimproof
4.259 \ \ \ \ %
4.260 @@ -297,7 +363,7 @@
4.261 \isanewline
4.262 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.263 \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
4.264 -\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
4.265 +\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
4.266 %
4.267 \isadelimproof
4.268 \ \ \ \ %
4.269 @@ -337,16 +403,20 @@
4.270 \endisadelimproof
4.271 %
4.272 \begin{isamarkuptext}%
4.273 -To finish our small algebra example, we add \isa{monoid}
4.274 - and \isa{group} classes with corresponding instances%
4.275 +\noindent Fully-fledged monoids are modelled by another subclass
4.276 + which does not add new operations but tightens the specification:%
4.277 \end{isamarkuptext}%
4.278 \isamarkuptrue%
4.279 \ \ \ \ \isacommand{class}\isamarkupfalse%
4.280 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
4.281 -\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
4.282 -\isanewline
4.283 +\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
4.284 +\begin{isamarkuptext}%
4.285 +\noindent Instantiations may also be given simultaneously for different
4.286 + type constructors:%
4.287 +\end{isamarkuptext}%
4.288 +\isamarkuptrue%
4.289 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.290 -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
4.291 +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
4.292 %
4.293 \isadelimproof
4.294 \ \ \ \ %
4.295 @@ -361,25 +431,7 @@
4.296 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
4.297 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
4.298 \ simp\isanewline
4.299 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
4.300 -%
4.301 -\endisatagproof
4.302 -{\isafoldproof}%
4.303 -%
4.304 -\isadelimproof
4.305 -\isanewline
4.306 -%
4.307 -\endisadelimproof
4.308 -\isanewline
4.309 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
4.310 -\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
4.311 -%
4.312 -\isadelimproof
4.313 -\ \ \ \ %
4.314 -\endisadelimproof
4.315 -%
4.316 -\isatagproof
4.317 -\isacommand{proof}\isamarkupfalse%
4.318 +\ \ \ \ \isacommand{next}\isamarkupfalse%
4.319 \isanewline
4.320 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
4.321 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
4.322 @@ -387,25 +439,7 @@
4.323 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
4.324 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
4.325 \ simp\isanewline
4.326 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
4.327 -%
4.328 -\endisatagproof
4.329 -{\isafoldproof}%
4.330 -%
4.331 -\isadelimproof
4.332 -\isanewline
4.333 -%
4.334 -\endisadelimproof
4.335 -\isanewline
4.336 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
4.337 -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
4.338 -%
4.339 -\isadelimproof
4.340 -\ \ \ \ %
4.341 -\endisadelimproof
4.342 -%
4.343 -\isatagproof
4.344 -\isacommand{proof}\isamarkupfalse%
4.345 +\ \ \ \ \isacommand{next}\isamarkupfalse%
4.346 \isanewline
4.347 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
4.348 \ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
4.349 @@ -434,10 +468,14 @@
4.350 {\isafoldproof}%
4.351 %
4.352 \isadelimproof
4.353 -\ \ \isanewline
4.354 %
4.355 \endisadelimproof
4.356 -\isanewline
4.357 +%
4.358 +\begin{isamarkuptext}%
4.359 +\noindent To finish our small algebra example, we add a \isa{group} class
4.360 + with a corresponding instance:%
4.361 +\end{isamarkuptext}%
4.362 +\isamarkuptrue%
4.363 \ \ \ \ \isacommand{class}\isamarkupfalse%
4.364 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
4.365 \ \ \ \ \ \ \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
4.366 @@ -445,7 +483,7 @@
4.367 \isanewline
4.368 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.369 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
4.370 -\ \ \ \ \ \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
4.371 +\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
4.372 %
4.373 \isadelimproof
4.374 \ \ \ \ %
4.375 @@ -473,6 +511,19 @@
4.376 %
4.377 \endisadelimproof
4.378 %
4.379 +\isamarkupsection{Type classes as locales%
4.380 +}
4.381 +\isamarkuptrue%
4.382 +%
4.383 +\isamarkupsubsection{A look behind the scene%
4.384 +}
4.385 +\isamarkuptrue%
4.386 +%
4.387 +\begin{isamarkuptext}%
4.388 +%
4.389 +\end{isamarkuptext}%
4.390 +\isamarkuptrue%
4.391 +%
4.392 \isamarkupsubsection{Abstract reasoning%
4.393 }
4.394 \isamarkuptrue%
4.395 @@ -535,139 +586,65 @@
4.396 \end{isamarkuptext}%
4.397 \isamarkuptrue%
4.398 %
4.399 -\isamarkupsubsection{Additional subclass relations%
4.400 +\isamarkupsection{Further issues%
4.401 +}
4.402 +\isamarkuptrue%
4.403 +%
4.404 +\isamarkupsubsection{Code generation%
4.405 }
4.406 \isamarkuptrue%
4.407 %
4.408 \begin{isamarkuptext}%
4.409 -Any \isa{group} is also a \isa{monoid}; this
4.410 - can be made explicit by claiming an additional subclass relation,
4.411 - together with a proof of the logical difference:%
4.412 +Turning back to the first motivation for type classes,
4.413 + namely overloading, it is obvious that overloading
4.414 + stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
4.415 + statements naturally maps to Haskell type classes.
4.416 + The code generator framework \cite{isabelle-codegen}
4.417 + takes this into account. Concerning target languages
4.418 + lacking type classes (e.g.~SML), type classes
4.419 + are implemented by explicit dictionary construction.
4.420 + As example, the natural power function on groups:%
4.421 \end{isamarkuptext}%
4.422 \isamarkuptrue%
4.423 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
4.424 -\ group\ {\isacharless}\ monoid\isanewline
4.425 -%
4.426 -\isadelimproof
4.427 -\ \ \ \ %
4.428 -\endisadelimproof
4.429 -%
4.430 -\isatagproof
4.431 -\isacommand{proof}\isamarkupfalse%
4.432 -\ {\isacharminus}\isanewline
4.433 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
4.434 -\ x\isanewline
4.435 -\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
4.436 -\ invl\ \isacommand{have}\isamarkupfalse%
4.437 -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
4.438 -\ simp\isanewline
4.439 -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
4.440 -\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
4.441 -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
4.442 -\ simp\isanewline
4.443 -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
4.444 -\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
4.445 -\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
4.446 -\ simp\isanewline
4.447 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
4.448 -%
4.449 -\endisatagproof
4.450 -{\isafoldproof}%
4.451 -%
4.452 -\isadelimproof
4.453 -%
4.454 -\endisadelimproof
4.455 -%
4.456 -\isamarkupsection{Code generation%
4.457 -}
4.458 -\isamarkuptrue%
4.459 -%
4.460 -\begin{isamarkuptext}%
4.461 -Code generation takes account of type classes,
4.462 - resulting either in Haskell type classes or SML dictionaries.
4.463 - As example, we define the natural power function on groups:%
4.464 -\end{isamarkuptext}%
4.465 -\isamarkuptrue%
4.466 -\ \ \ \ \isacommand{function}\isamarkupfalse%
4.467 +\ \ \ \ \isacommand{fun}\isamarkupfalse%
4.468 \isanewline
4.469 \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
4.470 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
4.471 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
4.472 -%
4.473 -\isadelimproof
4.474 -\ \ \ \ \ \ %
4.475 -\endisadelimproof
4.476 -%
4.477 -\isatagproof
4.478 -\isacommand{by}\isamarkupfalse%
4.479 -\ pat{\isacharunderscore}completeness\ auto%
4.480 -\endisatagproof
4.481 -{\isafoldproof}%
4.482 -%
4.483 -\isadelimproof
4.484 -\isanewline
4.485 -%
4.486 -\endisadelimproof
4.487 -\ \ \ \ \isacommand{termination}\isamarkupfalse%
4.488 -\ pow{\isacharunderscore}nat%
4.489 -\isadelimproof
4.490 -\ %
4.491 -\endisadelimproof
4.492 -%
4.493 -\isatagproof
4.494 -\isacommand{by}\isamarkupfalse%
4.495 -\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ fst{\isachardoublequoteclose}{\isacharparenright}%
4.496 -\endisatagproof
4.497 -{\isafoldproof}%
4.498 -%
4.499 -\isadelimproof
4.500 -%
4.501 -\endisadelimproof
4.502 -\isanewline
4.503 -\ \ \ \ \isacommand{declare}\isamarkupfalse%
4.504 -\ pow{\isacharunderscore}nat{\isachardot}simps\ {\isacharbrackleft}code\ func{\isacharbrackright}\isanewline
4.505 \isanewline
4.506 \ \ \ \ \isacommand{definition}\isamarkupfalse%
4.507 \isanewline
4.508 -\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
4.509 +\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
4.510 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
4.511 \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
4.512 \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
4.513 \isanewline
4.514 \ \ \ \ \isacommand{definition}\isamarkupfalse%
4.515 \isanewline
4.516 -\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\isanewline
4.517 +\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
4.518 \ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
4.519 \begin{isamarkuptext}%
4.520 -\noindent Now we generate and compile code for SML:%
4.521 +\noindent This maps to Haskell as:%
4.522 \end{isamarkuptext}%
4.523 \isamarkuptrue%
4.524 -\ \ \ \ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.525 -\ example\ {\isacharparenleft}SML\ {\isacharminus}{\isacharparenright}%
4.526 +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.527 +\ example\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
4.528 \begin{isamarkuptext}%
4.529 -\noindent The result is as expected:%
4.530 +\lsthaskell{Thy/code_examples/Classes.hs}
4.531 +
4.532 + \noindent (we have left out all other modules).
4.533 +
4.534 + \noindent The whole code in SML with explicit dictionary passing:%
4.535 +\end{isamarkuptext}%
4.536 +\isamarkuptrue%
4.537 +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.538 +\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
4.539 +\begin{isamarkuptext}%
4.540 +\lstsml{Thy/code_examples/classes.ML}%
4.541 \end{isamarkuptext}%
4.542 \isamarkuptrue%
4.543 %
4.544 -\isadelimML
4.545 -\ \ \ \ %
4.546 -\endisadelimML
4.547 -%
4.548 -\isatagML
4.549 -\isacommand{ML}\isamarkupfalse%
4.550 -\ {\isacharverbatimopen}\isanewline
4.551 -\ \ \ \ \ \ if\ ROOT{\isachardot}Classes{\isachardot}example\ {\isacharequal}\ {\isachartilde}{\isadigit{2}}{\isadigit{0}}\ then\ {\isacharparenleft}{\isacharparenright}\ else\ error\ {\isachardoublequote}Wrong\ result{\isachardoublequote}\isanewline
4.552 -\ \ \ \ {\isacharverbatimclose}%
4.553 -\endisatagML
4.554 -{\isafoldML}%
4.555 -%
4.556 -\isadelimML
4.557 -%
4.558 -\endisadelimML
4.559 -\isanewline
4.560 -%
4.561 \isadelimtheory
4.562 -\isanewline
4.563 %
4.564 \endisadelimtheory
4.565 %
5.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex Wed Feb 14 10:06:12 2007 +0100
5.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Wed Feb 14 10:06:13 2007 +0100
5.3 @@ -3,6 +3,7 @@
5.4
5.5 \documentclass[12pt,a4paper,fleqn]{report}
5.6 \usepackage{latexsym,graphicx}
5.7 +\usepackage{listings}
5.8 \usepackage[refpage]{nomencl}
5.9 \usepackage{../../iman,../../extra,../../isar,../../proof}
5.10 \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
5.11 @@ -38,6 +39,10 @@
5.12 \newcommand{\strong}[1]{{\bfseries #1}}
5.13 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
5.14
5.15 +\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
5.16 +\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
5.17 +\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
5.18 +
5.19 \hyphenation{Isabelle}
5.20 \hyphenation{Isar}
5.21
6.1 --- a/doc-src/manual.bib Wed Feb 14 10:06:12 2007 +0100
6.2 +++ b/doc-src/manual.bib Wed Feb 14 10:06:13 2007 +0100
6.3 @@ -1507,3 +1507,8 @@
6.4 series = LNCS,
6.5 volume = 2152,
6.6 year = 2001}
6.7 +
6.8 +@unpublished{classes_modules,
6.9 + title = {ML Modules and Haskell Type Classes: A Constructive Comparison},
6.10 + author = {Stefan Wehr et. al.}
6.11 +}