1 \chapter{More about Types}
4 So 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
9 \item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
10 and 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}).
19 The material in this section goes beyond the needs of most novices.
20 Serious users should at least skim the sections as far as type classes.
21 That material is fairly advanced; read the beginning to understand what it
22 is about, but consult the rest only when necessary.
24 \index{pairs and tuples|(}
25 \input{Types/document/Pairs} %%%Section "Pairs and Tuples"
26 \index{pairs and tuples|)}
28 \input{Types/document/Records} %%%Section "Records"
31 \section{Type Classes} %%%Section
33 \index{axiomatic type classes|(}
36 The programming language Haskell has popularized the notion of type
37 classes: a type class is a set of types with a
38 common interface: all types in that class must provide the functions
39 in the interface. Isabelle offers a similar type class concept: in
40 addition, properties (\emph{class axioms}) can be specified which any
41 instance 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
43 if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
44 organized in a hierarchy. Thus there is the notion of a class $D$
45 being 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$.
48 In this section we introduce the most important concepts behind type
49 classes by means of a running example from algebra. This should give
50 you an intuition how to use type classes and to understand
51 specifications involving type classes. Type classes are covered more
52 deeply in a separate tutorial \cite{isabelle-classes}.
54 \subsection{Overloading}
55 \label{sec:overloading}
58 \input{Types/document/Overloading}
62 \input{Types/document/Axioms}
64 \index{type classes|)}
67 \input{Types/numerics} %%%Section "Numbers"
69 \input{Types/document/Typedefs} %%%Section "Introducing New Types"