\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 datatpes
(\isacommand{datatype}). This chapter will introduce the following more
advanced material:
\begin{itemize}
\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
reason about them.
\item Introducing your own types: how to introduce your own new types that
cannot be constructed with any of the basic methods
({\S}\ref{sec:adv-typedef}).
\item Type classes: how to specify and reason about axiomatic collections of
types ({\S}\ref{sec:axclass}).
\end{itemize}
\section{Numbers}
\label{sec:numbers}
\index{pair|(}
\input{Types/document/Pairs}
\index{pair|)}
\section{Records}
\label{sec:records}
\input{Types/document/Typedef}
\section{Axiomatic type classes}
\label{sec:axclass}
\index{axiomatic type class|(}
\index{*axclass|(}
The programming language Haskell has popularized the notion of type classes.
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
$t$ being in a class $c$, which is written $\tau :: c$. This is the case of
$\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} of a class $c$, written $d < c$. This is the case if all
axioms of $c$ are also provable in $d$. Let us now 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 class|)}
\index{*axclass|)}