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
|
\achapter{Polymorphic Universes}
\aauthor{Matthieu Sozeau}
\label{Universes-full}
\index{Universes!presentation}
\asection{General Presentation}
This section describes the universe polymorphic extension of Coq.
Universe polymorphism allows writing generic definitions making use of
universes and reuse them at different and sometimes incompatible levels.
A standard example of the difference between universe \emph{polymorphic} and
\emph{monormorphic} definitions is given by the identity function:
\begin{coq_example*}
Definition identity {A : Type} (a : A) := a.
\end{coq_example*}
By default, constant declarations are monomorphic, hence the identity
function declares a global universe (say \texttt{Top.1}) for its
domain. Subsequently, if we try to self-apply the identity, we will get
an error:
\begin{coq_eval}
Set Printing Universes.
\end{coq_eval}
\begin{coq_example}
Fail Definition selfid := identity (@identity).
\end{coq_example}
Indeed, the global level \texttt{Top.1} would have to be strictly smaller than itself
for this self-application to typecheck, as the type of (@identity) is
\texttt{forall (A : Type@{Top.1}), A -> A} whose type is itself \texttt{Type@{Top.1+1}}.
A universe polymorphic identity function binds its domain universe level
at the definition level instead of making it global.
\begin{coq_example}
Polymorphic Definition pidentity {A : Type} (a : A) := a.
About pidentity.
\end{coq_example}
It is then possible to reuse the constant at different levels, like so:
\begin{coq_example}
Definition selfpid := pidentity (@pidentity).
\end{coq_example}
Of course, the two instances of \texttt{pidentity} in this definition
are different. This can be seen when \texttt{Set Printing Universes} is
on:
\begin{coq_example}
Print selfpid.
\end{coq_example}
Now \texttt{pidentity} is used at two different levels: at the head of
the application it is instantiated at \texttt{Top.3} while in the
argument position it is instantiated at \texttt{Top.4}. This definition
is only valid as long as \texttt{Top.4} is strictly smaller than
\texttt{Top.3}, as show by the constraints. Not that this definition is
monomorphic (not universe polymorphic), so in turn the two universes are
actually global levels.
Inductive types can also be declared universes polymorphic, on universes
appearing in their parameters or fields. A typical example is given by
monoids:
\begin{coq_example}
Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car;
mon_op : mon_car -> mon_car -> mon_car }.
Print Monoid.
\end{coq_example}
The \texttt{Monoid}'s carrier universe is polymorphic, hence it is
possible to instantiate it for example with \texttt{Monoid} itself.
First we build the trivial unit monoid, in \texttt{Set}:
\begin{coq_example}
Definition unit_monoid : Monoid :=
{| mon_car := unit; mon_unit := tt; mon_op x y := tt |}.
\end{coq_example}
From this we can build a definition for the monoid of
\texttt{Set}-monoids (where multiplication would be given by the product
of monoids).
\begin{coq_example}
Polymorphic Definition monoid_monoid : Monoid.
refine (@Build_Monoid Monoid unit_monoid _) ; admit.
Defined.
Print monoid_monoid.
\end{coq_example}
As one can see from the constraints, this monoid is ``large'', it lives
in a universe strictly higher than \texttt{Set}.
\asubsection{\tt Polymorphic, Monomorphic}
\comindex{Polymorphic}
\comindex{Monomorphic}
\comindex{Set Universe Polymorphism}
As shown in the examples, polymorphic definitions and inductives can be
declared using the \texttt{Polymorphic} prefix. There also exists an
option \texttt{Set Universe Polymorphism} which will implicitely prepend
it to any definition of the user. In that case, to make a definition
producing global universe constraints, one can use the
\texttt{Monomorphic} prefix. Many other commands support the
\texttt{Polymorphic} flag, including:
\begin{itemize}
\item \texttt{Lemma}, \texttt{Axiom}, \ldots. All ``definition''
keywords support polymorphism.
\item \texttt{Variables, Context} in a section, this means that the
variables are discharged polymorphically over definitions that use
them. In other words, two definitions in the section sharing a common
variable will both get parameterized by the universes produced by the
variable declaration. This is in contrast to a ``mononorphic'' variable
which introduce global universes, making the two definitions depend on
the \emph{same} universes associated to the variable.
\item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint
polymorphically, not at a single instance.
\end{itemize}
\asubsection{Conversion and unification}
The semantics of conversion and unification have to be modified a little
bit to account for the new universe instance arguments to polymorphic
references. The semantics respect the fact that definitions are
transparent, so undistinguishable from their bodies during conversion.
This is accomplished by changing one rule of unification, the
first-order approximation rule:
\asubsection{Explicit Universes}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
