doc-src/TutorialI/Types/types.tex

new numerics section using type classes

\chapter{More about Types}
\label{ch:more-types}

So far we have learned about a few basic types (for example \isa{bool} and
\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes
(\isacommand{datatype}). This chapter will introduce more
advanced material:
\begin{itemize}
\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
and how to reason about them.
\item Type classes: how to specify and reason about axiomatic collections of
  types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
  Isabelle's numeric types ({\S}\ref{sec:numbers}).  
\item Introducing your own types: how to define types that
  cannot be constructed with any of the basic methods
  ({\S}\ref{sec:adv-typedef}).
\end{itemize}

The material in this section goes beyond the needs of most novices.
Serious users should at least skim the sections as far as type classes.
That material is fairly advanced; read the beginning to understand what it
is about, but consult the rest only when necessary.

\index{pairs and tuples|(}
\input{Types/document/Pairs}    %%%Section "Pairs and Tuples"
\index{pairs and tuples|)}

\input{Types/document/Records}  %%%Section "Records"


\section{Axiomatic Type Classes} %%%Section
\label{sec:axclass}
\index{axiomatic type classes|(}
\index{*axclass|(}

The programming language Haskell has popularized the notion of type classes.
In its simplest form, a type class is a set of types with a common interface:
all types in that class must provide the functions in the interface.
Isabelle offers the related concept of an \textbf{axiomatic type class}.
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
an axiomatic specification of a class of types. Thus we can talk about a type
$\tau$ being in a class $C$, which is written $\tau :: C$.  This is the case if
$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
organized in a hierarchy.  Thus there is the notion of a class $D$ being a
\textbf{subclass}\index{subclasses}
of a class $C$, written $D < C$. This is the case if all
axioms of $C$ are also provable in $D$. We introduce these concepts
by means of a running example, ordering relations.

\subsection{Overloading}
\label{sec:overloading}
\index{overloading|(}

\input{Types/document/Overloading0}
\input{Types/document/Overloading1}
\input{Types/document/Overloading}
\input{Types/document/Overloading2}

\index{overloading|)}

\input{Types/document/Axioms}

\index{axiomatic type classes|)}
\index{*axclass|)}

\input{Types/numerics}             %%%Section "Numbers"

\input{Types/document/Typedefs}    %%%Section "Introducing New Types"