doc-src/AxClass/generated/Semigroups.tex

untabified for HTML

%
\begin{isabellebody}%
\def\isabellecontext{Semigroups}%
%
\isamarkupheader{Semigroups}
\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}%
\begin{isamarkuptext}%
\medskip\noindent An axiomatic type class is simply a class of types
 that all meet certain properties, which are also called \emph{class
 axioms}. Thus, type classes may be also understood as type predicates
 --- i.e.\ abstractions over a single type argument $\alpha$.  Class
 axioms typically contain polymorphic constants that depend on this
 type $\alpha$.  These \emph{characteristic constants} behave like
 operations associated with the ``carrier'' type $\alpha$.

 We illustrate these basic concepts by the following formulation of
 semigroups.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline
\isacommand{axclass}\isanewline
\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Above we have first declared a polymorphic constant $\TIMES
 :: \alpha \To \alpha \To \alpha$ and then defined the class
 $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
 \To \tau$ is indeed an associative operator.  The $assoc$ axiom
 contains exactly one type variable, which is invisible in the above
 presentation, though.  Also note that free term variables (like $x$,
 $y$, $z$) are allowed for user convenience --- conceptually all of
 these are bound by outermost universal quantifiers.

 \medskip In general, type classes may be used to describe
 \emph{structures} with exactly one carrier $\alpha$ and a fixed
 \emph{signature}.  Different signatures require different classes.
 Below, class $plus_semigroup$ represents semigroups of the form
 $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
 to semigroups $(\tau, \TIMES^\tau)$.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
\ \ 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
\isacommand{axclass}\isanewline
\ \ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOplus}\ y{\isacharparenright}\ {\isasymOplus}\ z\ {\isacharequal}\ x\ {\isasymOplus}\ {\isacharparenleft}y\ {\isasymOplus}\ z{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Even if classes $plus_semigroup$ and $semigroup$ both
 represent semigroups in a sense, they are certainly not quite the
 same.%
\end{isamarkuptext}%
\isacommand{end}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: