doc-src/TutorialI/Types/types.tex
 changeset 10305 adff80268127 child 10328 bf33cbd76c05
equal inserted replaced

     1 \chapter{More about Types}

     2

     3 So far we have learned about a few basic types (for example \isa{bool} and

     4 \isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes

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

     6 advanced material:

     7 \begin{itemize}

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

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

    10   about them.

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

    12   cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).

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

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

    15 \end{itemize}

    16

    17 \section{Axiomatic type classes}

    18 \label{sec:axclass}

    19 \index{axiomatic type class|(}

    20 \index{*axclass|(}

    21

    22

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

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

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

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

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

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

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

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

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

    32 by means of a running example, ordering relations.

    33

    34 \subsection{Overloading}

    35 \label{sec:overloading}

    36 \index{overloading|(}

    37

    38 \input{Types/document/Overloading0}

    39 \input{Types/document/Overloading1}

    40 \input{Types/document/Overloading}

    41 \input{Types/document/Overloading2}

    42

    43 \index{overloading|)}

    44

    45 Finally we should remind our readers that \isa{Main} contains a much more

    46 developed theory of orderings phrased in terms of the usual $\leq$ and

    47 \isa{<}. It is recommended that, if possible, you base your own

    48 ordering relations on this theory.

    49

    50 \index{axiomatic type class|)}

    51 \index{*axclass|)}