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