\def\Haskell{\textsc{Haskell}\xspace}
\def\eol{\setlength\parskip{0pt}\par}
\def\indent#1{\noindent\kern#1}
\def\cst#1{\textsf{#1}}
\def\tele#1{\overrightarrow{#1}}

\achapter{\protect{Type Classes}}
\aauthor{Matthieu Sozeau}
\label{typeclasses}

\begin{flushleft}
  \em The status of Type Classes is (extremelly) 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 a mix between the
record syntax of \Coq~and the type classes syntax of \Haskell:
\def\kw{\texttt}
\def\classid{\texttt}

\begin{center}
\[\begin{array}{l}
\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n) :=\\
\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.
\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 : Type} [ 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{[ 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 : Type) (eqa : EqDec A) (x y : A) := negb (eqb x y).
\end{coq_example}

However, the bracketed 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 class arguments and
  partialy applied type classes (\S \ref{classes:impl-quant})
\item They support implicit quantification on superclasses (\S \ref{classes:superclasses})
\end{itemize}

\subsection{Implicit quantification}
\label{classes:impl-quant}

Implicit quantification is an automatic elaboration of a statement with
free variables into a closed statement where these variables are
quantified explicitely. Implicit generalization is done only inside
bracketed binders and the codomain of \texttt{Instance} declarations.

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 implicitely generalized, and the resulting function
is equivalent to the one above. One must be careful that \emph{all} the
free variables are generalized, which may result in confusing errors in
case of typos. In such cases, the context will probably contain some
unexpected generalized variable.

The bracket binders [ ] are a shorthand for double-braces \{\{ \}\} binders
which declare the variables directly bound inside them as implicit
(maximally-inserted) arguments, whereas double-parens (( )) brackets
declare them as explicit arguments. Implicitely generalized variables
are always set as maximally-inserted implicit arguments.

\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{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 (( E : EqDec A )) => Ord :=
  le : A -> A -> bool.
\end{coq_example}

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). One should always give a
name to each superclass, but one will be generated automatically if it
is missing.

Internally, \texttt{Ord} will become 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 class 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
explicitely 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.

One can notice that superclasses are in fact equivalent to parameters of
the class, hence the above declaration is the same as:
\begin{coq_example*}
Class Ord ((EqDec A)) := le : A -> A -> bool.
\end{coq_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. 
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$}. A optional context of the form {\tt \binder$_1$, \ldots
  \binder$_j$ :} can be put before the name of the class to declare
superclasses or other parameters.

\subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} : {Class} {t$_1$ \ldots t$_n$}
  := 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.

\begin{Variants}
\item {\tt Instance Global} 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.
\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 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"
%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
%%% End: 
