header {* Syntactic classes *}
theory Product imports Main begin
text {*
\medskip\noindent There is still a feature of Isabelle's type system
left that we have not yet discussed. When declaring polymorphic
constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
may be constrained by type classes (or even general sorts) in an
arbitrary way. Note that by default, in Isabelle/HOL the
declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
universal class of HOL, this is not really a constraint at all.
The @{text product} class below provides a less degenerate example of
syntactic type classes.
*}
axclass
product \<subseteq> type
consts
product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
text {*
Here class @{text product} is defined as subclass of @{text type}
without any additional axioms. This effects in logical equivalence
of @{text product} and @{text type}, as is reflected by the trivial
introduction rule generated for this definition.
\medskip So what is the difference of declaring @{text "\<odot> \<Colon>
'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow>
'a"} anyway? In this particular case where @{text "product \<equiv>
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 @{text \<odot>} on some type @{text \<tau>} are rejected by the
type-checker, unless the arity @{text "\<tau> \<Colon> 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
@{text c}. Only immediately before \emph{specifying} these
constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon>
c"}.
This is done for class @{text product} and type @{typ bool} as
follows.
*}
instance bool :: product ..
defs (overloaded)
product_bool_def: "x \<odot> y \<equiv> x \<and> y"
text {*
The definition @{text prod_bool_def} becomes syntactically
well-formed only after the arity @{text "bool \<Colon> 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 @{text \<odot>} on @{typ bool}
after having instantiated @{text "bool \<Colon> 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