author | wenzelm |
Thu, 26 Jul 2012 18:55:42 +0200 | |
changeset 49537 | 708278fc2dff |
parent 31678 | 752f23a37240 |
permissions | -rw-r--r-- |
nipkow@10305 | 1 |
\chapter{More about Types} |
nipkow@10539 | 2 |
\label{ch:more-types} |
nipkow@10305 | 3 |
|
nipkow@10305 | 4 |
So far we have learned about a few basic types (for example \isa{bool} and |
nipkow@11277 | 5 |
\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes |
paulson@10885 | 6 |
(\isacommand{datatype}). This chapter will introduce more |
nipkow@10305 | 7 |
advanced material: |
nipkow@10305 | 8 |
\begin{itemize} |
haftmann@31678 | 9 |
\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), |
haftmann@31678 | 10 |
and how to reason about them. |
nipkow@11149 | 11 |
\item Type classes: how to specify and reason about axiomatic collections of |
paulson@14400 | 12 |
types ({\S}\ref{sec:axclass}). This section leads on to a discussion of |
paulson@14400 | 13 |
Isabelle's numeric types ({\S}\ref{sec:numbers}). |
paulson@14400 | 14 |
\item Introducing your own types: how to define types that |
nipkow@10538 | 15 |
cannot be constructed with any of the basic methods |
nipkow@10538 | 16 |
({\S}\ref{sec:adv-typedef}). |
nipkow@10305 | 17 |
\end{itemize} |
nipkow@10305 | 18 |
|
haftmann@31678 | 19 |
The material in this section goes beyond the needs of most novices. |
haftmann@31678 | 20 |
Serious users should at least skim the sections as far as type classes. |
haftmann@31678 | 21 |
That material is fairly advanced; read the beginning to understand what it |
haftmann@31678 | 22 |
is about, but consult the rest only when necessary. |
paulson@10595 | 23 |
|
paulson@11428 | 24 |
\index{pairs and tuples|(} |
wenzelm@49537 | 25 |
\input{document/Pairs} %%%Section "Pairs and Tuples" |
paulson@11428 | 26 |
\index{pairs and tuples|)} |
nipkow@10396 | 27 |
|
wenzelm@49537 | 28 |
\input{document/Records} %%%Section "Records" |
paulson@11389 | 29 |
|
nipkow@10396 | 30 |
|
haftmann@31678 | 31 |
\section{Type Classes} %%%Section |
nipkow@10305 | 32 |
\label{sec:axclass} |
paulson@11428 | 33 |
\index{axiomatic type classes|(} |
nipkow@10305 | 34 |
\index{*axclass|(} |
nipkow@10305 | 35 |
|
haftmann@31678 | 36 |
The programming language Haskell has popularized the notion of type |
haftmann@31678 | 37 |
classes: a type class is a set of types with a |
haftmann@31678 | 38 |
common interface: all types in that class must provide the functions |
haftmann@31678 | 39 |
in the interface. Isabelle offers a similar type class concept: in |
haftmann@31678 | 40 |
addition, properties (\emph{class axioms}) can be specified which any |
haftmann@31678 | 41 |
instance of this type class must obey. Thus we can talk about a type |
haftmann@31678 | 42 |
$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case |
haftmann@31678 | 43 |
if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be |
haftmann@31678 | 44 |
organized in a hierarchy. Thus there is the notion of a class $D$ |
haftmann@31678 | 45 |
being a subclass\index{subclasses} of a class $C$, written $D |
haftmann@31678 | 46 |
< C$. This is the case if all axioms of $C$ are also provable in $D$. |
nipkow@10305 | 47 |
|
haftmann@31678 | 48 |
In this section we introduce the most important concepts behind type |
haftmann@31678 | 49 |
classes by means of a running example from algebra. This should give |
haftmann@31678 | 50 |
you an intuition how to use type classes and to understand |
haftmann@31678 | 51 |
specifications involving type classes. Type classes are covered more |
haftmann@31678 | 52 |
deeply in a separate tutorial \cite{isabelle-classes}. |
nipkow@25257 | 53 |
|
nipkow@10305 | 54 |
\subsection{Overloading} |
nipkow@10305 | 55 |
\label{sec:overloading} |
nipkow@10305 | 56 |
\index{overloading|(} |
nipkow@10305 | 57 |
|
wenzelm@49537 | 58 |
\input{document/Overloading} |
nipkow@10305 | 59 |
|
nipkow@10305 | 60 |
\index{overloading|)} |
nipkow@10305 | 61 |
|
wenzelm@49537 | 62 |
\input{document/Axioms} |
nipkow@10305 | 63 |
|
haftmann@31678 | 64 |
\index{type classes|)} |
haftmann@31678 | 65 |
\index{*class|)} |
nipkow@11149 | 66 |
|
paulson@14400 | 67 |
\input{Types/numerics} %%%Section "Numbers" |
nipkow@11149 | 68 |
|
wenzelm@49537 | 69 |
\input{document/Typedefs} %%%Section "Introducing New Types" |