<commit_before>\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{<NAME>}
\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{multicols}{2}{
\medskip
  \kw{Class} \classid{Id} $(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n)$ :=
  \eol\indent{3.00em}$\cst{f}_1 : \phi_1$ ;
  \eol\indent{4.00em}\vdots
  \eol\indent{3.00em}$\cst{f}_m : \phi_m$.
\medskip}
{
 
  \medskip
  \kw{Instance} \classid{Id} $t_1 \cdots t_n$ :=
  \eol\indent{3.00em}$\cst{f}_1 := b_1$ ;
  \eol\indent{4.00em}\vdots
  \eol\indent{3.00em}$\cst{f}_m := b_m$.
  \medskip}
\end{multicols}

\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 : \phi_k}$ are called the
\emph{methods}. Each class definition gives rise to a corresponding
record declaration and each instance is a regular definition whose 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 Eq (A : Type) :=
  eq : A -> A -> bool ;
  eq_leibniz : forall x y, eq 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 Eq unit :=
  eq x y := true ;
  eq_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 : Eq bool :=
  eq x y := if x then y else negb y.
\end{coq_example*}

\begin{coq_example}
  Proof. intros x y H.
  destruct x ; destruct y ; try 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 neq {A : Type} [ Eq A ] (x y : A) := negb (eq 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{Eq A} is generated and
satisfied by \texttt{[ Eq A ]}. In case no satisfying constraint can be
found, an error is raised:

\begin{coq_example}
  Definition neq' (A : Type) (x y : A) := negb (eq 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 neq' (A : Type) (eqa : Eq A) (x y : A) := negb (eq 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:implicitquant}
\item They support implicit quantification on superclasses (see section
  \S \ref{classes:superclasses}
\end{itemize}

\subsection{Implicit quantification}

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.

Following the previous example, one can write:
\begin{coq_example}
  Definition neq_impl [ eqa : Eq A ] (x y : A) := negb (eq 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. 

\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 [ eqa : Eq A, eqb : Eq B ] => prod_eq : Eq (A * B) :=
  eq x y := match x, y with
  | (la, ra), (lb, rb) => andb (eq la lb) (eq ra rb)
  end.
\end{coq_example*}
\begin{coq_eval}
Admitted.
\end{coq_eval}

These instances are used just as well as lemmas in the instances hint database.

\asection{Building hierarchies}

\subsection{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 [ eqa : Eq 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{Eq}. The parameters of the subclass contains
at least all the parameters of its superclasses in their order of<commit_msg>Second pass on typeclasses documentation, fix html rendering.<commit_after>\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{<NAME>}
\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 Eq (A : Type) :=
  eq : A -> A -> bool ;
  eq_leibniz : forall x y, eq 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_Eq : Eq unit :=
  eq x y := true ;
  eq_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 : Eq bool :=
  eq x y := if x then y else negb y.
\end{coq_example*}

\begin{coq_example}
  Proof. intros x y H.
  destruct x ; destruct y ; try 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 neq {A : Type} [ Eq A ] (x y : A) := negb (eq 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{Eq A} is generated and
satisfied by \texttt{[ Eq A ]}. In case no satisfying constraint can be
found, an error is raised:

\begin{coq_example}
  Definition neq' (A : Type) (x y : A) := negb (eq 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 neq' (A : Type) (eqa : Eq A) (x y : A) := negb (eq 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.

Following the previous example, one can write:
\begin{coq_example}
  Definition neq_impl [ eqa : Eq A ] (x y : A) := negb (eq 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. 

\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_eq [ eqa : Eq A, eqb : Eq B ] : Eq (A * B) :=
  eq x y := match x, y with
  | (la, ra), (lb, rb) => andb (eq la lb) (eq ra rb)
  end.
\end{coq_example*}
\begin{coq_eval}
Admitted.
\end{coq_eval}

These instances are used just as well as lemmas in the instances 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 [ eqa : Eq 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{Eq}. The parameters of the subclass contains
at least all the parameters of its superclasses in their order of
{'fraction_non_alphanumeric': 0.09891970332150919, 'fraction_numerical': 0.004272815220896485, 'mean_word_length': 4.1730608840700585, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 22, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7211086', 'n_tokens_mistral': 3972, 'n_tokens_neox': 3877, 'n_words': 1631}