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|)}