doc-src/TutorialI/Types/types.tex
author nipkow
Thu Nov 01 13:44:44 2007 +0100 (2007-11-01)
changeset 25257 8faf184ba5b1
parent 14400 6069098854b9
child 31678 752f23a37240
permissions -rw-r--r--
*** empty log message ***
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}
paulson@14400
     9
\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
and how to reason about them.
nipkow@11149
    10
\item Type classes: how to specify and reason about axiomatic collections of
paulson@14400
    11
  types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
paulson@14400
    12
  Isabelle's numeric types ({\S}\ref{sec:numbers}).  
paulson@14400
    13
\item Introducing your own types: how to define types that
nipkow@10538
    14
  cannot be constructed with any of the basic methods
nipkow@10538
    15
  ({\S}\ref{sec:adv-typedef}).
nipkow@10305
    16
\end{itemize}
nipkow@10305
    17
paulson@14400
    18
The material in this section goes beyond the needs of most novices.
Serious users should at least skim the sections as far as type classes.
That material is fairly advanced; read the beginning to understand what it
is about, but consult the rest only when necessary.
paulson@10595
    19
paulson@11428
    20
\index{pairs and tuples|(}
paulson@14400
    21
\input{Types/document/Pairs}    %%%Section "Pairs and Tuples"
paulson@11428
    22
\index{pairs and tuples|)}
nipkow@10396
    23
paulson@14400
    24
\input{Types/document/Records}  %%%Section "Records"
paulson@11389
    25
nipkow@10396
    26
paulson@14400
    27
\section{Axiomatic Type Classes} %%%Section
nipkow@10305
    28
\label{sec:axclass}
paulson@11428
    29
\index{axiomatic type classes|(}
nipkow@10305
    30
\index{*axclass|(}
nipkow@10305
    31
nipkow@10305
    32
The programming language Haskell has popularized the notion of type classes.
nipkow@11277
    33
In its simplest form, a type class is a set of types with a common interface:
nipkow@11277
    34
all types in that class must provide the functions in the interface.
nipkow@10305
    35
Isabelle offers the related concept of an \textbf{axiomatic type class}.
nipkow@10305
    36
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
nipkow@10305
    37
an axiomatic specification of a class of types. Thus we can talk about a type
nipkow@11213
    38
$\tau$ being in a class $C$, which is written $\tau :: C$.  This is the case if
nipkow@11196
    39
$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
paulson@11494
    40
organized in a hierarchy.  Thus there is the notion of a class $D$ being a
paulson@11494
    41
\textbf{subclass}\index{subclasses}
paulson@11494
    42
of a class $C$, written $D < C$. This is the case if all
nipkow@11196
    43
axioms of $C$ are also provable in $D$. We introduce these concepts
nipkow@10305
    44
by means of a running example, ordering relations.
nipkow@10305
    45
nipkow@25257
    46
\begin{warn}
nipkow@25257
    47
The material in this section describes a low-level approach to type classes.
nipkow@25257
    48
It is recommended to use the new \isacommand{class} command instead.
nipkow@25257
    49
For details see the appropriate tutorial~\cite{isabelle-classes} and the
nipkow@25257
    50
related article~\cite{Haftmann-Wenzel:2006:classes}.
nipkow@25257
    51
\end{warn}
nipkow@25257
    52
nipkow@25257
    53
nipkow@10305
    54
\subsection{Overloading}
nipkow@10305
    55
\label{sec:overloading}
nipkow@10305
    56
\index{overloading|(}
nipkow@10305
    57
nipkow@10305
    58
\input{Types/document/Overloading0}
nipkow@10305
    59
\input{Types/document/Overloading1}
nipkow@10305
    60
\input{Types/document/Overloading}
nipkow@10305
    61
\input{Types/document/Overloading2}
nipkow@10305
    62
nipkow@10305
    63
\index{overloading|)}
nipkow@10305
    64
nipkow@10362
    65
\input{Types/document/Axioms}
nipkow@10305
    66
paulson@11428
    67
\index{axiomatic type classes|)}
nipkow@10305
    68
\index{*axclass|)}
nipkow@11149
    69
paulson@14400
    70
\input{Types/numerics}             %%%Section "Numbers"
nipkow@11149
    71
paulson@14400
    72
\input{Types/document/Typedefs}    %%%Section "Introducing New Types"