|
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 |
|
45 Finally we should remind our readers that \isa{Main} contains a much more |
|
46 developed theory of orderings phrased in terms of the usual $\leq$ and |
|
47 \isa{<}. It is recommended that, if possible, you base your own |
|
48 ordering relations on this theory. |
|
49 |
|
50 \index{axiomatic type class|)} |
|
51 \index{*axclass|)} |