doc-src/TutorialI/Types/types.tex
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10595 be043b89acc5 child 10885 90695f46440b permissions -rw-r--r--
*** empty log message ***
     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 datatpes

     6 (\isacommand{datatype}). This chapter will introduce the following more

     7 advanced material:

     8 \begin{itemize}

     9 \item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs

    10   ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to

    11   reason about them.

    12 \item Introducing your own types: how to introduce your own new types that

    13   cannot be constructed with any of the basic methods

    14   ({\S}\ref{sec:adv-typedef}).

    15 \item Type classes: how to specify and reason about axiomatic collections of

    16   types ({\S}\ref{sec:axclass}).

    17 \end{itemize}

    18

    19 \section{Numbers}

    20 \label{sec:numbers}

    21

    22 \input{Types/numerics}

    23

    24 \index{pair|(}

    25 \input{Types/document/Pairs}

    26 \index{pair|)}

    27

    28 \section{Records}

    29 \label{sec:records}

    30

    31 \input{Types/document/Typedef}

    32

    33 \section{Axiomatic type classes}

    34 \label{sec:axclass}

    35 \index{axiomatic type class|(}

    36 \index{*axclass|(}

    37

    38

    39 The programming language Haskell has popularized the notion of type classes.

    40 Isabelle offers the related concept of an \textbf{axiomatic type class}.

    41 Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\

    42 an axiomatic specification of a class of types. Thus we can talk about a type

    43 $t$ being in a class $c$, which is written $\tau :: c$.  This is the case of

    44 $\tau$ satisfies the axioms of $c$. Furthermore, type classes can be

    45 organized in a hierarchy. Thus there is the notion of a class $d$ being a

    46 \textbf{subclass} of a class $c$, written $d < c$. This is the case if all

    47 axioms of $c$ are also provable in $d$. Let us now introduce these concepts

    48 by means of a running example, ordering relations.

    49

    50 \subsection{Overloading}

    51 \label{sec:overloading}

    52 \index{overloading|(}

    53

    54 \input{Types/document/Overloading0}

    55 \input{Types/document/Overloading1}

    56 \input{Types/document/Overloading}

    57 \input{Types/document/Overloading2}

    58

    59 \index{overloading|)}

    60

    61 \input{Types/document/Axioms}

    62

    63 \index{axiomatic type class|)}

    64 \index{*axclass|)}