diff options
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | doc/refman/Classes.tex | 578 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 587 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/replaces.rst | 8 |
7 files changed, 599 insertions, 580 deletions
diff --git a/Makefile.doc b/Makefile.doc index 4a247f1d9..2d2b21ad8 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -62,7 +62,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-pro.v.tex \ Coercion.v.tex Extraction.v.tex \ Program.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex Universes.v.tex \ + Setoid.v.tex Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex deleted file mode 100644 index da798a238..000000000 --- a/doc/refman/Classes.tex +++ /dev/null @@ -1,578 +0,0 @@ -\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}} -%HEVEA\cutname{type-classes.html} -\aauthor{Matthieu Sozeau} -\label{typeclasses} - -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 => eq_refl 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} -Fail 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 partially applied type - classes (\S \ref{implicit-generalization}). - Any argument not given as part of a type class binder will be - automatically generalized. -\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. - -\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 is possible to do it directly in regular -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. If the priority is not specified, it defaults to -$n$, the number of binders of the instance. - -\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} [| \textit{priority}]} -\comindex{Existing Instance} -\label{ExistingInstance} - -This commands adds an arbitrary constant whose type ends with an applied -type class to the instance database with an optional priority. 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}. - -\begin{Variants} -\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$ - [| \textit{priority}]} - \comindex{Existing Instances} - With this command, several existing instances can be declared at once. -\end{Variants} - -\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}). - -\asubsection{\tt typeclasses eauto} -\tacindex{typeclasses eauto} -\label{typeclasseseauto} - -The {\tt typeclasses eauto} tactic uses a different resolution engine -than {\tt eauto} and {\tt auto}. The main differences are the following: -\begin{itemize} -\item Contrary to {\tt eauto} and {\tt auto}, the resolution is done - entirely in the new proof engine (as of Coq v8.6), meaning that - backtracking is available among dependent subgoals, and shelving goals - is supported. {\tt typeclasses eauto} is a multi-goal tactic. - It analyses the dependencies between subgoals to avoid - backtracking on subgoals that are entirely independent. -\item When called with no arguments, {\tt typeclasses eauto} uses the - {\tt typeclass\_instances} database by default (instead of {\tt - core}). - Dependent subgoals are automatically shelved, and shelved - goals can remain after resolution ends (following the behavior of - \Coq{} 8.5). - - \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)} - faithfully mimicks what happens during typeclass resolution when it is - called during refinement/type-inference, except that \emph{only} - declared class subgoals are considered at the start of resolution - during type inference, while ``all'' can select non-class subgoals as - well. It might move to {\tt all:typeclasses eauto} in future versions - when the refinement engine will be able to backtrack. -\item When called with specific databases (e.g. {\tt with}), {\tt - typeclasses eauto} allows shelved goals to remain at any point - during search and treat typeclasses goals like any other. -\item The transparency information of databases is used consistently for - all hints declared in them. It is always used when calling the unifier. - When considering the local hypotheses, we use the transparent - state of the first hint database given. Using an empty database - (created with {\tt Create HintDb} for example) with - unfoldable variables and constants as the first argument of - typeclasses eauto hence makes resolution with the local hypotheses use - full conversion during unification. -\end{itemize} - -\begin{Variants} -\item \label{depth} {\tt typeclasses eauto \zeroone{\num}} - \emph{Warning:} The semantics for the limit {\num} is different than - for {\tt auto}. By default, if no limit is given the search is - unbounded. Contrary to {\tt auto}, introduction steps ({\tt intro}) - are counted, which might result in larger limits being necessary - when searching with {\tt typeclasses eauto} than {\tt auto}. - -\item \label{with} {\tt typeclasses eauto with {\ident}$_1$ \ldots {\ident}$_n$}. - This variant runs resolution with the given hint databases. It treats - typeclass subgoals the same as other subgoals (no shelving of - non-typeclass goals in particular). -\end{Variants} - -\asubsection{\tt autoapply {\term} with {\ident}} -\tacindex{autoapply} - -The tactic {\tt autoapply} applies a term using the transparency -information of the hint database {\ident}, and does \emph{no} typeclass -resolution. This can be used in {\tt Hint Extern}'s for typeclass -instances (in hint db {\tt typeclass\_instances}) to -allow backtracking on the typeclass subgoals created by the lemma -application, rather than doing type class resolution locally at the hint -application time. - -\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 Set Typeclasses Axioms Are Instances} -\optindex{Typeclasses Axioms Are Instances} - -This option (off by default since 8.8) automatically declares axioms -whose type is a typeclass at declaration time as instances of that -class. - -\subsection{\tt Set Typeclasses Dependency Order} -\optindex{Typeclasses Dependency Order} - -This option (on by default since 8.6) respects the dependency order between -subgoals, meaning that subgoals which are depended on by other subgoals -come first, while the non-dependent subgoals were put before the -dependent ones previously (Coq v8.5 and below). This can result in quite -different performance behaviors of proof search. - -\subsection{\tt Set Typeclasses Filtered Unification} -\optindex{Typeclasses Filtered Unification} - -This option, available since Coq 8.6 and off by default, switches the -hint application procedure to a filter-then-unify strategy. To apply a -hint, we first check that the goal \emph{matches} syntactically the -inferred or specified pattern of the hint, and only then try to -\emph{unify} the goal with the conclusion of the hint. This can -drastically improve performance by calling unification less often, -matching syntactic patterns being very quick. This also provides more -control on the triggering of instances. For example, forcing a constant -to explicitely appear in the pattern will make it never apply on a goal -where there is a hole in that place. - -\subsection{\tt Set Typeclasses Limit Intros} -\optindex{Typeclasses Limit Intros} - -This option (on by default) controls the ability to -apply hints while avoiding (functional) eta-expansions in the generated -proof term. It does so by allowing hints that conclude in a product to -apply to a goal with a matching product directly, avoiding an -introduction. \emph{Warning:} this can be expensive as it requires -rebuilding hint clauses dynamically, and does not benefit from the -invertibility status of the product introduction rule, resulting in -potentially more expensive proof-search (i.e. more useless -backtracking). - -\subsection{\tt Set Typeclass Resolution For Conversion} -\optindex{Typeclass Resolution For Conversion} - -This option (on by default) controls the use of typeclass resolution -when a unification problem cannot be solved during -elaboration/type-inference. With this option on, when a unification -fails, typeclass resolution is tried before launching unification once again. - -\subsection{\tt Set Typeclasses Strict Resolution} -\optindex{Typeclasses Strict Resolution} - -Typeclass declarations introduced when this option is set have a -stricter resolution behavior (the option is off by default). When -looking for unifications of a goal with an instance of this class, we -``freeze'' all the existentials appearing in the goals, meaning that -they are considered rigid during unification and cannot be instantiated. - -\subsection{\tt Set Typeclasses Unique Solutions} -\optindex{Typeclasses Unique Solutions} - -When a typeclass resolution is launched we ensure that it has a single -solution or fail. This ensures that the resolution is canonical, but can -make proof search much more expensive. - -\subsection{\tt Set Typeclasses Unique Instances} -\optindex{Typeclasses Unique Instances} - -Typeclass declarations introduced when this option is set have a -more efficient resolution behavior (the option is off by default). When -a solution to the typeclass goal of this class is found, we never -backtrack on it, assuming that it is canonical. - -\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]} -\comindex{Typeclasses eauto} -\label{TypeclassesEauto} - -This command allows more global customization of the type class -resolution tactic. -The semantics of the options 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 limit of the search. -\end{itemize} - -\subsection{\tt Set Typeclasses Debug [Verbosity {\num}]} -\optindex{Typeclasses Debug} -\optindex{Typeclasses Debug Verbosity} - -These options allow to see the resolution steps of typeclasses that are -performed during search. The {\tt Debug} option is synonymous to -{\tt Debug Verbosity 1}, and {\tt Debug Verbosity 2} provides more -information (tried tactics, shelving of goals, etc\ldots). - -\subsection{\tt Set Refine Instance Mode} -\optindex{Refine Instance Mode} - -The option {\tt Refine Instance Mode} allows to switch the behavior of instance -declarations made through the {\tt Instance} command. -\begin{itemize} -\item When it is on (the default), instances that have unsolved holes in their -proof-term silently open the proof mode with the remaining obligations to prove. -\item When it is off, they fail with an error instead. -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 86f123322..7ce28ccf8 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -118,7 +118,6 @@ Options A and B of the licence are {\em not} elected.} \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% \include{Coercion.v}% -\include{Classes.v}% \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst new file mode 100644 index 000000000..becebb421 --- /dev/null +++ b/doc/sphinx/addendum/type-classes.rst @@ -0,0 +1,587 @@ +.. include:: ../replaces.rst + +.. _typeclasses: + +Type Classes +============ + +:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html +:Author: Matthieu Sozeau + +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. + + +Class and Instance declarations +------------------------------- + +The syntax for class and instance declarations is the same as the record +syntax of Coq: + +``Class Id (`` |p_1| ``:`` |t_1| ``) ⋯ (`` |p_n| ``:`` |t_n| ``) [: +sort] := {`` |f_1| ``:`` |u_1| ``; ⋮`` |f_m| ``:`` |u_m| ``}.`` + +``Instance ident : Id`` |p_1| ``⋯`` |p_n| ``:= {`` |f_1| ``:=`` |t_1| ``; ⋮`` |f_m| ``:=`` |t_m| ``}.`` + +The |p_i| ``:`` |t_i| variables are called the *parameters* of the class and +the |f_i| ``:`` |t_i| are called the *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: + +.. coqtop:: in + + Class EqDec (A : Type) := { + eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true -> x = y }. + +This class implements a boolean equality test which is compatible with +Leibniz equality on some type. An example implementation is: + +.. coqtop:: in + + Instance unit_EqDec : EqDec unit := + { eqb x y := true ; + eqb_leibniz x y H := + match x, y return x = y with tt, tt => eq_refl tt end }. + +If one does not give all the members in the Instance declaration, Coq +enters the proof-mode and the user is asked to build inhabitants of +the remaining fields, e.g.: + +.. coqtop:: in + + Instance eq_bool : EqDec bool := + { eqb x y := if x then y else negb y }. + +.. coqtop:: all + + Proof. intros x y H. + +.. coqtop:: all + + destruct x ; destruct y ; (discriminate || reflexivity). + +.. coqtop:: all + + Defined. + +One has to take care that the transparency of every field is +determined by the transparency of the ``Instance`` proof. One can use +alternatively the ``Program Instance`` variant which has richer facilities +for dealing with obligations. + + +Binding classes +--------------- + +Once a type class is declared, one can use it in class binders: + +.. coqtop:: all + + Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y). + +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 ``EqDec A`` is generated and +satisfied by ``eqa : EqDec A``. In case no satisfying constraint can be +found, an error is raised: + +.. coqtop:: all + + Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). + +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 ``typeclass_instances`` database. Hence the example can also be +written: + +.. coqtop:: all + + Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). + +However, the generalizing binders should be used instead as they have +particular support for type classes: + ++ 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, ``A`` and ``eqa`` should be set maximally implicit. ++ They support implicit quantification on partially applied type + classes (:ref:`implicit-generalization`). Any argument not given as part of a type class + binder will be automatically generalized. ++ They also support implicit quantification on :ref:`superclasses`. + + +Following the previous example, one can write: + +.. coqtop:: all + + Generalizable Variables A B C. + + Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). + +Here ``A`` is implicitly generalized, and the resulting function is +equivalent to the one above. + +Parameterized Instances +----------------------- + +One can declare parameterized instances as in Haskell simply by giving +the constraints as a binding context before the instance, e.g.: + +.. coqtop:: in + + 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 }. + +.. coqtop:: none + + Abort. + +These instances are used just as well as lemmas in the instance hint +database. + +Sections and contexts +--------------------- + +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 ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it +accepts any binding context as argument. For example: + +.. coqtop:: all + + Section EqDec_defs. + + Context `{EA : EqDec A}. + + 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 }. + Admitted. + + End EqDec_defs. + + About option_eqb. + +Here the Global modifier redeclares the instance at the end of the +section, once it has been generalized by the context variables it +uses. + + +Building hierarchies +-------------------- + +.. _superclasses: + +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: + +.. coqtop:: all + + Class Ord `(E : EqDec A) := { le : A -> A -> bool }. + +Contrary to Haskell, we have no special syntax for superclasses, but +this declaration is morally equivalent to: + +:: + + Class `(E : EqDec A) => Ord A := + { le : A -> A -> bool }. + + +This declaration means that any instance of the ``Ord`` class must have +an instance of ``EqDec``. The parameters of the subclass contain at +least all the parameters of its superclasses in their order of +appearance (here A is the only one). As we have seen, ``Ord`` is encoded +as a record type with two parameters: a type ``A`` and an ``E`` of type +``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. + +.. coqtop:: all + + Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). + +In some cases, to be able to specify sharing of structures, one may +want to give explicitly the superclasses. It is is possible to do it +directly in regular binders, and using the ``!`` modifier in class +binders. For example: + +.. coqtop:: all + + Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). + +The ``!`` 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. + +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.: + +.. coqtop:: none + + Require Import Relation_Definitions. + +.. coqtop:: in + + 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. + +This declares singleton classes for reflexive and transitive relations, +(see the :ref:`singleton class <singleton-class>` variant for an +explanation). These may be used as part of other classes: + +.. coqtop:: all + + Class PreOrder (A : Type) (R : relation A) := + { PreOrder_Reflexive :> Reflexive A R ; + PreOrder_Transitive :> Transitive A R }. + +The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a +``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 ``Structure`` declarations. The implementation simply +declares each projection as an instance. + +One can also declare existing objects or structure projections using +the Existing Instance command to achieve the same effect. + + +Summary of the commands +----------------------- + + +.. _Class: + +.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }. + + The ``Class`` command is used to declare a type class with parameters + ``binders`` and fields the declared record fields. + +Variants: + +.. _singleton-class: + +.. cmd:: Class @ident {? @binders} : {? @sort} := @ident : @term + + This variant declares a *singleton* class with a single method. This + singleton class is a so-called definitional class, represented simply + as a definition ``ident binders := term`` 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. + +.. cmd:: Existing Class @ident + + This variant declares a class a posteriori from a constant or + inductive definition. No methods or instances are defined. + +.. _Instance: + +.. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } + +The ``Instance`` command is used to declare a type class instance named +``ident`` of the class ``Class`` with parameters ``t1`` to ``tn`` and +fields ``b1`` to ``bi``, where each field must be a declared field of +the class. Missing fields must be filled in interactive proof mode. + +An arbitrary context of ``binders`` can be put after the name of the +instance and before the colon to declare a parameterized instance. An +optional priority can be declared, 0 being the highest priority as for +auto hints. If the priority is not specified, it defaults to the number +of non-dependent binders of the instance. + +Variants: + + +.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term + + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type ``forall binders, Class + t1 … tn``. One need not even mention the unique field name for + singleton classes. + +.. cmd:: Global Instance + + One can use the ``Global`` modifier on instances declared in a + section so that their generalization is automatically redeclared + after the section is closed. + +.. cmd:: Program Instance + + Switches the type-checking to Program (chapter :ref:`program`) and + uses the obligation mechanism to manage missing fields. + +.. cmd:: Declare Instance + + In a Module Type, this command states that a corresponding concrete + instance should exist in any implementation of thisModule Type. This + is similar to the distinction betweenParameter vs. Definition, or + between Declare Module and Module. + + +Besides the ``Class`` and ``Instance`` vernacular commands, there are a +few other commands related to type classes. + +.. _ExistingInstance: + +Existing Instance +~~~~~~~~~~~~~~~~~ + +.. cmd:: Existing Instance {+ @ident} [| priority] + +This commands adds an arbitrary list of constants whose type ends with +an applied type class to the instance database with an optional +priority. It can be used for redeclaring instances at the end of +sections, or declaring structure projections as instances. This is +equivalent to ``Hint Resolve ident : typeclass_instances``, except it +registers instances for ``Print Instances``. + +.. _Context: + +Context +~~~~~~~ + +.. cmd:: Context @binders + +Declares variables according to the given binding context, which might +use :ref:`implicit-generalization`. + + +.. _typeclasses-eauto: + +``typeclasses eauto`` +~~~~~~~~~~~~~~~~~~~~~ + +The ``typeclasses eauto`` tactic uses a different resolution engine than +eauto and auto. The main differences are the following: + ++ Contrary to ``eauto`` and ``auto``, the resolution is done entirely in + the new proof engine (as of Coq v8.6), meaning that backtracking is + available among dependent subgoals, and shelving goals is supported. + typeclasses eauto is a multi-goal tactic. It analyses the dependencies + between subgoals to avoid backtracking on subgoals that are entirely + independent. + ++ When called with no arguments, typeclasses eauto uses + thetypeclass_instances database by default (instead of core). + Dependent subgoals are automatically shelved, and shelved goals can + remain after resolution ends (following the behavior ofCoq 8.5). + *Note: * As of Coq 8.6, all:once (typeclasses eauto) faithfully + mimicks what happens during typeclass resolution when it is called + during refinement/type-inference, except that *only* declared class + subgoals are considered at the start of resolution during type + inference, while “all” can select non-class subgoals as well. It might + move to ``all:typeclasses eauto`` in future versions when the + refinement engine will be able to backtrack. + ++ When called with specific databases (e.g. with), typeclasses eauto + allows shelved goals to remain at any point during search and treat + typeclasses goals like any other. + ++ The transparency information of databases is used consistently for + all hints declared in them. It is always used when calling the + unifier. When considering the local hypotheses, we use the transparent + state of the first hint database given. Using an empty database + (created with Create HintDb for example) with unfoldable variables and + constants as the first argument of typeclasses eauto hence makes + resolution with the local hypotheses use full conversion during + unification. + + +Variants: + +#. ``typeclasses eauto [num]`` + + *Warning:* The semantics for the limit num + is different than for auto. By default, if no limit is given the + search is unbounded. Contrary to auto, introduction steps (intro) are + counted, which might result in larger limits being necessary when + searching with typeclasses eauto than auto. + +#. ``typeclasses eauto with {+ @ident}`` + + This variant runs resolution with the given hint databases. It treats + typeclass subgoals the same as other subgoals (no shelving of + non-typeclass goals in particular). + +.. _autoapply: + +``autoapply term with ident`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The tactic autoapply applies a term using the transparency information +of the hint database ident, and does *no* typeclass resolution. This can +be used in ``Hint Extern``’s for typeclass instances (in the hint +database ``typeclass_instances``) to allow backtracking on the typeclass +subgoals created by the lemma application, rather than doing type class +resolution locally at the hint application time. + +.. _TypeclassesTransparent: + +Typeclasses Transparent, Typclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} + + This commands defines the transparency of the given identifiers + 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:`thehintsdatabasesforautoandeauto`). 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: + +:: + + relation A := A -> A -> Prop. + +This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. + + +Set Typeclasses Dependency Order +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This option (on by default since 8.6) respects the dependency order +between subgoals, meaning that subgoals which are depended on by other +subgoals come first, while the non-dependent subgoals were put before +the dependent ones previously (Coq v8.5 and below). This can result in +quite different performance behaviors of proof search. + + +Set Typeclasses Filtered Unification +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This option, available since Coq 8.6 and off by default, switches the +hint application procedure to a filter-then-unify strategy. To apply a +hint, we first check that the goal *matches* syntactically the +inferred or specified pattern of the hint, and only then try to +*unify* the goal with the conclusion of the hint. This can drastically +improve performance by calling unification less often, matching +syntactic patterns being very quick. This also provides more control +on the triggering of instances. For example, forcing a constant to +explicitely appear in the pattern will make it never apply on a goal +where there is a hole in that place. + + +Set Typeclasses Limit Intros +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + +This option (on by default) controls the ability to apply hints while +avoiding (functional) eta-expansions in the generated proof term. It +does so by allowing hints that conclude in a product to apply to a +goal with a matching product directly, avoiding an introduction. +*Warning:* this can be expensive as it requires rebuilding hint +clauses dynamically, and does not benefit from the invertibility +status of the product introduction rule, resulting in potentially more +expensive proof-search (i.e. more useless backtracking). + + +Set Typeclass Resolution For Conversion +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This option (on by default) controls the use of typeclass resolution +when a unification problem cannot be solved during elaboration/type- +inference. With this option on, when a unification fails, typeclass +resolution is tried before launching unification once again. + + +Set Typeclasses Strict Resolution +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Typeclass declarations introduced when this option is set have a +stricter resolution behavior (the option is off by default). When +looking for unifications of a goal with an instance of this class, we +“freeze” all the existentials appearing in the goals, meaning that +they are considered rigid during unification and cannot be +instantiated. + + +Set Typeclasses Unique Solutions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When a typeclass resolution is launched we ensure that it has a single +solution or fail. This ensures that the resolution is canonical, but +can make proof search much more expensive. + + +Set Typeclasses Unique Instances +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Typeclass declarations introduced when this option is set have a more +efficient resolution behavior (the option is off by default). When a +solution to the typeclass goal of this class is found, we never +backtrack on it, assuming that it is canonical. + + +Typeclasses eauto `:=` +~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth + + This command allows more global customization of the type class + resolution tactic. The semantics of the options are: + + + ``debug`` In debug mode, the trace of successfully applied tactics is + printed. + + + ``dfs, bfs`` This sets the search strategy to depth-first search (the + default) or breadth-first search. + + + ``depth`` This sets the depth limit of the search. + + +Set Typeclasses Debug +~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Set Typeclasses Debug {? Verbosity @num} + +These options allow to see the resolution steps of typeclasses that are +performed during search. The ``Debug`` option is synonymous to ``Debug +Verbosity 1``, and ``Debug Verbosity 2`` provides more information +(tried tactics, shelving of goals, etc…). + + +Set Refine Instance Mode +~~~~~~~~~~~~~~~~~~~~~~~~ + +The option Refine Instance Mode allows to switch the behavior of +instance declarations made through the Instance command. + ++ When it is on (the default), instances that have unsolved holes in + their proof-term silently open the proof mode with the remaining + obligations to prove. + ++ When it is off, they fail with an error instead. diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index c5d4936b1..cf64aea03 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -45,6 +45,7 @@ Table of contents addendum/extended-pattern-matching addendum/canonical-structures + addendum/type-classes addendum/omega addendum/micromega diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index d618d90ad..68066faa3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2109,6 +2109,8 @@ case, this latter type is considered). Adds blocks of implicit types with different specifications. +.. _implicit-generalization: + Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst index d4f6835ef..1b2e17221 100644 --- a/doc/sphinx/replaces.rst +++ b/doc/sphinx/replaces.rst @@ -64,6 +64,14 @@ .. |t_i| replace:: `t`\ :math:`_{i}` .. |t_m| replace:: `t`\ :math:`_{m}` .. |t_n| replace:: `t`\ :math:`_{n}` +.. |f_1| replace:: `f`\ :math:`_{1}` +.. |f_i| replace:: `f`\ :math:`_{i}` +.. |f_m| replace:: `f`\ :math:`_{m}` +.. |f_n| replace:: `f`\ :math:`_{n}` +.. |u_1| replace:: `u`\ :math:`_{1}` +.. |u_i| replace:: `u`\ :math:`_{i}` +.. |u_m| replace:: `u`\ :math:`_{m}` +.. |u_n| replace:: `u`\ :math:`_{n}` .. |term_0| replace:: `term`\ :math:`_{0}` .. |term_1| replace:: `term`\ :math:`_{1}` .. |term_2| replace:: `term`\ :math:`_{2}` |