6c08816 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More paper changes

6c08816Edwin Brady15 years ago

impl-paper/elaboration.tex+162−4

compare with master

unifiedsplit

@@ -530,9 +530,9 @@ a Coq proof script.

530\newcommand{\iof}{\mathtt{of}}

531\newcommand{\ilet}[2]{\mathtt{let}\;#1\;\mathtt{=}\;#2\;\mathtt{in}}

532\newcommand{\ilam}[1]{\mathtt{\backslash}\;#1\;\mathtt{=>}}

533−\newcommand{\iarg}[2]{\mbox{\texttt{\{ $#1$ = $#2$ \}}}}

533+\newcommand{\iarg}[2]{\mbox{\texttt{\{$#1$ = $#2$\}}}}

534\newcommand{\ihab}[2]{\mbox{\texttt{$#1$ : $#2$}}}

535−\newcommand{\carg}[1]{\mbox{\texttt{\{\{ $#1$ \}\}}}}

535+\newcommand{\carg}[1]{\mbox{\texttt{\{\{$#1$\}\}}}}

536\newcommand{\fatarrow}{\mbox{\texttt{=>}}}

537\newcommand{\ibar}{\mbox{\texttt{|}}}

538\newcommand{\mvar}[1]{\mbox{\texttt{?}}#1}

@@ -600,7 +600,7 @@ a Coq proof script.

600\medskip\\

601\VV{cdecl} ::= & \iclass\;[\VV{constr}]\;\vx\;(\ihab{\tx}{\ttt})\;\iwhere\;\td

602\\

603−\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\vt\;\iwhere\;\td

603+\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\ttt\;\iwhere\;\td

604\end{array}

605\end{array}

606}

@@ -789,7 +789,8 @@ Elaborating a global function application makes a $\MO{Claim}$ for each argument

789in turn. Then the function is elaborated, applied to each of the claimed arguments.

790Finally, each argument which has been given explicitly is elaborated. If this fails,

791elaboration 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}).

793

794

794\DM{

795\DM{

795\ttinterp{\vx\:\ta}\:\mq\:

796\ttinterp{\vx\:\ta}\:\mq\:

@@ -1069,6 +1070,163 @@ as $\tp$, which is verified by $\MO{CheckComplete}$.

1069

1070

1070\subsubsection{Elaborating Class and Instance Declarations}

1071\subsubsection{Elaborating Class and Instance Declarations}

1071

1072

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+

1072\subsection{Syntax Extensions}

1230\subsection{Syntax Extensions}

1073

1231

1074\subsubsection{Metavariables}

1232\subsubsection{Metavariables}

src/Idris/Parser.hs+1

@@ -658,6 +658,7 @@ pSimpleExpr syn =

658 <|> try (do c <- pConstant; fc <- pfc

659 return (modifyConst syn fc (PConstant c)))

660 <|> do reserved "Set"; return PSet

661+-- <|> do symbol "*"; return PSet

661 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))

662 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))

662 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))

663 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))

663 <|> do lchar '_'; return Placeholder

664 <|> do lchar '_'; return Placeholder

tutorial/interp.tex+3

@@ -303,6 +303,9 @@ app = \f, a => App f a

303\useverb{lazyapp}

304

305\noindent

306+The vertical bar annotation before the \texttt{f} argument indicates that this

307+argument should be evaluated lazily when \texttt{app} is applied --- that is, the

308+argument will be evaluated only when needed.

306Then \texttt{fact}

309Then \texttt{fact}

307(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})

310(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})

308is written as follows:

311is written as follows: