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