10305
|
1 |
\chapter{More about Types}
|
10539
|
2 |
\label{ch:more-types}
|
10305
|
3 |
|
|
4 |
So far we have learned about a few basic types (for example \isa{bool} and
|
11277
|
5 |
\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes
|
10885
|
6 |
(\isacommand{datatype}). This chapter will introduce more
|
10305
|
7 |
advanced material:
|
|
8 |
\begin{itemize}
|
14400
|
9 |
\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
and how to reason about them.
|
11149
|
10 |
\item Type classes: how to specify and reason about axiomatic collections of
|
14400
|
11 |
types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
|
|
12 |
Isabelle's numeric types ({\S}\ref{sec:numbers}).
|
|
13 |
\item Introducing your own types: how to define types that
|
10538
|
14 |
cannot be constructed with any of the basic methods
|
|
15 |
({\S}\ref{sec:adv-typedef}).
|
10305
|
16 |
\end{itemize}
|
|
17 |
|
14400
|
18 |
The material in this section goes beyond the needs of most novices.
Serious users should at least skim the sections as far as type classes.
That material is fairly advanced; read the beginning to understand what it
is about, but consult the rest only when necessary.
|
10595
|
19 |
|
11428
|
20 |
\index{pairs and tuples|(}
|
14400
|
21 |
\input{Types/document/Pairs} %%%Section "Pairs and Tuples"
|
11428
|
22 |
\index{pairs and tuples|)}
|
10396
|
23 |
|
14400
|
24 |
\input{Types/document/Records} %%%Section "Records"
|
11389
|
25 |
|
10396
|
26 |
|
14400
|
27 |
\section{Axiomatic Type Classes} %%%Section
|
10305
|
28 |
\label{sec:axclass}
|
11428
|
29 |
\index{axiomatic type classes|(}
|
10305
|
30 |
\index{*axclass|(}
|
|
31 |
|
|
32 |
The programming language Haskell has popularized the notion of type classes.
|
11277
|
33 |
In its simplest form, a type class is a set of types with a common interface:
|
|
34 |
all types in that class must provide the functions in the interface.
|
10305
|
35 |
Isabelle offers the related concept of an \textbf{axiomatic type class}.
|
|
36 |
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
|
|
37 |
an axiomatic specification of a class of types. Thus we can talk about a type
|
11213
|
38 |
$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if
|
11196
|
39 |
$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
|
11494
|
40 |
organized in a hierarchy. Thus there is the notion of a class $D$ being a
|
|
41 |
\textbf{subclass}\index{subclasses}
|
|
42 |
of a class $C$, written $D < C$. This is the case if all
|
11196
|
43 |
axioms of $C$ are also provable in $D$. We introduce these concepts
|
10305
|
44 |
by means of a running example, ordering relations.
|
|
45 |
|
25257
|
46 |
\begin{warn}
|
|
47 |
The material in this section describes a low-level approach to type classes.
|
|
48 |
It is recommended to use the new \isacommand{class} command instead.
|
|
49 |
For details see the appropriate tutorial~\cite{isabelle-classes} and the
|
|
50 |
related article~\cite{Haftmann-Wenzel:2006:classes}.
|
|
51 |
\end{warn}
|
|
52 |
|
|
53 |
|
10305
|
54 |
\subsection{Overloading}
|
|
55 |
\label{sec:overloading}
|
|
56 |
\index{overloading|(}
|
|
57 |
|
|
58 |
\input{Types/document/Overloading0}
|
|
59 |
\input{Types/document/Overloading1}
|
|
60 |
\input{Types/document/Overloading}
|
|
61 |
\input{Types/document/Overloading2}
|
|
62 |
|
|
63 |
\index{overloading|)}
|
|
64 |
|
10362
|
65 |
\input{Types/document/Axioms}
|
10305
|
66 |
|
11428
|
67 |
\index{axiomatic type classes|)}
|
10305
|
68 |
\index{*axclass|)}
|
11149
|
69 |
|
14400
|
70 |
\input{Types/numerics} %%%Section "Numbers"
|
11149
|
71 |
|
14400
|
72 |
\input{Types/document/Typedefs} %%%Section "Introducing New Types"
|