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 ***
     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{Types/document/Pairs}    %%%Section "Pairs and Tuples"

    26 \index{pairs and tuples|)}

    27

    28 \input{Types/document/Records}  %%%Section "Records"

    29

    30

    31 \section{Axiomatic 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 classes.

    37 In its simplest form, a type class is a set of types with a common interface:

    38 all types in that class must provide the functions in the interface.

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

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

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

    42 $\tau$ being in a class $C$, which is written $\tau :: C$.  This is the case if

    43 $\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$ being a

    45 \textbf{subclass}\index{subclasses}

    46 of a class $C$, written $D < C$. This is the case if all

    47 axioms of $C$ are also provable in $D$. We introduce these concepts

    48 by means of a running example, ordering relations.

    49

    50 \begin{warn}

    51 The material in this section describes a low-level approach to type classes.

    52 It is recommended to use the new \isacommand{class} command instead.

    53 For details see the appropriate tutorial~\cite{isabelle-classes} and the

    54 related article~\cite{Haftmann-Wenzel:2006:classes}.

    55 \end{warn}

    56

    57

    58 \subsection{Overloading}

    59 \label{sec:overloading}

    60 \index{overloading|(}

    61

    62 \input{Types/document/Overloading0}

    63 \input{Types/document/Overloading1}

    64 \input{Types/document/Overloading}

    65 \input{Types/document/Overloading2}

    66

    67 \index{overloading|)}

    68

    69 \input{Types/document/Axioms}

    70

    71 \index{axiomatic type classes|)}

    72 \index{*axclass|)}

    73

    74 \input{Types/numerics}             %%%Section "Numbers"

    75

    76 \input{Types/document/Typedefs}    %%%Section "Introducing New Types"