1 files changed, 412 insertions, 0 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
new file mode 100644
index 00000000..7bd4f352
--- /dev/null
+++ b/doc/refman/Classes.tex
@@ -0,0 +1,412 @@
+\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 (extremely) 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 (\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.
+
+\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: