@@ -530,9 +530,9 @@ a Coq proof script.
530530\newcommand{\iof}{\mathtt{of}}
531531\newcommand{\ilet}[2]{\mathtt{let}\;#1\;\mathtt{=}\;#2\;\mathtt{in}}
532532\newcommand{\ilam}[1]{\mathtt{\backslash}\;#1\;\mathtt{=>}}
533−\newcommand{\iarg}[2]{\mbox{\texttt{\{ $#1$ = $#2$ \}}}}
533+\newcommand{\iarg}[2]{\mbox{\texttt{\{$#1$ = $#2$\}}}}
534534\newcommand{\ihab}[2]{\mbox{\texttt{$#1$ : $#2$}}}
535−\newcommand{\carg}[1]{\mbox{\texttt{\{\{ $#1$ \}\}}}}
535+\newcommand{\carg}[1]{\mbox{\texttt{\{\{$#1$\}\}}}}
536536\newcommand{\fatarrow}{\mbox{\texttt{=>}}}
537537\newcommand{\ibar}{\mbox{\texttt{|}}}
538538\newcommand{\mvar}[1]{\mbox{\texttt{?}}#1}
@@ -600,7 +600,7 @@ a Coq proof script.
600600\medskip\\
601601\VV{cdecl} ::= & \iclass\;[\VV{constr}]\;\vx\;(\ihab{\tx}{\ttt})\;\iwhere\;\td
602602\\
603−\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\vt\;\iwhere\;\td
603+\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\ttt\;\iwhere\;\td
604604\end{array}
605605\end{array}
606606}
@@ -789,7 +789,8 @@ Elaborating a global function application makes a $\MO{Claim}$ for each argument
789789in turn. Then the function is elaborated, applied to each of the claimed arguments.
790790Finally, each argument which has been given explicitly is elaborated. If this fails,
791791elaboration tries again in the opposite order. Finally, we resolve any type
792−class instance arguments with the built-in $\MO{Instance}$ tactic.
792+class instance arguments with the built-in $\MO{Instance}$ tactic (see Section
793+\ref{sect:instance}).
793794
794795\DM{
795796\ttinterp{\vx\:\ta}\:\mq\:
@@ -1069,6 +1070,163 @@ as $\tp$, which is verified by $\MO{CheckComplete}$.
10691070
10701071\subsubsection{Elaborating Class and Instance Declarations}
10711072
1073+Type classes are implemented as dictionaries of functions for each instance. Therefore,
1074+a type class declaration elaborates to a record type containing all of the functions
1075+in the class, and an instance is simply an instance of the record. The methods
1076+are translated to top level functions which extract the relevant function from the
1077+dictionary.
1078+For example, for the \texttt{Show} type class, we translate the \texttt{class}
1079+declaration to:
1080+
1081+\begin{SaveVerbatim}{showdata}
1082+
1083+data Show : Set -> Set where
1084+ instanceShow : (show : a -> String) -> Show a
1085+
1086+show : Show a -> a -> String
1087+show (instanceShow show') = show'
1088+
1089+\end{SaveVerbatim}
1090+\useverb{showdata}
1091+
1092+\noindent
1093+An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for example for Nat:
1094+
1095+\begin{SaveVerbatim}{shownatf}
1096+
1097+showNat : Show Nat;
1098+showNat = instanceShow show' where
1099+ show' : Nat -> String
1100+ show' O = "O"
1101+ show' (S k) = "s" ++ show k
1102+
1103+\end{SaveVerbatim}
1104+\useverb{shownatf}
1105+
1106+The call to \tFN{show} in the body of the instance uses the top level \tFN{show}
1107+function, with the type class instance resolved by the elaborator.
1108+Where instances have constraints, we can simply pass these constraints on to
1109+the function declaration for the instance. For example, for \texttt{Show (List a)}:
1110+
1111+\begin{SaveVerbatim}{showlista}
1112+
1113+showList : Show a => Show (List a)
1114+showList = instanceShow show' where
1115+ show' : List a -> String
1116+ show' [] = "[]"
1117+ show' (x :: xs) = show x ++ " :: " ++ show xs
1118+
1119+\end{SaveVerbatim}
1120+\useverb{showlista}
1121+
1122+\noindent
1123+Where classes have constraints, we can again pass the
1124+constraints on to the data type declaration, and leave resolving the
1125+constraints to the elaborator. For example, for \texttt{Ord}:
1126+
1127+\begin{SaveVerbatim}{eqorda}
1128+
1129+class Eq a => Ord a where
1130+ compare : a -> a -> Ordering
1131+ max : a -> a -> a
1132+ -- remaining methods elided
1133+
1134+\end{SaveVerbatim}
1135+\useverb{eqorda}
1136+
1137+\noindent
1138+This translates to:
1139+
1140+\begin{SaveVerbatim}{orddata}
1141+
1142+data Ord : Set -> Set where
1143+ instanceOrd : Eq a => (compare : a -> a -> Ordering) ->
1144+ (max : a -> a -> a) -> Ord a
1145+
1146+compare : Ord a -> a -> a -> Ordering
1147+compare (instanceOrd compare' max') = compare'
1148+
1149+max : Ord a -> a -> a -> Ordering
1150+max (instanceOrd compare' max') = max'
1151+
1152+\end{SaveVerbatim}
1153+\useverb{orddata}
1154+
1155+We also add functions to retrieve parent classes from a dictionary, to assist
1156+with type class resolution. In this case, we add:
1157+
1158+\begin{SaveVerbatim}{ordparent}
1159+
1160+OrdEq : Ord a -> Eq a
1161+OrdEq (instanceOrd {{eq}} compare' max') = eq
1162+
1163+\end{SaveVerbatim}
1164+\useverb{ordparent}
1165+
1166+In general, we elaborate \texttt{class} declarations as follows:
1167+
1168+\DM{
1169+\AR{
1170+\MO{Elab}\:(\iclass\;\piconst{\tc}\TC{C}\:(\ta\Hab\ttt)\:\iwhere\:\td)
1171+\\
1172+\hg\hg
1173+\mq\:\RW{do}\:\AR{
1174+(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1175+\MO{Elab}\:
1176+\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Set\:\iwhere\\
1177+\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}
1178+\\
1179+\vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\
1180+\vec{\MO{ElabParent}}\:\tc
1181+}
1182+\medskip\\
1183+\MO{ElabMeth}\:(\vf\Hab\vt)\\
1184+\hg\hg\mq\:\RW{do}\:\AR{
1185+\MO{Elab}\:(\vf\Hab\TC{C}\:\ta\to\vt)\\
1186+\MO{Elab}\:(\vf\:(\DC{InstanceC}\:\vec{\VV{meth}})\:=\:\vec{\VV{meth}[\vf]})
1187+}
1188+\medskip\\
1189+\MO{ElabParent}\:\vc\\
1190+\hg\hg\mq\:\RW{do}\:\AR{
1191+\MO{Elab}\:(\VV{cC}\Hab\TC{C}\:\ta\to\vc)\\
1192+\MO{Elab}\:(\VV{cC}\:(\DC{InstanceC}\:\carg{\vc'}\:\vec{\VV{meth}})\:=\:\vc')
1193+}
1194+}
1195+}
1196+
1197+Then we elaborate \texttt{instance} declarations as follows:
1198+
1199+\DM{
1200+\AR{
1201+\MO{Elab}\:(\iinstance\;\piconst{\tc}\TC{C}\:\ttt\:\iwhere\:\td)\\
1202+\hg\hg\mq\:\RW{do}\:\AR{
1203+(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\td\\
1204+\vec{\VV{ty'}}\:=\:\vec{\VV{ty}}[\ttt/\ta]\\
1205+\MO{Elab}\:(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\:\ttt)\\
1206+\MO{Elab}\:\AR{
1207+(\FN{instanceC}\:=\:\DC{InstanceC}\;\vec{\VV{meth'}}\;\iwhere
1208+\\
1209+\hg\vec{\VV{meth'}}\Hab\vec{\VV{ty'}}\\
1210+\hg\td
1211+)}
1212+}
1213+}
1214+}
1215+
1216+Adding default definitions is straightforward: simply insert the default definition where
1217+there is a method missing in an \texttt{instance} declaration.
1218+
1219+Key point: we've added a higher level language construct simply by elaborating in terms of
1220+a lower level language construct. In particular, we don't need to worry about type
1221+class \remph{resolution}, because we have a tactic to do that.
1222+We can build a lot of extensions this way because we
1223+have effectively built, bottom up, an Embedded Domain Specific Language for constructing
1224+programs in \TT{}.
1225+
1226+\subsubsection{The $\MO{Instance}$ tactic}
1227+
1228+\label{sect:instance}
1229+
10721230\subsection{Syntax Extensions}
10731231
10741232\subsubsection{Metavariables}