diff options
Diffstat (limited to 'doc/refman/Classes.tex')
-rw-r--r-- | doc/refman/Classes.tex | 423 |
1 files changed, 0 insertions, 423 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex deleted file mode 100644 index f427609f..00000000 --- a/doc/refman/Classes.tex +++ /dev/null @@ -1,423 +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}} -\aauthor{Matthieu Sozeau} -\label{typeclasses} - -\begin{flushleft} - \em The status of Type Classes is 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. -\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. - -The parsing of generalized type-class binders is different from regular -binders: -\begin{itemize} -\item Implicit arguments of the class type are ignored. -\item Superclasses arguments are automatically generalized. -\item Any remaining arguments not given as part of a type class binder - will be automatically generalized. In other words, the rightmost - parameters are automatically generalized if not mentionned. -\end{itemize} - -One can switch off this special treatment using the $!$ mark in front of -the class name (see example below). - -\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 possible to do it directly in regular -generalized 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: |