doc-src/AxClass/Group/Product.thy

new Isar version;

header {* Syntactic classes *};

theory Product = Main:;

text {*
 \medskip\noindent There is still a feature of Isabelle's type system
 left that we have not yet used: when declaring polymorphic constants
 $c :: \sigma$, the type variables occurring in $\sigma$ may be
 constrained by type classes (or even general sorts) in an arbitrary
 way.  Note that by default, in Isabelle/HOL the declaration $\TIMES
 :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for
 $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class $term$
 is the universal class of HOL, this is not really a restriction at
 all.

 The $product$ class below provides a less degenerate example of
 syntactic type classes.
*};

axclass
  product < "term";
consts
  product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<otimes>" 70);

text {*
 Here class $product$ is defined as subclass of $term$ without any
 additional axioms.  This effects in logical equivalence of $product$
 and $term$, as is reflected by the trivial introduction rule
 generated for this definition.

 \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
 product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
 term) \To \alpha \To \alpha$ anyway?  In this particular case where
 $product \equiv term$, 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 $\TIMES^\tau$ are rejected by the type-checker, unless the
 arity $\tau :: product$ is part of the type signature.  In our
 example, this arity may be always added when required by means of an
 $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.

 \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 $c$.
 Only immediately before \emph{specifying} these constants on a
 certain type $\tau$ do we instantiate $\tau :: c$.

 This is done for class $product$ and type $bool$ as follows.
*};

instance bool :: product;
  by intro_classes;
defs
  product_bool_def: "x \\<otimes> y \\<equiv> x \\<and> y";

text {*
 The definition $prod_bool_def$ becomes syntactically well-formed only
 after the arity $bool :: product$ is made known to the type checker.

 \medskip It is very important to see that above $\DEFS$ are not
 directly connected with $\isarkeyword{instance}$ at all!  We were
 just following our convention to specify $\TIMES$ on $bool$ after
 having instantiated $bool :: 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 major 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} won't make much sense in Isabelle,
 because its meta-logic has no corresponding notion of ``providing
 operations'' or ``names''.
*};

end;