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"