diff options
| -rw-r--r-- | doc/refman/Universes.tex | 74 |
1 files changed, 72 insertions, 2 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 288d7c910..7de74ef95 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -56,20 +56,90 @@ Print selfpid. \end{coq_example} Now \texttt{pidentity} is used at two different levels: at the head of -the application is is instantiated at \texttt{Top.3} while in the +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. -Polymorphic constants, inductive +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: |