10305
|
1 |
\chapter{More about Types}
|
|
2 |
|
|
3 |
So far we have learned about a few basic types (for example \isa{bool} and
|
|
4 |
\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes
|
|
5 |
(\isacommand{datatype}). This chapter will introduce the following more
|
|
6 |
advanced material:
|
|
7 |
\begin{itemize}
|
|
8 |
\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
|
|
9 |
({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
|
|
10 |
about them.
|
|
11 |
\item Introducing your own types: how to introduce your own new types that
|
|
12 |
cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).
|
|
13 |
\item Type classes: how to specify and reason about axiomatic collections of
|
|
14 |
types ({\S}\ref{sec:axclass}).
|
|
15 |
\end{itemize}
|
|
16 |
|
|
17 |
\section{Axiomatic type classes}
|
|
18 |
\label{sec:axclass}
|
|
19 |
\index{axiomatic type class|(}
|
|
20 |
\index{*axclass|(}
|
|
21 |
|
|
22 |
|
|
23 |
The programming language Haskell has popularized the notion of type classes.
|
|
24 |
Isabelle offers the related concept of an \textbf{axiomatic type class}.
|
|
25 |
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
|
|
26 |
an axiomatic specification of a class of types. Thus we can talk about a type
|
|
27 |
$t$ being in a class $c$, which is written $\tau :: c$. This is the case of
|
|
28 |
$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
|
|
29 |
organized in a hierarchy. Thus there is the notion of a class $d$ being a
|
|
30 |
\textbf{subclass} of a class $c$, written $d < c$. This is the case if all
|
|
31 |
axioms of $c$ are also provable in $d$. Let us now introduce these concepts
|
|
32 |
by means of a running example, ordering relations.
|
|
33 |
|
|
34 |
\subsection{Overloading}
|
|
35 |
\label{sec:overloading}
|
|
36 |
\index{overloading|(}
|
|
37 |
|
|
38 |
\input{Types/document/Overloading0}
|
|
39 |
\input{Types/document/Overloading1}
|
|
40 |
\input{Types/document/Overloading}
|
|
41 |
\input{Types/document/Overloading2}
|
|
42 |
|
|
43 |
\index{overloading|)}
|
|
44 |
|
10329
|
45 |
\input{Types/document/Axioms0}
|
10305
|
46 |
|
|
47 |
\index{axiomatic type class|)}
|
|
48 |
\index{*axclass|)}
|