8890
|
1 |
|
|
2 |
\chapter{Introduction}
|
|
3 |
|
|
4 |
A Haskell-style type-system \cite{haskell-report} with ordered type-classes
|
|
5 |
has been present in Isabelle since 1991 \cite{nipkow-sorts93}. Initially,
|
|
6 |
classes have mainly served as a \emph{purely syntactic} tool to formulate
|
|
7 |
polymorphic object-logics in a clean way, such as the standard Isabelle
|
|
8 |
formulation of many-sorted FOL \cite{paulson-isa-book}.
|
|
9 |
|
|
10 |
Applying classes at the \emph{logical level} to provide a simple notion of
|
|
11 |
abstract theories and instantiations to concrete ones, has been long proposed
|
|
12 |
as well \cite{nipkow-types93,nipkow-sorts93}). At that time, Isabelle still
|
|
13 |
lacked built-in support for these \emph{axiomatic type classes}. More
|
|
14 |
importantly, their semantics was not yet fully fleshed out (and unnecessarily
|
|
15 |
complicated, too).
|
|
16 |
|
|
17 |
Since the Isabelle94 releases, actual axiomatic type classes have been an
|
|
18 |
integral part of Isabelle's meta-logic. This very simple implementation is
|
|
19 |
based on a straight-forward extension of traditional simple-typed Higher-Order
|
|
20 |
Logic, including types qualified by logical predicates and overloaded constant
|
|
21 |
definitions; see \cite{Wenzel:1997:TPHOL} for further details.
|
|
22 |
|
|
23 |
Yet until Isabelle99, there used to be still a fundamental methodological
|
|
24 |
problem in using axiomatic type classes conveniently, due to the traditional
|
|
25 |
distinction of Isabelle theory files vs.\ ML proof scripts. This has been
|
|
26 |
finally overcome with the advent of Isabelle/Isar theories
|
|
27 |
\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
|
|
28 |
This nicely accommodates the usual procedure of defining axiomatic type
|
|
29 |
classes, proving abstract properties, defining operations on concrete types,
|
|
30 |
proving concrete properties for instantiation of classes etc.
|
|
31 |
|
|
32 |
\medskip
|
|
33 |
|
|
34 |
So to cut a long story short, the present version of axiomatic type classes
|
|
35 |
(Isabelle99 or later) now provides an even more useful and convenient
|
|
36 |
mechanism for light-weight abstract theories, without any special provisions
|
|
37 |
to be observed by the user.
|
|
38 |
|
|
39 |
|
|
40 |
\chapter{Examples}\label{sec:ex}
|
|
41 |
|
|
42 |
Axiomatic type classes are a concept of Isabelle's meta-logic
|
|
43 |
\cite{paulson-isa-book,Wenzel:1997:TPHOL}. They may be applied to any
|
|
44 |
object-logic that directly uses the meta type system, such as Isabelle/HOL
|
|
45 |
\cite{isabelle-HOL}. Subsequently, we present various examples that are all
|
|
46 |
formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
|
|
47 |
FOL.
|
|
48 |
|
|
49 |
\section{Semigroups}
|
|
50 |
|
|
51 |
An axiomatic type class is simply a class of types that all meet certain
|
|
52 |
\emph{axioms}. Thus, type classes may be also understood as type predicates
|
|
53 |
--- i.e.\ abstractions over a single type argument $\alpha$. Class axioms
|
|
54 |
typically contain polymorphic constants that depend on this type $\alpha$.
|
|
55 |
These \emph{characteristic constants} behave like operations associated with
|
|
56 |
the ``carrier'' type $\alpha$.
|
|
57 |
|
8903
|
58 |
We illustrate these basic concepts by the following theory of semigroups.
|
8890
|
59 |
|
|
60 |
\bigskip
|
|
61 |
\input{generated/Semigroup}
|
|
62 |
\bigskip
|
|
63 |
|
|
64 |
\noindent
|
|
65 |
Above we have first declared a polymorphic constant $\TIMES :: \alpha \To
|
|
66 |
\alpha \To \alpha$ and then defined the class $semigroup$ of all types $\tau$
|
|
67 |
such that $\TIMES :: \tau \To \tau \To \tau$ is indeed an associative
|
|
68 |
operator. The $assoc$ axiom contains exactly one type variable, which is
|
|
69 |
invisible in the above presentation, though. Also note that free term
|
|
70 |
variables (like $x$, $y$, $z$) are allowed for user convenience ---
|
|
71 |
conceptually all of these are bound by outermost universal quantifiers.
|
|
72 |
|
|
73 |
\medskip
|
|
74 |
|
|
75 |
In general, type classes may be used to describe \emph{structures} with
|
|
76 |
exactly one carrier $\alpha$ and a fixed \emph{signature}. Different
|
|
77 |
signatures require different classes. In the following theory, class
|
|
78 |
$plus_semigroup$ represents semigroups of the form $(\tau, \PLUS^\tau)$ while
|
|
79 |
$times_semigroup$ represents semigroups $(\tau, \TIMES^\tau)$.
|
|
80 |
|
|
81 |
\bigskip
|
|
82 |
\input{generated/Semigroups}
|
|
83 |
\bigskip
|
|
84 |
|
|
85 |
\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both represent
|
|
86 |
semigroups in a sense, they are not the same!
|
|
87 |
|
|
88 |
|
|
89 |
\input{generated/Group}
|
|
90 |
|
8903
|
91 |
\input{generated/Product}
|
8890
|
92 |
|
|
93 |
|
8903
|
94 |
\section{Defining natural numbers in FOL}\label{sec:ex-natclass}
|
8890
|
95 |
|
8903
|
96 |
Axiomatic type classes abstract over exactly one type argument. Thus, any
|
|
97 |
\emph{axiomatic} theory extension where each axiom refers to at most one type
|
|
98 |
variable, may be trivially turned into a \emph{definitional} one.
|
8890
|
99 |
|
8903
|
100 |
We illustrate this with the natural numbers in Isabelle/FOL.
|
8890
|
101 |
|
8903
|
102 |
\bigskip
|
|
103 |
\input{generated/NatClass}
|
|
104 |
\bigskip
|
8890
|
105 |
|
8903
|
106 |
This is an abstract version of the plain $Nat$ theory in
|
|
107 |
FOL.\footnote{See \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
|
8890
|
108 |
|
8903
|
109 |
Basically, we have just replaced all occurrences of type $nat$ by $\alpha$ and
|
|
110 |
used the natural number axioms to define class $nat$. There is only a minor
|
|
111 |
snag, that the original recursion operator $rec$ had to be made monomorphic,
|
|
112 |
in a sense. Thus class $nat$ contains exactly those types $\tau$ that are
|
|
113 |
isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, $rec$).
|
8890
|
114 |
|
|
115 |
\medskip
|
|
116 |
|
8903
|
117 |
What we have done here can be also viewed as \emph{type specification}. Of
|
|
118 |
course, it still remains open if there is some type at all that meets the
|
|
119 |
class axioms. Now a very nice property of axiomatic type classes is, that
|
|
120 |
abstract reasoning is always possible --- independent of satisfiability. The
|
|
121 |
meta-logic won't break, even if some classes (or general sorts) turns out to
|
|
122 |
be empty (``inconsistent'') later.
|
8890
|
123 |
|
8903
|
124 |
Theorems of the abstract natural numbers may be derived in the same way as for
|
|
125 |
the concrete version. The original proof scripts may be used with some
|
|
126 |
trivial changes only (mostly adding some type constraints).
|
8890
|
127 |
|
|
128 |
|
|
129 |
%% FIXME move some parts to ref or isar-ref manual (!?);
|
|
130 |
|
|
131 |
% \chapter{The user interface of Isabelle's axclass package}
|
|
132 |
|
|
133 |
% The actual axiomatic type class package of Isabelle/Pure mainly consists
|
|
134 |
% of two new theory sections: \texttt{axclass} and \texttt{instance}. Some
|
|
135 |
% typical applications of these have already been demonstrated in
|
|
136 |
% \secref{sec:ex}, below their syntax and semantics are presented more
|
|
137 |
% completely.
|
|
138 |
|
|
139 |
|
|
140 |
% \section{The axclass section}
|
|
141 |
|
|
142 |
% Within theory files, \texttt{axclass} introduces an axiomatic type class
|
|
143 |
% definition. Its concrete syntax is:
|
|
144 |
|
|
145 |
% \begin{matharray}{l}
|
|
146 |
% \texttt{axclass} \\
|
|
147 |
% \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
|
|
148 |
% \ \ id@1\ axm@1 \\
|
|
149 |
% \ \ \vdots \\
|
|
150 |
% \ \ id@m\ axm@m
|
|
151 |
% \emphnd{matharray}
|
|
152 |
|
|
153 |
% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
|
|
154 |
% $string$) and $axm@1, \ldots, axm@m$ (with $m \ge
|
|
155 |
% 0$) are formulas (category $string$).
|
|
156 |
|
|
157 |
% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
|
|
158 |
% \texttt{logic}. Each class axiom $axm@j$ may contain any term
|
|
159 |
% variables, but at most one type variable (which need not be the same
|
|
160 |
% for all axioms). The sort of this type variable has to be a supersort
|
|
161 |
% of $\{c@1, \ldots, c@n\}$.
|
|
162 |
|
|
163 |
% \medskip
|
|
164 |
|
|
165 |
% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
|
|
166 |
% c@n$ to the type signature.
|
|
167 |
|
|
168 |
% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
|
|
169 |
% ``abstract axioms'' of $c$ with names $id@1, \ldots,
|
|
170 |
% id@m$. This is done by replacing all occurring type variables
|
|
171 |
% by $\alpha :: c$. Original axioms that do not contain any type
|
|
172 |
% variable will be prefixed by the logical precondition
|
|
173 |
% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
|
|
174 |
|
|
175 |
% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
|
|
176 |
% rule'' --- is built from the respective universal closures of
|
|
177 |
% $axm@1, \ldots, axm@m$ appropriately.
|
|
178 |
|
|
179 |
|
|
180 |
% \section{The instance section}
|
|
181 |
|
|
182 |
% Section \texttt{instance} proves class inclusions or type arities at the
|
|
183 |
% logical level and then transfers these into the type signature.
|
|
184 |
|
|
185 |
% Its concrete syntax is:
|
|
186 |
|
|
187 |
% \begin{matharray}{l}
|
|
188 |
% \texttt{instance} \\
|
|
189 |
% \ \ [\ c@1 \texttt{ < } c@2 \ |\
|
|
190 |
% t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
|
|
191 |
% \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
|
|
192 |
% \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
|
|
193 |
% \emphnd{matharray}
|
|
194 |
|
|
195 |
% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
|
|
196 |
% (all of category $id$ or $string)$. Furthermore,
|
|
197 |
% $sort@i$ are sorts in the usual Isabelle-syntax.
|
|
198 |
|
|
199 |
% \medskip
|
|
200 |
|
|
201 |
% Internally, \texttt{instance} first sets up an appropriate goal that
|
|
202 |
% expresses the class inclusion or type arity as a meta-proposition.
|
|
203 |
% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
|
|
204 |
% meta-definitions of the current theory file and the user-supplied
|
|
205 |
% witnesses. The latter are $name@1, \ldots, name@m$, where
|
|
206 |
% $id$ refers to an \ML-name of a theorem, and $string$ to an
|
|
207 |
% axiom of the current theory node\footnote{Thus, the user may reference
|
|
208 |
% axioms from above this \texttt{instance} in the theory file. Note
|
|
209 |
% that new axioms appear at the \ML-toplevel only after the file is
|
|
210 |
% processed completely.}.
|
|
211 |
|
|
212 |
% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
|
|
213 |
% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
|
|
214 |
% according to their form: Meta-definitions are unfolded, all other
|
|
215 |
% formulas are repeatedly resolved\footnote{This is done in a way that
|
|
216 |
% enables proper object-\emph{rules} to be used as witnesses for
|
|
217 |
% corresponding class axioms.} with.
|
|
218 |
|
|
219 |
% The final optional argument $text$ is \ML-code of an arbitrary
|
|
220 |
% user tactic which is applied last to any remaining goals.
|
|
221 |
|
|
222 |
% \medskip
|
|
223 |
|
|
224 |
% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
|
|
225 |
% new users of the axclass package are advised to only use the simple
|
|
226 |
% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
|
|
227 |
% the identifiers refer to theorems that are appropriate type instances
|
|
228 |
% of the class axioms. This typically requires an auxiliary theory,
|
|
229 |
% though, which defines some constants and then proves these witnesses.
|
|
230 |
|
|
231 |
|
|
232 |
%%% Local Variables:
|
|
233 |
%%% mode: latex
|
|
234 |
%%% TeX-master: "axclass"
|
|
235 |
%%% End:
|
|
236 |
% LocalWords: Isabelle FOL
|