\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.
\begin{warn}
The material in this section describes a low-level approach to type classes.
It is recommended to use the new \isacommand{class} command instead.
For details see the appropriate tutorial~\cite{isabelle-classes} and the
related article~\cite{Haftmann-Wenzel:2006:classes}.
\end{warn}
\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"