17133
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Semigroups}%
|
|
4 |
%
|
|
5 |
\isamarkupheader{Semigroups%
|
|
6 |
}
|
17175
|
7 |
\isamarkuptrue%
|
17133
|
8 |
%
|
|
9 |
\isadelimtheory
|
|
10 |
%
|
|
11 |
\endisadelimtheory
|
|
12 |
%
|
|
13 |
\isatagtheory
|
17175
|
14 |
\isacommand{theory}\isamarkupfalse%
|
|
15 |
\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
|
17133
|
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}%
|
17175
|
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}%
|
17133
|
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}%
|
17175
|
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}%
|
17133
|
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}%
|
17175
|
68 |
\isamarkuptrue%
|
17133
|
69 |
%
|
|
70 |
\isadelimtheory
|
|
71 |
%
|
|
72 |
\endisadelimtheory
|
|
73 |
%
|
|
74 |
\isatagtheory
|
17175
|
75 |
\isacommand{end}\isamarkupfalse%
|
|
76 |
%
|
17133
|
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:
|