17 declarations: \footnote{syntax here is a kind of isabellized |
17 declarations: \footnote{syntax here is a kind of isabellized |
18 Haskell} |
18 Haskell} |
19 |
19 |
20 \begin{quote} |
20 \begin{quote} |
21 |
21 |
22 \noindent@{text "class eq where"} \\ |
22 \<^noindent>@{text "class eq where"} \\ |
23 \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} |
23 \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} |
24 |
24 |
25 \medskip\noindent@{text "instance nat :: eq where"} \\ |
25 \<^medskip>\<^noindent>@{text "instance nat :: eq where"} \\ |
26 \hspace*{2ex}@{text "eq 0 0 = True"} \\ |
26 \hspace*{2ex}@{text "eq 0 0 = True"} \\ |
27 \hspace*{2ex}@{text "eq 0 _ = False"} \\ |
27 \hspace*{2ex}@{text "eq 0 _ = False"} \\ |
28 \hspace*{2ex}@{text "eq _ 0 = False"} \\ |
28 \hspace*{2ex}@{text "eq _ 0 = False"} \\ |
29 \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"} |
29 \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"} |
30 |
30 |
31 \medskip\noindent@{text "instance (\<alpha>::eq, \<beta>::eq) pair :: eq where"} \\ |
31 \<^medskip>\<^noindent>@{text "instance (\<alpha>::eq, \<beta>::eq) pair :: eq where"} \\ |
32 \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"} |
32 \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"} |
33 |
33 |
34 \medskip\noindent@{text "class ord extends eq where"} \\ |
34 \<^medskip>\<^noindent>@{text "class ord extends eq where"} \\ |
35 \hspace*{2ex}@{text "less_eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\ |
35 \hspace*{2ex}@{text "less_eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\ |
36 \hspace*{2ex}@{text "less :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} |
36 \hspace*{2ex}@{text "less :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} |
37 |
37 |
38 \end{quote} |
38 \end{quote} |
39 |
39 |
40 \noindent Type variables are annotated with (finitely many) classes; |
40 \<^noindent> Type variables are annotated with (finitely many) classes; |
41 these annotations are assertions that a particular polymorphic type |
41 these annotations are assertions that a particular polymorphic type |
42 provides definitions for overloaded functions. |
42 provides definitions for overloaded functions. |
43 |
43 |
44 Indeed, type classes not only allow for simple overloading but form |
44 Indeed, type classes not only allow for simple overloading but form |
45 a generic calculus, an instance of order-sorted algebra |
45 a generic calculus, an instance of order-sorted algebra |
54 @{text "class eq"} is an equivalence relation obeying reflexivity, |
54 @{text "class eq"} is an equivalence relation obeying reflexivity, |
55 symmetry and transitivity: |
55 symmetry and transitivity: |
56 |
56 |
57 \begin{quote} |
57 \begin{quote} |
58 |
58 |
59 \noindent@{text "class eq where"} \\ |
59 \<^noindent>@{text "class eq where"} \\ |
60 \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\ |
60 \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\ |
61 @{text "satisfying"} \\ |
61 @{text "satisfying"} \\ |
62 \hspace*{2ex}@{text "refl: eq x x"} \\ |
62 \hspace*{2ex}@{text "refl: eq x x"} \\ |
63 \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\ |
63 \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\ |
64 \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"} |
64 \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"} |
65 |
65 |
66 \end{quote} |
66 \end{quote} |
67 |
67 |
68 \noindent From a theoretical point of view, type classes are |
68 \<^noindent> From a theoretical point of view, type classes are |
69 lightweight modules; Haskell type classes may be emulated by SML |
69 lightweight modules; Haskell type classes may be emulated by SML |
70 functors @{cite classes_modules}. Isabelle/Isar offers a discipline |
70 functors @{cite classes_modules}. Isabelle/Isar offers a discipline |
71 of type classes which brings all those aspects together: |
71 of type classes which brings all those aspects together: |
72 |
72 |
73 \begin{enumerate} |
73 \begin{enumerate} |
78 \item in connection with a ``less ad-hoc'' approach to overloading, |
78 \item in connection with a ``less ad-hoc'' approach to overloading, |
79 \item with a direct link to the Isabelle module system: |
79 \item with a direct link to the Isabelle module system: |
80 locales @{cite "kammueller-locales"}. |
80 locales @{cite "kammueller-locales"}. |
81 \end{enumerate} |
81 \end{enumerate} |
82 |
82 |
83 \noindent Isar type classes also directly support code generation in |
83 \<^noindent> Isar type classes also directly support code generation in |
84 a Haskell like fashion. Internally, they are mapped to more |
84 a Haskell like fashion. Internally, they are mapped to more |
85 primitive Isabelle concepts @{cite "Haftmann-Wenzel:2006:classes"}. |
85 primitive Isabelle concepts @{cite "Haftmann-Wenzel:2006:classes"}. |
86 |
86 |
87 This tutorial demonstrates common elements of structured |
87 This tutorial demonstrates common elements of structured |
88 specifications and abstract reasoning with type classes by the |
88 specifications and abstract reasoning with type classes by the |
104 class %quote semigroup = |
104 class %quote semigroup = |
105 fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70) |
105 fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70) |
106 assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
106 assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
107 |
107 |
108 text \<open> |
108 text \<open> |
109 \noindent This @{command class} specification consists of two parts: |
109 \<^noindent> This @{command class} specification consists of two parts: |
110 the \qn{operational} part names the class parameter (@{element |
110 the \qn{operational} part names the class parameter (@{element |
111 "fixes"}), the \qn{logical} part specifies properties on them |
111 "fixes"}), the \qn{logical} part specifies properties on them |
112 (@{element "assumes"}). The local @{element "fixes"} and @{element |
112 (@{element "assumes"}). The local @{element "fixes"} and @{element |
113 "assumes"} are lifted to the theory toplevel, yielding the global |
113 "assumes"} are lifted to the theory toplevel, yielding the global |
114 parameter @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the |
114 parameter @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the |
139 qed |
139 qed |
140 |
140 |
141 end %quote |
141 end %quote |
142 |
142 |
143 text \<open> |
143 text \<open> |
144 \noindent @{command instantiation} defines class parameters at a |
144 \<^noindent> @{command instantiation} defines class parameters at a |
145 particular instance using common specification tools (here, |
145 particular instance using common specification tools (here, |
146 @{command definition}). The concluding @{command instance} opens a |
146 @{command definition}). The concluding @{command instance} opens a |
147 proof that the given parameters actually conform to the class |
147 proof that the given parameters actually conform to the class |
148 specification. Note that the first proof step is the @{method |
148 specification. Note that the first proof step is the @{method |
149 default} method, which for such instance proofs maps to the @{method |
149 default} method, which for such instance proofs maps to the @{method |
153 |
153 |
154 From now on, the type-checker will consider @{typ int} as a @{class |
154 From now on, the type-checker will consider @{typ int} as a @{class |
155 semigroup} automatically, i.e.\ any general results are immediately |
155 semigroup} automatically, i.e.\ any general results are immediately |
156 available on concrete instances. |
156 available on concrete instances. |
157 |
157 |
158 \medskip Another instance of @{class semigroup} yields the natural |
158 \<^medskip> Another instance of @{class semigroup} yields the natural |
159 numbers: |
159 numbers: |
160 \<close> |
160 \<close> |
161 |
161 |
162 instantiation %quote nat :: semigroup |
162 instantiation %quote nat :: semigroup |
163 begin |
163 begin |
173 qed |
173 qed |
174 |
174 |
175 end %quote |
175 end %quote |
176 |
176 |
177 text \<open> |
177 text \<open> |
178 \noindent Note the occurrence of the name @{text mult_nat} in the |
178 \<^noindent> Note the occurrence of the name @{text mult_nat} in the |
179 primrec declaration; by default, the local name of a class operation |
179 primrec declaration; by default, the local name of a class operation |
180 @{text f} to be instantiated on type constructor @{text \<kappa>} is |
180 @{text f} to be instantiated on type constructor @{text \<kappa>} is |
181 mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be |
181 mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be |
182 inspected using the @{command "print_context"} command. |
182 inspected using the @{command "print_context"} command. |
183 \<close> |
183 \<close> |
203 qed |
203 qed |
204 |
204 |
205 end %quote |
205 end %quote |
206 |
206 |
207 text \<open> |
207 text \<open> |
208 \noindent Associativity of product semigroups is established using |
208 \<^noindent> Associativity of product semigroups is established using |
209 the definition of @{text "(\<otimes>)"} on products and the hypothetical |
209 the definition of @{text "(\<otimes>)"} on products and the hypothetical |
210 associativity of the type components; these hypotheses are |
210 associativity of the type components; these hypotheses are |
211 legitimate due to the @{class semigroup} constraints imposed on the |
211 legitimate due to the @{class semigroup} constraints imposed on the |
212 type components by the @{command instance} proposition. Indeed, |
212 type components by the @{command instance} proposition. Indeed, |
213 this pattern often occurs with parametric types and type classes. |
213 this pattern often occurs with parametric types and type classes. |
225 class %quote monoidl = semigroup + |
225 class %quote monoidl = semigroup + |
226 fixes neutral :: "\<alpha>" ("\<one>") |
226 fixes neutral :: "\<alpha>" ("\<one>") |
227 assumes neutl: "\<one> \<otimes> x = x" |
227 assumes neutl: "\<one> \<otimes> x = x" |
228 |
228 |
229 text \<open> |
229 text \<open> |
230 \noindent Again, we prove some instances, by providing suitable |
230 \<^noindent> Again, we prove some instances, by providing suitable |
231 parameter definitions and proofs for the additional specifications. |
231 parameter definitions and proofs for the additional specifications. |
232 Observe that instantiations for types with the same arity may be |
232 Observe that instantiations for types with the same arity may be |
233 simultaneous: |
233 simultaneous: |
234 \<close> |
234 \<close> |
235 |
235 |
301 qed |
301 qed |
302 |
302 |
303 end %quote |
303 end %quote |
304 |
304 |
305 text \<open> |
305 text \<open> |
306 \noindent To finish our small algebra example, we add a @{text |
306 \<^noindent> To finish our small algebra example, we add a @{text |
307 group} class with a corresponding instance: |
307 group} class with a corresponding instance: |
308 \<close> |
308 \<close> |
309 |
309 |
310 class %quote group = monoidl + |
310 class %quote group = monoidl + |
311 fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999) |
311 fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999) |
341 class %quote idem = |
341 class %quote idem = |
342 fixes f :: "\<alpha> \<Rightarrow> \<alpha>" |
342 fixes f :: "\<alpha> \<Rightarrow> \<alpha>" |
343 assumes idem: "f (f x) = f x" |
343 assumes idem: "f (f x) = f x" |
344 |
344 |
345 text \<open> |
345 text \<open> |
346 \noindent essentially introduces the locale |
346 \<^noindent> essentially introduces the locale |
347 \<close> (*<*)setup %invisible \<open>Sign.add_path "foo"\<close> |
347 \<close> (*<*)setup %invisible \<open>Sign.add_path "foo"\<close> |
348 (*>*) |
348 (*>*) |
349 locale %quote idem = |
349 locale %quote idem = |
350 fixes f :: "\<alpha> \<Rightarrow> \<alpha>" |
350 fixes f :: "\<alpha> \<Rightarrow> \<alpha>" |
351 assumes idem: "f (f x) = f x" |
351 assumes idem: "f (f x) = f x" |
352 |
352 |
353 text \<open>\noindent together with corresponding constant(s):\<close> |
353 text \<open>\<^noindent> together with corresponding constant(s):\<close> |
354 |
354 |
355 consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>" |
355 consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>" |
356 |
356 |
357 text \<open> |
357 text \<open> |
358 \noindent The connection to the type system is done by means of a |
358 \<^noindent> The connection to the type system is done by means of a |
359 primitive type class @{text "idem"}, together with a corresponding |
359 primitive type class @{text "idem"}, together with a corresponding |
360 interpretation: |
360 interpretation: |
361 \<close> |
361 \<close> |
362 |
362 |
363 interpretation %quote idem_class: |
363 interpretation %quote idem_class: |
364 idem "f :: (\<alpha>::idem) \<Rightarrow> \<alpha>" |
364 idem "f :: (\<alpha>::idem) \<Rightarrow> \<alpha>" |
365 (*<*)sorry(*>*) |
365 (*<*)sorry(*>*) |
366 |
366 |
367 text \<open> |
367 text \<open> |
368 \noindent This gives you the full power of the Isabelle module system; |
368 \<^noindent> This gives you the full power of the Isabelle module system; |
369 conclusions in locale @{text idem} are implicitly propagated |
369 conclusions in locale @{text idem} are implicitly propagated |
370 to class @{text idem}. |
370 to class @{text idem}. |
371 \<close> (*<*)setup %invisible \<open>Sign.parent_path\<close> |
371 \<close> (*<*)setup %invisible \<open>Sign.parent_path\<close> |
372 (*>*) |
372 (*>*) |
373 subsection \<open>Abstract reasoning\<close> |
373 subsection \<open>Abstract reasoning\<close> |
389 assume "y = z" |
389 assume "y = z" |
390 then show "x \<otimes> y = x \<otimes> z" by simp |
390 then show "x \<otimes> y = x \<otimes> z" by simp |
391 qed |
391 qed |
392 |
392 |
393 text \<open> |
393 text \<open> |
394 \noindent Here the \qt{@{keyword "in"} @{class group}} target |
394 \<^noindent> Here the \qt{@{keyword "in"} @{class group}} target |
395 specification indicates that the result is recorded within that |
395 specification indicates that the result is recorded within that |
396 context for later use. This local theorem is also lifted to the |
396 context for later use. This local theorem is also lifted to the |
397 global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z :: |
397 global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z :: |
398 \<alpha>::group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been |
398 \<alpha>::group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been |
399 made an instance of @{text "group"} before, we may refer to that |
399 made an instance of @{text "group"} before, we may refer to that |
411 primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where |
411 primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where |
412 "pow_nat 0 x = \<one>" |
412 "pow_nat 0 x = \<one>" |
413 | "pow_nat (Suc n) x = x \<otimes> pow_nat n x" |
413 | "pow_nat (Suc n) x = x \<otimes> pow_nat n x" |
414 |
414 |
415 text \<open> |
415 text \<open> |
416 \noindent If the locale @{text group} is also a class, this local |
416 \<^noindent> If the locale @{text group} is also a class, this local |
417 definition is propagated onto a global definition of @{term [source] |
417 definition is propagated onto a global definition of @{term [source] |
418 "pow_nat :: nat \<Rightarrow> \<alpha>::monoid \<Rightarrow> \<alpha>::monoid"} with corresponding theorems |
418 "pow_nat :: nat \<Rightarrow> \<alpha>::monoid \<Rightarrow> \<alpha>::monoid"} with corresponding theorems |
419 |
419 |
420 @{thm pow_nat.simps [no_vars]}. |
420 @{thm pow_nat.simps [no_vars]}. |
421 |
421 |
422 \noindent As you can see from this example, for local definitions |
422 \<^noindent> As you can see from this example, for local definitions |
423 you may use any specification tool which works together with |
423 you may use any specification tool which works together with |
424 locales, such as Krauss's recursive function package |
424 locales, such as Krauss's recursive function package |
425 @{cite krauss2006}. |
425 @{cite krauss2006}. |
426 \<close> |
426 \<close> |
427 |
427 |
444 |
444 |
445 interpretation %quote list_monoid: monoid append "[]" |
445 interpretation %quote list_monoid: monoid append "[]" |
446 proof qed auto |
446 proof qed auto |
447 |
447 |
448 text \<open> |
448 text \<open> |
449 \noindent This enables us to apply facts on monoids |
449 \<^noindent> This enables us to apply facts on monoids |
450 to lists, e.g. @{thm list_monoid.neutl [no_vars]}. |
450 to lists, e.g. @{thm list_monoid.neutl [no_vars]}. |
451 |
451 |
452 When using this interpretation pattern, it may also |
452 When using this interpretation pattern, it may also |
453 be appropriate to map derived definitions accordingly: |
453 be appropriate to map derived definitions accordingly: |
454 \<close> |
454 \<close> |
468 by (induct n) auto |
468 by (induct n) auto |
469 qed |
469 qed |
470 qed intro_locales |
470 qed intro_locales |
471 |
471 |
472 text \<open> |
472 text \<open> |
473 \noindent This pattern is also helpful to reuse abstract |
473 \<^noindent> This pattern is also helpful to reuse abstract |
474 specifications on the \emph{same} type. For example, think of a |
474 specifications on the \emph{same} type. For example, think of a |
475 class @{text preorder}; for type @{typ nat}, there are at least two |
475 class @{text preorder}; for type @{typ nat}, there are at least two |
476 possible instances: the natural order or the order induced by the |
476 possible instances: the natural order or the order induced by the |
477 divides relation. But only one of these instances can be used for |
477 divides relation. But only one of these instances can be used for |
478 @{command instantiation}; using the locale behind the class @{text |
478 @{command instantiation}; using the locale behind the class @{text |
540 "pow_int k x = (if k >= 0 |
540 "pow_int k x = (if k >= 0 |
541 then pow_nat (nat k) x |
541 then pow_nat (nat k) x |
542 else (pow_nat (nat (- k)) x)\<div>)" |
542 else (pow_nat (nat (- k)) x)\<div>)" |
543 |
543 |
544 text \<open> |
544 text \<open> |
545 \noindent yields the global definition of @{term [source] "pow_int :: |
545 \<^noindent> yields the global definition of @{term [source] "pow_int :: |
546 int \<Rightarrow> \<alpha>::group \<Rightarrow> \<alpha>::group"} with the corresponding theorem @{thm |
546 int \<Rightarrow> \<alpha>::group \<Rightarrow> \<alpha>::group"} with the corresponding theorem @{thm |
547 pow_int_def [no_vars]}. |
547 pow_int_def [no_vars]}. |
548 \<close> |
548 \<close> |
549 |
549 |
550 subsection \<open>A note on syntax\<close> |
550 subsection \<open>A note on syntax\<close> |
564 end %quote |
564 end %quote |
565 |
565 |
566 term %quote "x \<otimes> y" -- \<open>example 3\<close> |
566 term %quote "x \<otimes> y" -- \<open>example 3\<close> |
567 |
567 |
568 text \<open> |
568 text \<open> |
569 \noindent Here in example 1, the term refers to the local class |
569 \<^noindent> Here in example 1, the term refers to the local class |
570 operation @{text "mult [\<alpha>]"}, whereas in example 2 the type |
570 operation @{text "mult [\<alpha>]"}, whereas in example 2 the type |
571 constraint enforces the global class operation @{text "mult [nat]"}. |
571 constraint enforces the global class operation @{text "mult [nat]"}. |
572 In the global context in example 3, the reference is to the |
572 In the global context in example 3, the reference is to the |
573 polymorphic global class operation @{text "mult [?\<alpha> :: semigroup]"}. |
573 polymorphic global class operation @{text "mult [?\<alpha> :: semigroup]"}. |
574 \<close> |
574 \<close> |
590 |
590 |
591 definition %quote example :: int where |
591 definition %quote example :: int where |
592 "example = pow_int 10 (-2)" |
592 "example = pow_int 10 (-2)" |
593 |
593 |
594 text \<open> |
594 text \<open> |
595 \noindent This maps to Haskell as follows: |
595 \<^noindent> This maps to Haskell as follows: |
596 \<close> |
596 \<close> |
597 text %quotetypewriter \<open> |
597 text %quotetypewriter \<open> |
598 @{code_stmts example (Haskell)} |
598 @{code_stmts example (Haskell)} |
599 \<close> |
599 \<close> |
600 |
600 |
601 text \<open> |
601 text \<open> |
602 \noindent The code in SML has explicit dictionary passing: |
602 \<^noindent> The code in SML has explicit dictionary passing: |
603 \<close> |
603 \<close> |
604 text %quotetypewriter \<open> |
604 text %quotetypewriter \<open> |
605 @{code_stmts example (SML)} |
605 @{code_stmts example (SML)} |
606 \<close> |
606 \<close> |
607 |
607 |
608 |
608 |
609 text \<open> |
609 text \<open> |
610 \noindent In Scala, implicits are used as dictionaries: |
610 \<^noindent> In Scala, implicits are used as dictionaries: |
611 \<close> |
611 \<close> |
612 text %quotetypewriter \<open> |
612 text %quotetypewriter \<open> |
613 @{code_stmts example (Scala)} |
613 @{code_stmts example (Scala)} |
614 \<close> |
614 \<close> |
615 |
615 |