doc-src/TutorialI/Types/types.tex

document/Records.tex;

\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 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 Type classes: how to specify and reason about axiomatic collections of
  types ({\S}\ref{sec:axclass}).
\item Introducing your own types: how to introduce new 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 on basic types and on type classes.
The latter material is fairly advanced; read the beginning to understand what
it is 
about, but consult the rest only when necessary.

\input{Types/numerics}

\index{pairs and tuples|(}
\input{Types/document/Pairs}
\index{pairs and tuples|)}

\input{Types/document/Records}


\section{Axiomatic Type Classes}
\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/document/Typedefs}