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 ***
nipkow@10305
     1
\chapter{More about Types}
nipkow@10539
     2
\label{ch:more-types}
nipkow@10305
     3
nipkow@10305
     4
So far we have learned about a few basic types (for example \isa{bool} and
nipkow@10305
     5
\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes
nipkow@10305
     6
(\isacommand{datatype}). This chapter will introduce the following more
nipkow@10305
     7
advanced material:
nipkow@10305
     8
\begin{itemize}
nipkow@10305
     9
\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
nipkow@10538
    10
  ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
nipkow@10538
    11
  reason about them.
nipkow@10305
    12
\item Introducing your own types: how to introduce your own new types that
nipkow@10538
    13
  cannot be constructed with any of the basic methods
nipkow@10538
    14
  ({\S}\ref{sec:adv-typedef}).
nipkow@10305
    15
\item Type classes: how to specify and reason about axiomatic collections of
nipkow@10305
    16
  types ({\S}\ref{sec:axclass}).
nipkow@10305
    17
\end{itemize}
nipkow@10305
    18
nipkow@10538
    19
\section{Numbers}
nipkow@10396
    20
\label{sec:numbers}
nipkow@10396
    21
paulson@10595
    22
\input{Types/numerics}
paulson@10595
    23
nipkow@10543
    24
\index{pair|(}
nipkow@10538
    25
\input{Types/document/Pairs}
nipkow@10543
    26
\index{pair|)}
nipkow@10396
    27
nipkow@10538
    28
\section{Records}
nipkow@10396
    29
\label{sec:records}
nipkow@10396
    30
nipkow@10362
    31
\input{Types/document/Typedef}
nipkow@10362
    32
nipkow@10305
    33
\section{Axiomatic type classes}
nipkow@10305
    34
\label{sec:axclass}
nipkow@10305
    35
\index{axiomatic type class|(}
nipkow@10305
    36
\index{*axclass|(}
nipkow@10305
    37
nipkow@10305
    38
nipkow@10305
    39
The programming language Haskell has popularized the notion of type classes.
nipkow@10305
    40
Isabelle offers the related concept of an \textbf{axiomatic type class}.
nipkow@10305
    41
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
nipkow@10305
    42
an axiomatic specification of a class of types. Thus we can talk about a type
nipkow@10305
    43
$t$ being in a class $c$, which is written $\tau :: c$.  This is the case of
nipkow@10305
    44
$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
nipkow@10305
    45
organized in a hierarchy. Thus there is the notion of a class $d$ being a
nipkow@10305
    46
\textbf{subclass} of a class $c$, written $d < c$. This is the case if all
nipkow@10305
    47
axioms of $c$ are also provable in $d$. Let us now introduce these concepts
nipkow@10305
    48
by means of a running example, ordering relations.
nipkow@10305
    49
nipkow@10305
    50
\subsection{Overloading}
nipkow@10305
    51
\label{sec:overloading}
nipkow@10305
    52
\index{overloading|(}
nipkow@10305
    53
nipkow@10305
    54
\input{Types/document/Overloading0}
nipkow@10305
    55
\input{Types/document/Overloading1}
nipkow@10305
    56
\input{Types/document/Overloading}
nipkow@10305
    57
\input{Types/document/Overloading2}
nipkow@10305
    58
nipkow@10305
    59
\index{overloading|)}
nipkow@10305
    60
nipkow@10362
    61
\input{Types/document/Axioms}
nipkow@10305
    62
nipkow@10305
    63
\index{axiomatic type class|)}
nipkow@10305
    64
\index{*axclass|)}