1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Semigroups}% |
|
4 % |
|
5 \isamarkupheader{Semigroups% |
|
6 } |
|
7 \isamarkuptrue% |
|
8 % |
|
9 \isadelimtheory |
|
10 % |
|
11 \endisadelimtheory |
|
12 % |
|
13 \isatagtheory |
|
14 \isacommand{theory}\isamarkupfalse% |
|
15 \ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}% |
|
16 \endisatagtheory |
|
17 {\isafoldtheory}% |
|
18 % |
|
19 \isadelimtheory |
|
20 % |
|
21 \endisadelimtheory |
|
22 % |
|
23 \begin{isamarkuptext}% |
|
24 \medskip\noindent An axiomatic type class is simply a class of types |
|
25 that all meet certain properties, which are also called \emph{class |
|
26 axioms}. Thus, type classes may be also understood as type |
|
27 predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}. Class axioms typically contain polymorphic constants that |
|
28 depend on this type \isa{{\isacharprime}a}. These \emph{characteristic |
|
29 constants} behave like operations associated with the ``carrier'' |
|
30 type \isa{{\isacharprime}a}. |
|
31 |
|
32 We illustrate these basic concepts by the following formulation of |
|
33 semigroups.% |
|
34 \end{isamarkuptext}% |
|
35 \isamarkuptrue% |
|
36 \isacommand{consts}\isamarkupfalse% |
|
37 \isanewline |
|
38 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
39 \isacommand{axclass}\isamarkupfalse% |
|
40 \ semigroup\ {\isasymsubseteq}\ type\isanewline |
|
41 \ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}% |
|
42 \begin{isamarkuptext}% |
|
43 \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of |
|
44 all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an |
|
45 associative operator. The \isa{assoc} axiom contains exactly one |
|
46 type variable, which is invisible in the above presentation, though. |
|
47 Also note that free term variables (like \isa{x}, \isa{y}, |
|
48 \isa{z}) are allowed for user convenience --- conceptually all of |
|
49 these are bound by outermost universal quantifiers. |
|
50 |
|
51 \medskip In general, type classes may be used to describe |
|
52 \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed |
|
53 \emph{signature}. Different signatures require different classes. |
|
54 Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would |
|
55 correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.% |
|
56 \end{isamarkuptext}% |
|
57 \isamarkuptrue% |
|
58 \isacommand{consts}\isamarkupfalse% |
|
59 \isanewline |
|
60 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
61 \isacommand{axclass}\isamarkupfalse% |
|
62 \ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline |
|
63 \ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}% |
|
64 \begin{isamarkuptext}% |
|
65 \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly |
|
66 not quite the same.% |
|
67 \end{isamarkuptext}% |
|
68 \isamarkuptrue% |
|
69 % |
|
70 \isadelimtheory |
|
71 % |
|
72 \endisadelimtheory |
|
73 % |
|
74 \isatagtheory |
|
75 \isacommand{end}\isamarkupfalse% |
|
76 % |
|
77 \endisatagtheory |
|
78 {\isafoldtheory}% |
|
79 % |
|
80 \isadelimtheory |
|
81 % |
|
82 \endisadelimtheory |
|
83 \isanewline |
|
84 \end{isabellebody}% |
|
85 %%% Local Variables: |
|
86 %%% mode: latex |
|
87 %%% TeX-master: "root" |
|
88 %%% End: |
|