doc-src/AxClass/Group/document/Product.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/document/Product.tex	Fri Aug 19 22:44:01 2005 +0200
@@ -0,0 +1,132 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Product}%
+\isamarkuptrue%
+%
+\isamarkupheader{Syntactic classes%
+}
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{theory}\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\medskip\noindent There is still a feature of Isabelle's type system
+  left that we have not yet discussed.  When declaring polymorphic
+  constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
+  may be constrained by type classes (or even general sorts) in an
+  arbitrary way.  Note that by default, in Isabelle/HOL the
+  declaration \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
+  for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
+  universal class of HOL, this is not really a constraint at all.
+
+ The \isa{product} class below provides a less degenerate example of
+ syntactic type classes.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{axclass}\isanewline
+\ \ product\ {\isasymsubseteq}\ type\isanewline
+\isamarkupfalse%
+\isacommand{consts}\isanewline
+\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Here class \isa{product} is defined as subclass of \isa{type}
+  without any additional axioms.  This effects in logical equivalence
+  of \isa{product} and \isa{type}, as is reflected by the trivial
+  introduction rule generated for this definition.
+
+  \medskip So what is the difference of declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway?  In this particular case where \isa{product\ {\isasymequiv}\ type}, it should be obvious that both declarations are the same
+  from the logic's point of view.  It even makes the most sense to
+  remove sort constraints from constant declarations, as far as the
+  purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+
+  On the other hand there are syntactic differences, of course.
+  Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
+  type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
+  type signature.  In our example, this arity may be always added when
+  required by means of an $\INSTANCE$ with the default proof $\DDOT$.
+
+  \medskip Thus, we may observe the following discipline of using
+  syntactic classes.  Overloaded polymorphic constants have their type
+  arguments restricted to an associated (logically trivial) class
+  \isa{c}.  Only immediately before \emph{specifying} these
+  constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
+
+  This is done for class \isa{product} and type \isa{bool} as
+  follows.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isamarkupfalse%
+\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
+ well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
+ known to the type checker.
+
+ \medskip It is very important to see that above $\DEFS$ are not
+ directly connected with $\INSTANCE$ at all!  We were just following
+ our convention to specify \isa{{\isasymodot}} on \isa{bool} after having
+ instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does not require
+ these definitions, which is in contrast to programming languages like
+ Haskell \cite{haskell-report}.
+
+ \medskip While Isabelle type classes and those of Haskell are almost
+ the same as far as type-checking and type inference are concerned,
+ there are important semantic differences.  Haskell classes require
+ their instances to \emph{provide operations} of certain \emph{names}.
+ Therefore, its \texttt{instance} has a \texttt{where} part that tells
+ the system what these ``member functions'' should be.
+
+ This style of \texttt{instance} would not make much sense in
+ Isabelle's meta-logic, because there is no internal notion of
+ ``providing operations'' or even ``names of functions''.%
+\end{isamarkuptext}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{end}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: