| products/sources/formale sprachen/Java/openjdk-20-36_src/test/jdk/javax/script/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: types0.tex Sprache: Unknown
|
\chapter{More about Types}
\label{ch:more-types} So far we have learned about a few basic types (for example \isa{bool} and \isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes (\isacommand{datatype}). This chapter will introduce more advanced material: \begin{itemize} \item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason about them. \item Type classes: how to specify and reason about axiomatic collections of types ({\S}\ref{sec:axclass}). This section leads on to a discussion of Isabelle's numeric types ({\S}\ref{sec:numbers}). \item Introducing your own types: how to define types that cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}). \end{itemize} 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. \index{pairs and tuples|(} \input{Pairs} %%%Section "Pairs and Tuples" \index{pairs and tuples|)} \input{Records} %%%Section "Records" \section{Type Classes} %%%Section \label{sec:axclass} \index{axiomatic type classes|(} \index{*axclass|(} The programming language Haskell has popularized the notion of type classes: a type class is a set of types with a common interface: all types in that class must provide the functions in the interface. Isabelle offers a similar type class concept: in addition, properties (\emph{class axioms}) can be specified which any instance of this type class must obey. Thus we can talk about a type $\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be organized in a hierarchy. Thus there is the notion of a class $D$ being a subclass\index{subclasses} of a class $C$, written $D < C$. This is the case if all axioms of $C$ are also provable in $D$. In this section we introduce the most important concepts behind type classes by means of a running example from algebra. This should give you an intuition how to use type classes and to understand specifications involving type classes. Type classes are covered more deeply in a separate tutorial \cite{isabelle-classes}. \subsection{Overloading} \label{sec:overloading} \index{overloading|(} \input{Overloading} \index{overloading|)} \input{Axioms} \index{type classes|)} \index{*class|)} \input{numerics} %%%Section "Numbers" \input{Typedefs} %%%Section "Introducing New Types" [ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ] |