2 header {* Semigroups *} |
2 header {* Semigroups *} |
3 |
3 |
4 theory Semigroups = Main: |
4 theory Semigroups = Main: |
5 |
5 |
6 text {* |
6 text {* |
7 \medskip\noindent An axiomatic type class is simply a class of types |
7 \medskip\noindent An axiomatic type class is simply a class of types |
8 that all meet certain properties, which are also called \emph{class |
8 that all meet certain properties, which are also called \emph{class |
9 axioms}. Thus, type classes may be also understood as type predicates |
9 axioms}. Thus, type classes may be also understood as type |
10 --- i.e.\ abstractions over a single type argument @{typ 'a}. Class |
10 predicates --- i.e.\ abstractions over a single type argument @{typ |
11 axioms typically contain polymorphic constants that depend on this |
11 'a}. Class axioms typically contain polymorphic constants that |
12 type @{typ 'a}. These \emph{characteristic constants} behave like |
12 depend on this type @{typ 'a}. These \emph{characteristic |
13 operations associated with the ``carrier'' type @{typ 'a}. |
13 constants} behave like operations associated with the ``carrier'' |
|
14 type @{typ 'a}. |
14 |
15 |
15 We illustrate these basic concepts by the following formulation of |
16 We illustrate these basic concepts by the following formulation of |
16 semigroups. |
17 semigroups. |
17 *} |
18 *} |
18 |
19 |
19 consts |
20 consts |
20 times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
21 times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
21 axclass semigroup \<subseteq> "term" |
22 axclass semigroup \<subseteq> type |
22 assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
23 assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
23 |
24 |
24 text {* |
25 text {* |
25 \noindent Above we have first declared a polymorphic constant @{text |
26 \noindent Above we have first declared a polymorphic constant @{text |
26 "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of |
27 "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of |
27 all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an |
28 all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an |
28 associative operator. The @{text assoc} axiom contains exactly one |
29 associative operator. The @{text assoc} axiom contains exactly one |
29 type variable, which is invisible in the above presentation, though. |
30 type variable, which is invisible in the above presentation, though. |
30 Also note that free term variables (like @{term x}, @{term y}, @{term |
31 Also note that free term variables (like @{term x}, @{term y}, |
31 z}) are allowed for user convenience --- conceptually all of these |
32 @{term z}) are allowed for user convenience --- conceptually all of |
32 are bound by outermost universal quantifiers. |
33 these are bound by outermost universal quantifiers. |
33 |
34 |
34 \medskip In general, type classes may be used to describe |
35 \medskip In general, type classes may be used to describe |
35 \emph{structures} with exactly one carrier @{typ 'a} and a fixed |
36 \emph{structures} with exactly one carrier @{typ 'a} and a fixed |
36 \emph{signature}. Different signatures require different classes. |
37 \emph{signature}. Different signatures require different classes. |
37 Below, class @{text plus_semigroup} represents semigroups |
38 Below, class @{text plus_semigroup} represents semigroups @{text |
38 @{text "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would |
39 "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would |
39 correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}. |
40 correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}. |
40 *} |
41 *} |
41 |
42 |
42 consts |
43 consts |
43 plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70) |
44 plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70) |
44 axclass plus_semigroup \<subseteq> "term" |
45 axclass plus_semigroup \<subseteq> type |
45 assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
46 assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
46 |
47 |
47 text {* |
48 text {* |
48 \noindent Even if classes @{text plus_semigroup} and @{text |
49 \noindent Even if classes @{text plus_semigroup} and @{text |
49 semigroup} both represent semigroups in a sense, they are certainly |
50 semigroup} both represent semigroups in a sense, they are certainly |
50 not quite the same. |
51 not quite the same. |
51 *} |
52 *} |
52 |
53 |
53 end |
54 end |