115903Swosch\chapter{More about Types} 215903Swosch\label{ch:more-types} 315903Swosch 415903SwoschSo far we have learned about a few basic types (for example \isa{bool} and 515903Swosch\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes 615903Swosch(\isacommand{datatype}). This chapter will introduce more 715903Swoschadvanced material: 815903Swosch\begin{itemize} 914968Swosch\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), 1014968Swoschand how to reason about them. 1115903Swosch\item Type classes: how to specify and reason about axiomatic collections of 1215903Swosch types ({\S}\ref{sec:axclass}). This section leads on to a discussion of 1315903Swosch Isabelle's numeric types ({\S}\ref{sec:numbers}). 1415903Swosch\item Introducing your own types: how to define types that 1515903Swosch cannot be constructed with any of the basic methods 1615903Swosch ({\S}\ref{sec:adv-typedef}). 1715903Swosch\end{itemize} 1815903Swosch 1915903SwoschThe material in this section goes beyond the needs of most novices. 2015903SwoschSerious users should at least skim the sections as far as type classes. 2115903SwoschThat material is fairly advanced; read the beginning to understand what it 2215903Swoschis about, but consult the rest only when necessary. 2315903Swosch 2415903Swosch\index{pairs and tuples|(} 2515903Swosch\input{Pairs} %%%Section "Pairs and Tuples" 2615903Swosch\index{pairs and tuples|)} 2715903Swosch 2815903Swosch\input{Records} %%%Section "Records" 2915903Swosch 3015903Swosch 3115903Swosch\section{Type Classes} %%%Section 3215903Swosch\label{sec:axclass} 3315903Swosch\index{axiomatic type classes|(} 3415903Swosch\index{*axclass|(} 3515903Swosch 3615903SwoschThe programming language Haskell has popularized the notion of type 3715903Swoschclasses: a type class is a set of types with a 3815903Swoschcommon interface: all types in that class must provide the functions 3915903Swoschin the interface. Isabelle offers a similar type class concept: in 4015903Swoschaddition, properties (\emph{class axioms}) can be specified which any 4115903Swoschinstance of this type class must obey. Thus we can talk about a type 4215903Swosch$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case 4315903Swoschif $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be 4415903Swoschorganized in a hierarchy. Thus there is the notion of a class $D$ 4515903Swoschbeing a subclass\index{subclasses} of a class $C$, written $D 4615903Swosch< C$. This is the case if all axioms of $C$ are also provable in $D$. 4715903Swosch 4815903SwoschIn this section we introduce the most important concepts behind type 4915903Swoschclasses by means of a running example from algebra. This should give 5015903Swoschyou an intuition how to use type classes and to understand 5115903Swoschspecifications involving type classes. Type classes are covered more 5215903Swoschdeeply in a separate tutorial \cite{isabelle-classes}. 5315903Swosch 5415903Swosch\subsection{Overloading} 5515903Swosch\label{sec:overloading} 5615903Swosch\index{overloading|(} 5715903Swosch 5815903Swosch\input{Overloading} 5915903Swosch 6015903Swosch\index{overloading|)} 6115903Swosch 6215903Swosch\input{Axioms} 6315903Swosch 6415903Swosch\index{type classes|)} 6515903Swosch\index{*class|)} 6615903Swosch 6715903Swosch\input{numerics} %%%Section "Numbers" 6815903Swosch 6915903Swosch\input{Typedefs} %%%Section "Introducing New Types" 7015903Swosch