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

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

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

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

37

42

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