1\chapter{More about Types}
2\label{ch:more-types}
3
4So far we have learned about a few basic types (for example \isa{bool} and
5\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes
6(\isacommand{datatype}). This chapter will introduce more
7advanced material:
8\begin{itemize}
9\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
10and how to reason about them.
11\item Type classes: how to specify and reason about axiomatic collections of
12  types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
13  Isabelle's numeric types ({\S}\ref{sec:numbers}).  
14\item Introducing your own types: how to define types that
15  cannot be constructed with any of the basic methods
16  ({\S}\ref{sec:adv-typedef}).
17\end{itemize}
18
19The material in this section goes beyond the needs of most novices.
20Serious users should at least skim the sections as far as type classes.
21That material is fairly advanced; read the beginning to understand what it
22is about, but consult the rest only when necessary.
23
24\index{pairs and tuples|(}
25\input{Pairs}    %%%Section "Pairs and Tuples"
26\index{pairs and tuples|)}
27
28\input{Records}  %%%Section "Records"
29
30
31\section{Type Classes} %%%Section
32\label{sec:axclass}
33\index{axiomatic type classes|(}
34\index{*axclass|(}
35
36The programming language Haskell has popularized the notion of type
37classes: a type class is a set of types with a
38common interface: all types in that class must provide the functions
39in the interface.  Isabelle offers a similar type class concept: in
40addition, properties (\emph{class axioms}) can be specified which any
41instance of this type class must obey.  Thus we can talk about a type
42$\tau$ being in a class $C$, which is written $\tau :: C$.  This is the case
43if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
44organized in a hierarchy.  Thus there is the notion of a class $D$
45being a subclass\index{subclasses} of a class $C$, written $D
46< C$. This is the case if all axioms of $C$ are also provable in $D$.
47
48In this section we introduce the most important concepts behind type
49classes by means of a running example from algebra.  This should give
50you an intuition how to use type classes and to understand
51specifications involving type classes.  Type classes are covered more
52deeply in a separate tutorial \cite{isabelle-classes}.
53
54\subsection{Overloading}
55\label{sec:overloading}
56\index{overloading|(}
57
58\input{Overloading}
59
60\index{overloading|)}
61
62\input{Axioms}
63
64\index{type classes|)}
65\index{*class|)}
66
67\input{numerics}             %%%Section "Numbers"
68
69\input{Typedefs}    %%%Section "Introducing New Types"
70