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 ***
 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@11277  5 \isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes  paulson@10885  6 (\isacommand{datatype}). This chapter will introduce more  nipkow@10305  7 advanced material:  nipkow@10305  8 \begin{itemize}  paulson@14400  9 \item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason about them.  nipkow@11149  10 \item Type classes: how to specify and reason about axiomatic collections of  paulson@14400  11  types ({\S}\ref{sec:axclass}). This section leads on to a discussion of  paulson@14400  12  Isabelle's numeric types ({\S}\ref{sec:numbers}).  paulson@14400  13 \item Introducing your own types: how to define types that  nipkow@10538  14  cannot be constructed with any of the basic methods  nipkow@10538  15  ({\S}\ref{sec:adv-typedef}).  nipkow@10305  16 \end{itemize}  nipkow@10305  17 paulson@14400  18 The material in this section goes beyond the needs of most novices. Serious users should at least skim the sections as far as type classes. That material is fairly advanced; read the beginning to understand what it is about, but consult the rest only when necessary.  paulson@10595  19 paulson@11428  20 \index{pairs and tuples|(}  paulson@14400  21 \input{Types/document/Pairs} %%%Section "Pairs and Tuples"  paulson@11428  22 \index{pairs and tuples|)}  nipkow@10396  23 paulson@14400  24 \input{Types/document/Records} %%%Section "Records"  paulson@11389  25 nipkow@10396  26 paulson@14400  27 \section{Axiomatic Type Classes} %%%Section  nipkow@10305  28 \label{sec:axclass}  paulson@11428  29 \index{axiomatic type classes|(}  nipkow@10305  30 \index{*axclass|(}  nipkow@10305  31 nipkow@10305  32 The programming language Haskell has popularized the notion of type classes.  nipkow@11277  33 In its simplest form, a type class is a set of types with a common interface:  nipkow@11277  34 all types in that class must provide the functions in the interface.  nipkow@10305  35 Isabelle offers the related concept of an \textbf{axiomatic type class}.  nipkow@10305  36 Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\  nipkow@10305  37 an axiomatic specification of a class of types. Thus we can talk about a type  nipkow@11213  38 $\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if  nipkow@11196  39 $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be  paulson@11494  40 organized in a hierarchy. Thus there is the notion of a class $D$ being a  paulson@11494  41 \textbf{subclass}\index{subclasses}  paulson@11494  42 of a class $C$, written $D < C$. This is the case if all  nipkow@11196  43 axioms of $C$ are also provable in $D$. We introduce these concepts  nipkow@10305  44 by means of a running example, ordering relations.  nipkow@10305  45 nipkow@25257  46 \begin{warn}  nipkow@25257  47 The material in this section describes a low-level approach to type classes.  nipkow@25257  48 It is recommended to use the new \isacommand{class} command instead.  nipkow@25257  49 For details see the appropriate tutorial~\cite{isabelle-classes} and the  nipkow@25257  50 related article~\cite{Haftmann-Wenzel:2006:classes}.  nipkow@25257  51 \end{warn}  nipkow@25257  52 nipkow@25257  53 nipkow@10305  54 \subsection{Overloading}  nipkow@10305  55 \label{sec:overloading}  nipkow@10305  56 \index{overloading|(}  nipkow@10305  57 nipkow@10305  58 \input{Types/document/Overloading0}  nipkow@10305  59 \input{Types/document/Overloading1}  nipkow@10305  60 \input{Types/document/Overloading}  nipkow@10305  61 \input{Types/document/Overloading2}  nipkow@10305  62 nipkow@10305  63 \index{overloading|)}  nipkow@10305  64 nipkow@10362  65 \input{Types/document/Axioms}  nipkow@10305  66 paulson@11428  67 \index{axiomatic type classes|)}  nipkow@10305  68 \index{*axclass|)}  nipkow@11149  69 paulson@14400  70 \input{Types/numerics} %%%Section "Numbers"  nipkow@11149  71 paulson@14400  72 \input{Types/document/Typedefs} %%%Section "Introducing New Types"