\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{Pairs} %%%Section "Pairs and Tuples"
\index{pairs and tuples|)}
\input{Records} %%%Section "Records"
\section{Type Classes} %%%Section
\label{sec:axclass}
\index{axiomatic type classes|(}
\index{*axclass|(}
The programming language Haskell has popularized the notion of type
classes: 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 a similar type class concept: in
addition, properties (\emph{class axioms}) can be specified which any
instance of this type class must obey. 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 subclass\index{subclasses} of a class $C$, written $D
< C$. This is the case if all axioms of $C$ are also provable in $D$.
In this section we introduce the most important concepts behind type
classes by means of a running example from algebra. This should give
you an intuition how to use type classes and to understand
specifications involving type classes. Type classes are covered more
deeply in a separate tutorial \cite{isabelle-classes}.
\subsection{Overloading}
\label{sec:overloading}
\index{overloading|(}
\input{Overloading}
\index{overloading|)}
\input{Axioms}
\index{type classes|)}
\index{*class|)}
\input{numerics} %%%Section "Numbers"
\input{Typedefs} %%%Section "Introducing New Types"