1
\achapter{Implicit Coercions}
2
\aauthor{Amokrane Sa�bi}
5
\index{Coercions!presentation}
7
\asection{General Presentation}
9
This section describes the inheritance mechanism of {\Coq}. In {\Coq} with
10
inheritance, we are not interested in adding any expressive power to
11
our theory, but only convenience. Given a term, possibly not typable,
12
we are interested in the problem of determining if it can be well
13
typed modulo insertion of appropriate coercions. We allow to write:
16
\item $f~a$ where $f:forall~ x:A, B$ and $a:A'$ when $A'$ can
17
be seen in some sense as a subtype of $A$.
18
\item $x:A$ when $A$ is not a type, but can be seen in
19
a certain sense as a type: set, group, category etc.
20
\item $f~a$ when $f$ is not a function, but can be seen in a certain sense
21
as a function: bijection, functor, any structure morphism etc.
25
\index{Coercions!classes}
26
A class with $n$ parameters is any defined name with a type
27
$forall~ (x_1:A_1)..(x_n:A_n), s$ where $s$ is a sort. Thus a class with
28
parameters is considered as a single class and not as a family of
29
classes. An object of a class $C$ is any term of type $C~t_1
30
.. t_n$. In addition to these user-classes, we have two abstract
34
\item {\tt Sortclass}, the class of sorts;
35
its objects are the terms whose type is a sort.
36
\item {\tt Funclass}, the class of functions;
37
its objects are all the terms with a functional
38
type, i.e. of form $forall~ x:A, B$.
41
Formally, the syntax of a classes is defined on Figure~\ref{fig:classes}.
45
{\class} & ::= & {\qualid} \\
46
& $|$ & {\tt Sortclass} \\
47
& $|$ & {\tt Funclass}
50
\caption{Syntax of classes}
55
\index{Coercions!Funclass}
56
\index{Coercions!Sortclass}
57
A name $f$ can be declared as a coercion between a source user-class
58
$C$ with $n$ parameters and a target class $D$ if one of these
61
\newcommand{\oftype}{\!:\!}
64
\item $D$ is a user-class, then the type of $f$ must have the form
65
$forall~ (x_1 \oftype A_1)..(x_n \oftype A_n)(y\oftype C~x_1..x_n), D~u_1..u_m$ where $m$
66
is the number of parameters of $D$.
67
\item $D$ is {\tt Funclass}, then the type of $f$ must have the form
68
$forall~ (x_1\oftype A_1)..(x_n\oftype A_n)(y\oftype C~x_1..x_n)(x:A), B$.
69
\item $D$ is {\tt Sortclass}, then the type of $f$ must have the form
70
$forall~ (x_1\oftype A_1)..(x_n\oftype A_n)(y\oftype C~x_1..x_n), s$ with $s$ a sort.
73
We then write $f:C \mbox{\texttt{>->}} D$. The restriction on the type
74
of coercions is called {\em the uniform inheritance condition}.
75
Remark that the abstract classes {\tt Funclass} and {\tt Sortclass}
76
cannot be source classes.
78
To coerce an object $t:C~t_1..t_n$ of $C$ towards $D$, we have to
79
apply the coercion $f$ to it; the obtained term $f~t_1..t_n~t$ is
80
then an object of $D$.
82
\asection{Identity Coercions}
83
\index{Coercions!identity}
85
Identity coercions are special cases of coercions used to go around
86
the uniform inheritance condition. Let $C$ and $D$ be two classes
87
with respectively $n$ and $m$ parameters and
88
$f:forall~(x_1:T_1)..(x_k:T_k)(y:C~u_1..u_n), D~v_1..v_m$ a function which
89
does not verify the uniform inheritance condition. To declare $f$ as
90
coercion, one has first to declare a subclass $C'$ of $C$:
92
$$C' := fun~ (x_1:T_1)..(x_k:T_k) => C~u_1..u_n$$
94
\noindent We then define an {\em identity coercion} between $C'$ and $C$:
96
Id\_C'\_C & := & fun~ (x_1:T_1)..(x_k:T_k)(y:C'~x_1..x_k) => (y:C~u_1..u_n)\\
99
We can now declare $f$ as coercion from $C'$ to $D$, since we can
101
$forall~ (x_1:T_1)..(x_k:T_k)(y:C'~x_1..x_k),D~v_1..v_m$.\\ The identity
102
coercions have a special status: to coerce an object $t:C'~t_1..t_k$
103
of $C'$ towards $C$, we does not have to insert explicitly $Id\_C'\_C$
104
since $Id\_C'\_C~t_1..t_k~t$ is convertible with $t$. However we
105
``rewrite'' the type of $t$ to become an object of $C$; in this case,
106
it becomes $C~u_1^*..u_k^*$ where each $u_i^*$ is the result of the
107
substitution in $u_i$ of the variables $x_j$ by $t_j$.
110
\asection{Inheritance Graph}
111
\index{Coercions!inheritance graph}
112
Coercions form an inheritance graph with classes as nodes. We call
113
{\em coercion path} an ordered list of coercions between two nodes of
114
the graph. A class $C$ is said to be a subclass of $D$ if there is a
115
coercion path in the graph from $C$ to $D$; we also say that $C$
116
inherits from $D$. Our mechanism supports multiple inheritance since a
117
class may inherit from several classes, contrary to simple inheritance
118
where a class inherits from at most one class. However there must be
119
at most one path between two classes. If this is not the case, only
120
the {\em oldest} one is valid and the others are ignored. So the order
121
of declaration of coercions is important.
123
We extend notations for coercions to coercion paths. For instance
124
$[f_1;..;f_k]:C \mbox{\texttt{>->}} D$ is the coercion path composed
125
by the coercions $f_1..f_k$. The application of a coercion path to a
126
term consists of the successive application of its coercions.
128
\asection{Declaration of Coercions}
130
%%%%% "Class" is useless, since classes are implicitely defined via coercions.
132
% \asubsection{\tt Class {\qualid}.}\comindex{Class}
133
% Declares {\qualid} as a new class.
136
% \item {\qualid} \errindex{not declared}
137
% \item {\qualid} \errindex{is already a class}
138
% \item \errindex{Type of {\qualid} does not end with a sort}
142
% \item {\tt Class Local {\qualid}.} \\
143
% Declares the construction denoted by {\qualid} as a new local class to
144
% the current section.
147
% END "Class" is useless
149
\asubsection{\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
152
Declares the construction denoted by {\qualid} as a coercion between
153
{\class$_1$} and {\class$_2$}.
155
% Useless information
156
% The classes {\class$_1$} and {\class$_2$} are first declared if necessary.
159
\item {\qualid} \errindex{not declared}
160
\item {\qualid} \errindex{is already a coercion}
161
\item \errindex{Funclass cannot be a source class}
162
\item \errindex{Sortclass cannot be a source class}
163
\item {\qualid} \errindex{is not a function}
164
\item \errindex{Cannot find the source class of {\qualid}}
165
\item \errindex{Cannot recognize {\class$_1$} as a source class of {\qualid}}
166
\item {\qualid} \errindex{does not respect the inheritance uniform condition}
167
\item \errindex{Found target class {\class} instead of {\class$_2$}}
171
When the coercion {\qualid} is added to the inheritance graph, non
172
valid coercion paths are ignored; they are signaled by a warning.
174
\noindent {\bf Warning :}
176
\item \begin{tabbing}
177
{\tt Ambiguous paths: }\= $[f_1^1;..;f_{n_1}^1] : C_1\mbox{\tt >->}D_1$\\
179
\>$[f_1^m;..;f_{n_m}^m] : C_m\mbox{\tt >->}D_m$
184
\item {\tt Local Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
185
\comindex{Local Coercion}\\
186
Declares the construction denoted by {\qualid} as a coercion local to
189
\item {\tt Coercion {\ident} := {\term}}\comindex{Coercion}\\
190
This defines {\ident} just like \texttt{Definition {\ident} :=
191
{\term}}, and then declares {\ident} as a coercion between it
192
source and its target.
194
\item {\tt Coercion {\ident} := {\term} : {\type}}\\
195
This defines {\ident} just like
196
\texttt{Definition {\ident} : {\type} := {\term}}, and then
197
declares {\ident} as a coercion between it source and its target.
199
\item {\tt Local Coercion {\ident} := {\term}}\comindex{Local Coercion}\\
200
This defines {\ident} just like \texttt{Let {\ident} :=
201
{\term}}, and then declares {\ident} as a coercion between it
202
source and its target.
204
\item Assumptions can be declared as coercions at declaration
205
time. This extends the grammar of declarations from Figure
206
\ref{sentences-syntax} as follows:
207
\comindex{Variable \mbox{\rm (and coercions)}}
208
\comindex{Axiom \mbox{\rm (and coercions)}}
209
\comindex{Parameter \mbox{\rm (and coercions)}}
210
\comindex{Hypothesis \mbox{\rm (and coercions)}}
214
{\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\
216
{\assums} & ::= & {\simpleassums} \\
217
& $|$ & \nelist{{\tt (} \simpleassums {\tt )}}{} \\
219
{\simpleassums} & ::= & \nelist{\ident}{} {\tt :}\zeroone{{\tt >}} {\term}\\
222
If the extra {\tt >} is present before the type of some assumptions, these
223
assumptions are declared as coercions.
225
\item Constructors of inductive types can be declared as coercions at
226
definition time of the inductive type. This extends and modifies the
227
grammar of inductive types from Figure \ref{sentences-syntax} as follows:
228
\comindex{Inductive \mbox{\rm (and coercions)}}
229
\comindex{CoInductive \mbox{\rm (and coercions)}}
235
{\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
236
& $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
238
{\inductivebody} & ::= &
239
{\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\
240
&& ~~~\zeroone{\zeroone{\tt |} \nelist{\constructor}{|}} \\
242
{\constructor} & ::= & {\ident} \sequence{\binderlet}{} \zeroone{{\tt :}\zeroone{\tt >} {\term}} \\
246
Especially, if the extra {\tt >} is present in a constructor
247
declaration, this constructor is declared as a coercion.
250
\asubsection{\tt Identity Coercion {\ident}:{\class$_1$} >-> {\class$_2$}.}
251
\comindex{Identity Coercion}
253
We check that {\class$_1$} is a constant with a value of the form
254
$fun~ (x_1:T_1)..(x_n:T_n) => (\mbox{\class}_2~t_1..t_m)$ where $m$ is the
255
number of parameters of \class$_2$. Then we define an identity
256
function with the type
257
$forall~ (x_1:T_1)..(x_n:T_n)(y:\mbox{\class}_1~x_1..x_n),
258
{\mbox{\class}_2}~t_1..t_m$, and we declare it as an identity
259
coercion between {\class$_1$} and {\class$_2$}.
262
\item {\class$_1$} \errindex{must be a transparent constant}
266
\item {\tt Local Identity Coercion {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\
267
Idem but locally to the current section.
269
\item {\tt SubClass {\ident} := {\type}.} \\
271
If {\type} is a class
272
{\ident'} applied to some arguments then {\ident} is defined and an
273
identity coercion of name {\tt Id\_{\ident}\_{\ident'}} is
274
declared. Otherwise said, this is an abbreviation for
276
{\tt Definition {\ident} := {\type}.}
280
{\tt Identity Coercion Id\_{\ident}\_{\ident'}:{\ident} >-> {\ident'}}.
282
\item {\tt Local SubClass {\ident} := {\type}.} \\
283
Same as before but locally to the current section.
287
\asection{Displaying Available Coercions}
289
\asubsection{\tt Print Classes.}
290
\comindex{Print Classes}
291
Print the list of declared classes in the current context.
293
\asubsection{\tt Print Coercions.}
294
\comindex{Print Coercions}
295
Print the list of declared coercions in the current context.
297
\asubsection{\tt Print Graph.}
298
\comindex{Print Graph}
299
Print the list of valid coercion paths in the current context.
301
\asubsection{\tt Print Coercion Paths {\class$_1$} {\class$_2$}.}
302
\comindex{Print Coercion Paths}
303
Print the list of valid coercion paths from {\class$_1$} to {\class$_2$}.
305
\asection{Activating the Printing of Coercions}
307
\asubsection{\tt Set Printing Coercions.}
308
\comindex{Set Printing Coercions}
309
\comindex{Unset Printing Coercions}
311
This command forces all the coercions to be printed.
312
Conversely, to skip the printing of coercions, use
313
{\tt Unset Printing Coercions}.
314
By default, coercions are not printed.
316
\asubsection{\tt Set Printing Coercion {\qualid}.}
317
\comindex{Set Printing Coercion}
318
\comindex{Unset Printing Coercion}
320
This command forces coercion denoted by {\qualid} to be printed.
321
To skip the printing of coercion {\qualid}, use
322
{\tt Unset Printing Coercion {\qualid}}.
323
By default, a coercion is never printed.
325
\asection{Classes as Records}
326
\label{Coercions-and-records}
327
\index{Coercions!and records}
328
We allow the definition of {\em Structures with Inheritance} (or
329
classes as records) by extending the existing {\tt Record} macro
330
(see Section~\ref{Record}). Its new syntax is:
334
{\tt Record \zeroone{>}~{\ident} {\binderlet} : {\sort} := \zeroone{\ident$_0$} \verb+{+} \\
335
~~~~\begin{tabular}{l}
336
{\tt \ident$_1$ $[$:$|$:>$]$ \term$_1$ ;} \\
338
{\tt \ident$_n$ $[$:$|$:>$]$ \term$_n$ \verb+}+. }
342
The identifier {\ident} is the name of the defined record and {\sort}
343
is its type. The identifier {\ident$_0$} is the name of its
344
constructor. The identifiers {\ident$_1$}, .., {\ident$_n$} are the
345
names of its fields and {\term$_1$}, .., {\term$_n$} their respective
346
types. The alternative {\tt $[$:$|$:>$]$} is ``{\tt :}'' or ``{\tt
347
:>}''. If {\tt {\ident$_i$}:>{\term$_i$}}, then {\ident$_i$} is
348
automatically declared as coercion from {\ident} to the class of
349
{\term$_i$}. Remark that {\ident$_i$} always verifies the uniform
350
inheritance condition. If the optional ``{\tt >}'' before {\ident} is
351
present, then {\ident$_0$} (or the default name {\tt Build\_{\ident}}
352
if {\ident$_0$} is omitted) is automatically declared as a coercion
353
from the class of {\term$_n$} to {\ident} (this may fail if the
354
uniform inheritance condition is not satisfied).
356
\Rem The keyword {\tt Structure}\comindex{Structure} is a synonym of {\tt
359
\asection{Coercions and Sections}
360
\index{Coercions!and sections}
361
The inheritance mechanism is compatible with the section
362
mechanism. The global classes and coercions defined inside a section
363
are redefined after its closing, using their new value and new
364
type. The classes and coercions which are local to the section are
366
Coercions with a local source class or a local target class, and
367
coercions which do not verify the uniform inheritance condition any longer
372
There are three situations:
375
\item $f~a$ is ill-typed where $f:forall~x:A,B$ and $a:A'$. If there is a
376
coercion path between $A'$ and $A$, $f~a$ is transformed into
377
$f~a'$ where $a'$ is the result of the application of this
378
coercion path to $a$.
380
We first give an example of coercion between atomic inductive types
384
Definition bool_in_nat (b:bool) := if b then 0 else 1.
385
Coercion bool_in_nat : bool >-> nat.
387
Set Printing Coercions.
393
Unset Printing Coercions.
396
\Warning ``\verb|Check true=O.|'' fails. This is ``normal'' behaviour of
397
coercions. To validate \verb|true=O|, the coercion is searched from
398
\verb=nat= to \verb=bool=. There is none.
400
We give an example of coercion between classes with parameters.
405
(C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
406
Parameter f : forall n:nat, C n -> D (S n) true.
407
Coercion f : C >-> D.
408
Parameter g : forall (n:nat) (b:bool), D n b -> E b.
409
Coercion g : D >-> E.
411
Parameter T : E true -> nat.
413
Set Printing Coercions.
419
Unset Printing Coercions.
422
We give now an example using identity coercions.
426
Definition D' (b:bool) := D 1 b.
427
Identity Coercion IdD'D : D' >-> D.
429
Parameter d' : D' true.
431
Set Printing Coercions.
437
Unset Printing Coercions.
441
In the case of functional arguments, we use the monotonic rule of
442
sub-typing. Approximatively, to coerce $t:forall~x:A, B$ towards
443
$forall~x:A',B'$, one have to coerce $A'$ towards $A$ and $B$ towards
444
$B'$. An example is given below:
448
Parameters (A B : Set) (h : A -> B).
449
Coercion h : A >-> B.
450
Parameter U : (A -> E true) -> nat.
451
Parameter t : B -> C 0.
453
Set Printing Coercions.
459
Unset Printing Coercions.
462
Remark the changes in the result following the modification of the
467
Parameter U' : (C 0 -> B) -> nat.
468
Parameter t' : E true -> A.
470
Set Printing Coercions.
476
Unset Printing Coercions.
479
\item An assumption $x:A$ when $A$ is not a type, is ill-typed. It is
480
replaced by $x:A'$ where $A'$ is the result of the application
481
to $A$ of the coercion path between the class of $A$ and {\tt
482
Sortclass} if it exists. This case occurs in the abstraction
483
$fun~ x:A => t$, universal quantification $forall~x:A, B$,
484
global variables and parameters of (co-)inductive definitions
485
and functions. In $forall~x:A, B$, such a coercion path may be
486
applied to $B$ also if necessary.
490
Parameter Graph : Type.
491
Parameter Node : Graph -> Type.
492
Coercion Node : Graph >-> Sortclass.
494
Parameter Arrows : G -> G -> Type.
496
Parameter fg : G -> G.
498
Set Printing Coercions.
504
Unset Printing Coercions.
507
\item $f~a$ is ill-typed because $f:A$ is not a function. The term
508
$f$ is replaced by the term obtained by applying to $f$ the
509
coercion path between $A$ and {\tt Funclass} if it exists.
513
Parameter bij : Set -> Set -> Set.
514
Parameter ap : forall A B:Set, bij A B -> A -> B.
515
Coercion ap : bij >-> Funclass.
516
Parameter b : bij nat nat.
518
Set Printing Coercions.
524
Unset Printing Coercions.
527
Let us see the resulting graph of this session.
540
%%% TeX-master: "Reference-Manual"
added
removed
doc/refman/Coercion.tex
