1\chapter{More about Types} 2\label{ch:more-types} 3 4So far we have learned about a few basic types (for example \isa{bool} and 5\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes 6(\isacommand{datatype}). This chapter will introduce more 7advanced material: 8\begin{itemize} 9\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), 10and how to reason about them. 11\item Type classes: how to specify and reason about axiomatic collections of 12 types ({\S}\ref{sec:axclass}). This section leads on to a discussion of 13 Isabelle's numeric types ({\S}\ref{sec:numbers}). 14\item Introducing your own types: how to define types that 15 cannot be constructed with any of the basic methods 16 ({\S}\ref{sec:adv-typedef}). 17\end{itemize} 18 19The material in this section goes beyond the needs of most novices. 20Serious users should at least skim the sections as far as type classes. 21That material is fairly advanced; read the beginning to understand what it 22is about, but consult the rest only when necessary. 23 24\index{pairs and tuples|(} 25\input{Pairs} %%%Section "Pairs and Tuples" 26\index{pairs and tuples|)} 27 28\input{Records} %%%Section "Records" 29 30 31\section{Type Classes} %%%Section 32\label{sec:axclass} 33\index{axiomatic type classes|(} 34\index{*axclass|(} 35 36The programming language Haskell has popularized the notion of type 37classes: a type class is a set of types with a 38common interface: all types in that class must provide the functions 39in the interface. Isabelle offers a similar type class concept: in 40addition, properties (\emph{class axioms}) can be specified which any 41instance of this type class must obey. Thus we can talk about a type 42$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case 43if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be 44organized in a hierarchy. Thus there is the notion of a class $D$ 45being a subclass\index{subclasses} of a class $C$, written $D 46< C$. This is the case if all axioms of $C$ are also provable in $D$. 47 48In this section we introduce the most important concepts behind type 49classes by means of a running example from algebra. This should give 50you an intuition how to use type classes and to understand 51specifications involving type classes. Type classes are covered more 52deeply in a separate tutorial \cite{isabelle-classes}. 53 54\subsection{Overloading} 55\label{sec:overloading} 56\index{overloading|(} 57 58\input{Overloading} 59 60\index{overloading|)} 61 62\input{Axioms} 63 64\index{type classes|)} 65\index{*class|)} 66 67\input{numerics} %%%Section "Numbers" 68 69\input{Typedefs} %%%Section "Introducing New Types" 70