|
1 \chapter{More about Types} |
|
2 \label{ch:more-types} |
|
3 |
|
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 |
|
7 advanced material: |
|
8 \begin{itemize} |
|
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}). |
|
17 \end{itemize} |
|
18 |
|
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. |
|
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 |
|
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$. |
|
47 |
|
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}. |
|
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" |