doc-src/TutorialI/Types/types.tex

*** empty log message ***

\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 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 is fairly advanced: read the beginning to understand what it is
about, but consult the rest only when necessary.

\section{Numbers}
\label{sec:numbers}

\input{Types/numerics}

\index{pair|(}
\input{Types/document/Pairs}
\index{pair|)}

\section{Records}
\label{sec:records}

\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
$\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} 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 class|)}
\index{*axclass|)}


\input{Types/document/Typedef}