summaryrefslogtreecommitdiff
path: root/doc/refman/Classes.tex
blob: f427609fe0e56d37b77d1ec35f8cdcd78e5209a8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
\def\Haskell{\textsc{Haskell}\xspace}
\def\eol{\setlength\parskip{0pt}\par}
\def\indent#1{\noindent\kern#1}
\def\cst#1{\textsf{#1}}

\newcommand\tele[1]{\overrightarrow{#1}}

\achapter{\protect{Type Classes}}
\aauthor{Matthieu Sozeau}
\label{typeclasses}

\begin{flushleft}
  \em The status of Type Classes is experimental.
\end{flushleft}

This chapter presents a quick reference of the commands related to type
classes. For an actual introduction to type classes, there is a
description of the system \cite{sozeau08} and the literature on type
classes in \Haskell which also applies.

\asection{Class and Instance declarations}
\label{ClassesInstances}

The syntax for class and instance declarations is the same as
record syntax of \Coq:
\def\kw{\texttt}
\def\classid{\texttt}

\begin{center}
\[\begin{array}{l}
\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n) 
[: \sort] := \{\\
\begin{array}{p{0em}lcl}
  & \cst{f}_1 & : & \type_1 ; \\
  & \vdots & &  \\
  & \cst{f}_m & : & \type_m \}.
\end{array}\end{array}\]
\end{center}
\begin{center}
\[\begin{array}{l}
\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n := \{\\
\begin{array}{p{0em}lcl}
  & \cst{f}_1 & := & \term_{f_1} ; \\
  & \vdots & &  \\
  & \cst{f}_m & := & \term_{f_m} \}.
\end{array}\end{array}\]
\end{center}
\begin{coq_eval}
  Reset Initial.
  Generalizable All Variables.
\end{coq_eval}

The $\tele{\alpha_i : \tau_i}$ variables are called the \emph{parameters}
of the class and the $\tele{f_k : \type_k}$ are called the
\emph{methods}. Each class definition gives rise to a corresponding
record declaration and each instance is a regular definition whose name
is given by $\ident$ and type is an instantiation of the record type.

We'll use the following example class in the rest of the chapter:

\begin{coq_example*}
Class EqDec (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y }.
\end{coq_example*}

This class implements a boolean equality test which is compatible with
Leibniz equality on some type. An example implementation is:

\begin{coq_example*}
Instance unit_EqDec : EqDec unit :=
{ eqb x y := true ;
  eqb_leibniz x y H := 
    match x, y return x = y with tt, tt => refl_equal tt end }.
\end{coq_example*}

If one does not give all the members in the \texttt{Instance}
declaration, Coq enters the proof-mode and the user is asked to build
inhabitants of the remaining fields, e.g.:

\begin{coq_example*}
Instance eq_bool : EqDec bool :=
{ eqb x y := if x then y else negb y }.
\end{coq_example*}
\begin{coq_example}
Proof. intros x y H.
  destruct x ; destruct y ; (discriminate || reflexivity). 
Defined.
\end{coq_example}

One has to take care that the transparency of every field is determined
by the transparency of the \texttt{Instance} proof. One can use
alternatively the \texttt{Program} \texttt{Instance} \comindex{Program Instance} variant which has
richer facilities for dealing with obligations.

\asection{Binding classes}

Once a type class is declared, one can use it in class binders:
\begin{coq_example}
Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).
\end{coq_example}

When one calls a class method, a constraint is generated that is
satisfied only in contexts where the appropriate instances can be
found. In the example above, a constraint \texttt{EqDec A} is generated and
satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
found, an error is raised:

\begin{coq_example}
Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
\end{coq_example}

The algorithm used to solve constraints is a variant of the eauto tactic
that does proof search with a set of lemmas (the instances). It will use
local hypotheses as well as declared lemmas in the
\texttt{typeclass\_instances} database. Hence the example can also be
written:

\begin{coq_example}
Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).
\end{coq_example}

However, the generalizing binders should be used instead as they have
particular support for type classes:
\begin{itemize}
\item They automatically set the maximally implicit status for type
  class arguments, making derived functions as easy to use as class
  methods. In the example above, \texttt{A} and \texttt{eqa} should be
  set maximally implicit.
\item They support implicit quantification on partialy applied type
  classes.
\item They also support implicit quantification on superclasses
  (\S \ref{classes:superclasses})
\end{itemize}

Following the previous example, one can write:
\begin{coq_example}
Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
\end{coq_example}

Here \texttt{A} is implicitly generalized, and the resulting function
is equivalent to the one above.

The parsing of generalized type-class binders is different from regular
binders:
\begin{itemize}
\item Implicit arguments of the class type are ignored.
\item Superclasses arguments are automatically generalized.
\item Any remaining arguments not given as part of a type class binder
  will be automatically generalized. In other words, the rightmost
  parameters are automatically generalized if not mentionned.
\end{itemize}

One can switch off this special treatment using the $!$ mark in front of
the class name (see example below).

\asection{Parameterized Instances}

One can declare parameterized instances as in \Haskell simply by giving
the constraints as a binding context before the instance, e.g.:

\begin{coq_example}
Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
{ eqb x y := match x, y with
  | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
  end }.
\end{coq_example}
\begin{coq_eval}
Admitted.
\end{coq_eval}

These instances are used just as well as lemmas in the instance hint database.

\asection{Sections and contexts}
\label{SectionContext}
To ease the parametrization of developments by type classes, we provide
a new way to introduce variables into section contexts, compatible with 
the implicit argument mechanism. 
The new command works similarly to the \texttt{Variables} vernacular
(see \ref{Variable}), except it accepts any binding context as argument.
For example:

\begin{coq_example}
Section EqDec_defs.
  Context `{EA : EqDec A}.
\end{coq_example}

\begin{coq_example*}
  Global Instance option_eqb : EqDec (option A) :=
  { eqb x y := match x, y with
    | Some x, Some y => eqb x y
    | None, None => true
    | _, _ => false
    end }.
\end{coq_example*}
\begin{coq_eval}
Proof.
intros x y ; destruct x ; destruct y ; intros H ; 
try discriminate ; try apply eqb_leibniz in H ;
subst ; auto. 
Defined.
\end{coq_eval}

\begin{coq_example}
End EqDec_defs.
About option_eqb.
\end{coq_example}

Here the \texttt{Global} modifier redeclares the instance at the end of 
the section, once it has been generalized by the context variables it uses.

\asection{Building hierarchies}

\subsection{Superclasses}
\label{classes:superclasses}
One can also parameterize classes by other classes, generating a
hierarchy of classes and superclasses. In the same way, we give the
superclasses as a binding context:

\begin{coq_example*}
Class Ord `(E : EqDec A) :=
  { le : A -> A -> bool }.
\end{coq_example*}

Contrary to \Haskell, we have no special syntax for superclasses, but
this declaration is morally equivalent to:
\begin{verbatim}
Class `(E : EqDec A) => Ord A :=
  { le : A -> A -> bool }.
\end{verbatim}

This declaration means that any instance of the \texttt{Ord} class must
have an instance of \texttt{EqDec}. The parameters of the subclass contain
at least all the parameters of its superclasses in their order of
appearance (here \texttt{A} is the only one).
As we have seen, \texttt{Ord} is encoded as a record type with two parameters:
a type \texttt{A} and an \texttt{E} of type \texttt{EqDec A}. However, one can
still use it as if it had a single parameter inside generalizing binders: the
generalization of superclasses will be done automatically. 
\begin{coq_example*}
Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
\end{coq_example*}

In some cases, to be able to specify sharing of structures, one may want to give
explicitly the superclasses. It is possible to do it directly in regular
generalized binders, and using the \texttt{!} modifier in class
binders. For example:
\begin{coq_example*}
Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := 
  andb (le x y) (neqb x y).
\end{coq_example*}

The \texttt{!} modifier switches the way a binder is parsed back to the
regular interpretation of Coq. In particular, it uses the implicit
arguments mechanism if available, as shown in the example.

\subsection{Substructures}

Substructures are components of a class which are instances of a class
themselves. They often arise when using classes for logical properties,
e.g.:

\begin{coq_eval}
Require Import Relations.
\end{coq_eval}
\begin{coq_example*}
Class Reflexive (A : Type) (R : relation A) :=
  reflexivity : forall x, R x x.
Class Transitive (A : Type) (R : relation A) :=
  transitivity : forall x y z, R x y -> R y z -> R x z.
\end{coq_example*}

This declares singleton classes for reflexive and transitive relations,
(see \ref{SingletonClass} for an explanation).
These may be used as part of other classes:

\begin{coq_example*}
Class PreOrder (A : Type) (R : relation A) :=
{ PreOrder_Reflexive :> Reflexive A R ;
  PreOrder_Transitive :> Transitive A R }.
\end{coq_example*}

The syntax \texttt{:>} indicates that each \texttt{PreOrder} can be seen
as a \texttt{Reflexive} relation. So each time a reflexive relation is
needed, a preorder can be used instead. This is very similar to the
coercion mechanism of \texttt{Structure} declarations.
The implementation simply declares each projection as an instance. 

One can also declare existing objects or structure
projections using the \texttt{Existing Instance} command to achieve the 
same effect.

\section{Summary of the commands
\label{TypeClassCommands}}

\subsection{\tt Class {\ident} {\binder$_1$ \ldots~\binder$_n$} 
  : \sort := \{ field$_1$ ; \ldots ; field$_k$ \}.}
\comindex{Class}
\label{Class}

The \texttt{Class} command is used to declare a type class with
parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
{\tt field$_k$}.

\begin{Variants}
\item \label{SingletonClass} {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} 
    : \sort := \ident$_1$ : \type$_1$.}
  This variant declares a \emph{singleton} class whose only method is
  {\tt \ident$_1$}. This singleton class is a so-called definitional
  class, represented simply as a definition 
  {\tt {\ident} \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose
  instances are themselves objects of this type. Definitional classes
  are not wrapped inside records, and the trivial projection of an
  instance of such a class is convertible to the instance itself. This can
  be useful to make instances of existing objects easily and to reduce 
  proof size by not inserting useless projections. The class
  constant itself is declared rigid during resolution so that the class 
  abstraction is maintained.  

\item \label{ExistingClass} {\tt Existing Class {\ident}.\comindex{Existing Class}}
  This variant declares a class a posteriori from a constant or
  inductive definition. No methods or instances are defined.
\end{Variants}

\subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
  {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}]
  := \{ field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$ \}}
\comindex{Instance}
\label{Instance}

The \texttt{Instance} command is used to declare a type class instance
named {\ident} of the class \emph{Class} with parameters {t$_1$} to {t$_n$} and
fields {\tt b$_1$} to {\tt b$_i$}, where each field must be a declared
field of the class. Missing fields must be filled in interactive proof mode.

An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$}
can be put after the name of the instance and before the colon to
declare a parameterized instance.
An optional \textit{priority} can be declared, 0 being the highest
priority as for auto hints.

\begin{Variants}
\item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
    forall {\binder$_{n+1}$ \ldots \binder$_m$},
    {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term} 
  This syntax is used for declaration of singleton class instances or
  for directly giving an explicit term of type
  {\tt forall {\binder$_{n+1}$ \ldots \binder$_m$}, {Class} {t$_1$ \ldots t$_n$}}.
  One need not even mention the unique field name for singleton classes.

\item {\tt Global Instance} One can use the \texttt{Global} modifier on
  instances declared in a section so that their generalization is automatically
  redeclared after the section is closed.

\item {\tt Program Instance} \comindex{Program Instance}
  Switches the type-checking to \Program~(chapter \ref{Program})
  and uses the obligation mechanism to manage missing fields.

\item {\tt Declare Instance} \comindex{Declare Instance}
  In a {\tt Module Type}, this command states that a corresponding
  concrete instance should exist in any implementation of this
  {\tt Module Type}. This is similar to the distinction between
  {\tt Parameter} vs. {\tt Definition}, or between {\tt Declare Module}
  and {\tt Module}.

\end{Variants}

Besides the {\tt Class} and {\tt Instance} vernacular commands, there
are a few other commands related to type classes.

\subsection{\tt Existing Instance {\ident}}
\comindex{Existing Instance}
\label{ExistingInstance}

This commands adds an arbitrary constant whose type ends with an applied
type class to the instance database. It can be used for redeclaring
instances at the end of sections, or declaring structure projections as
instances. This is almost equivalent to {\tt Hint Resolve {\ident} :
  typeclass\_instances}.

\subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}}
\comindex{Context}
\label{Context}

Declares variables according to the given binding context, which might
use implicit generalization (see \ref{SectionContext}).

\subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}}
\comindex{Typeclasses Transparent}
\comindex{Typeclasses Opaque}
\label{TypeclassesTransparency}

This commands defines the transparency of {\ident$_1$ \ldots \ident$_n$} 
during type class resolution. It is useful when some constants prevent some
unifications and make resolution fail. It is also useful to declare
constants which should never be unfolded during proof-search, like
fixpoints or anything which does not look like an abbreviation. This can
additionally speed up proof search as the typeclass map can be indexed
by such rigid constants (see \ref{HintTransparency}).
By default, all constants and local variables are considered transparent.
One should take care not to make opaque any constant that is used to
abbreviate a type, like {\tt relation A := A -> A -> Prop}.

This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.

\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
\comindex{Typeclasses eauto}
\label{TypeclassesEauto}

This commands allows to customize the type class resolution tactic,
based on a variant of eauto. The flags semantics are:
\begin{itemize}
\item {\tt debug} In debug mode, the trace of successfully applied
  tactics is printed.
\item {\tt dfs, bfs} This sets the search strategy to depth-first search
  (the default) or breadth-first search.
\item {\emph{depth}} This sets the depth of the search (the default is 100).
\end{itemize}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: