author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 48966 | doc-src/TutorialI/document/types0.tex@6e15de7dd871 |
permissions | -rw-r--r-- |
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} |
|
31678 | 9 |
\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), |
10 |
and how to reason about them. |
|
11149 | 11 |
\item Type classes: how to specify and reason about axiomatic collections of |
14400 | 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 |
|
10538 | 15 |
cannot be constructed with any of the basic methods |
16 |
({\S}\ref{sec:adv-typedef}). |
|
10305 | 17 |
\end{itemize} |
18 |
||
31678 | 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. |
|
10595 | 23 |
|
11428 | 24 |
\index{pairs and tuples|(} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
25 |
\input{Pairs} %%%Section "Pairs and Tuples" |
11428 | 26 |
\index{pairs and tuples|)} |
10396 | 27 |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
28 |
\input{Records} %%%Section "Records" |
11389 | 29 |
|
10396 | 30 |
|
31678 | 31 |
\section{Type Classes} %%%Section |
10305 | 32 |
\label{sec:axclass} |
11428 | 33 |
\index{axiomatic type classes|(} |
10305 | 34 |
\index{*axclass|(} |
35 |
||
31678 | 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$. |
|
10305 | 47 |
|
31678 | 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}. |
|
25257 | 53 |
|
10305 | 54 |
\subsection{Overloading} |
55 |
\label{sec:overloading} |
|
56 |
\index{overloading|(} |
|
57 |
||
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
58 |
\input{Overloading} |
10305 | 59 |
|
60 |
\index{overloading|)} |
|
61 |
||
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
62 |
\input{Axioms} |
10305 | 63 |
|
31678 | 64 |
\index{type classes|)} |
65 |
\index{*class|)} |
|
11149 | 66 |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
67 |
\input{numerics} %%%Section "Numbers" |
11149 | 68 |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
69 |
\input{Typedefs} %%%Section "Introducing New Types" |