doc-src/TutorialI/Types/types.tex
changeset 10305 adff80268127
child 10328 bf33cbd76c05
equal deleted inserted replaced
10304:a372910d82d6 10305:adff80268127
       
     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|)}