--- a/doc-src/AxClass/Group/document/Product.tex Wed Mar 04 11:05:02 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Product}%
-%
-\isamarkupheader{Syntactic classes%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\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}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\isanewline
-\ \ product\ {\isasymsubseteq}\ type\isanewline
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
-\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 \isakeyword{instance} with the default proof
- (double-dot).
-
- \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}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ product%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequoteclose}%
-\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 \isakeyword{defs} are
- not directly connected with \isakeyword{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}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: