a706b8e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Proof read for voice/consistency

a706b8eEdwin Brady15 years ago

impl-paper/conclusions.tex+5−4

compare with master

unifiedsplit

@@ -87,7 +87,8 @@ these are implemented by lifting the branches out to a top level function.

87We do not need to make any changes to the core language type system in order to

88implement these high level features.

89Other high level features such as dependent records, tuples and monad comprehensions

90+can be added equally easily --- and indeed have been added in the full implementation.

90−can be added equally easily. Furthermore,

91+Furthermore,

91since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it is

92since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it is

92possible to expose the tactic language to the programmer. This opens up the

93possible to expose the tactic language to the programmer. This opens up the

93possibility of implementing domain specific decision procedures, or implementing

94possibility of implementing domain specific decision procedures, or implementing

@@ -116,12 +117,12 @@ by building on top of a small, well-understood, easy to reason about type

116theory.

117theory.

117However, a programming language implementation is not an end in itself.

118However, a programming language implementation is not an end in itself.

118Programming languages exist to support research and practice in many different

119Programming languages exist to support research and practice in many different

119−domains. In future work, therefore, we plan to apply domain specific

120+domains. In future work, therefore, I plan to apply domain specific

120language based techniques to realistic problems

121language based techniques to realistic problems

121in important safety critical domains such as security and network protocol

122in important safety critical domains such as security and network protocol

122−design and implementation. In order to be successful, we need a language which

123+design and implementation. In order to be successful, this will require a language which

123is expressive enough to describe protocol specifications at a high level, and robust

124is expressive enough to describe protocol specifications at a high level, and robust

124−enough to guarantee correct implementation of those protocols. \Idris{}, we believe,

125+enough to guarantee correct implementation of those protocols. \Idris{}, I believe,

125is the right tool for this work.

126is the right tool for this work.

126

127

128

impl-paper/delab.tex+2−2

@@ -90,7 +90,7 @@ which arguments are implicit or constraint arguments:

91\noindent

92Using this, we define $\MO{Unelab}$ for top level declarations. For pattern

93−matching clauses, we reverse elaborate as follows, discarding the explicit

93+matching clauses reversing elaboration proceeds as follows, discarding the explicit

94pattern variable bindings and applying $\MO{UnelabType}$ to reconstruct

95the type declaration:

@@ -103,7 +103,7 @@ the type declaration:

103}

104

105\noindent

106−For data type declarations, we unelaborate as follows, applying $\MO{UnelabType}$

106+For data type declarations, reverse elaboration proceeds as follows, applying $\MO{UnelabType}$

107for each of the top level type declarations:

108

109\DM{

impl-paper/elaboration.tex+76−66

@@ -22,7 +22,7 @@ one or more \TT{} declarations.

23\subsection{The Development Calculus \TTdev}

25−We build \TT{} expressions by using high level \Idris{} expressions to

25+\TT{} expressions are built by using high level \Idris{} expressions to

26direct a tactic based theorem prover, which builds the \TT{} expressions

27step by step, by refinement. In order to build expressions in this way,

28the type theory needs to support

@@ -129,7 +129,7 @@ the final proof term, which must be a \TT{} program (i.e. does not contain any o

129\demph{pure}. Although a pure term does not contain hole or guess bindings, it may

130nevertheless \remph{refer} to hole- or guess-bound variables.

131

132−We initialise a proof state with the $\MO{NewProof}$ operation. Given a global

132+The proof state is initialised with the $\MO{NewProof}$ operation. Given a global

133context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:

134

135\DM{

@@ -137,7 +137,7 @@ context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:

137}

138

139The local context is initially empty, and the initial hole queue is the $\vx$ standing for

140−the entire expression. We can reset the proof term with the $\MO{NewTerm}$ operation.

140+the entire expression. The proof term is reset with the $\MO{NewTerm}$ operation.

141In an existing proof state $(\vC, \Delta, \ve, \vQ)$,

142$\MO{NewTerm}\:\vt$ discards the proof term and hole queue, and

143updates the proof state to:

@@ -147,8 +147,8 @@ updates the proof state to:

147}

148

149

150−This allows us in particular to use pattern bindings from the left hand side of a pattern

150+This allows the elaborator to use pattern bindings from the left

151−matching definition in the term on the right hand side.

151+hand side of a pattern matching definition in the term on the right hand side.

152

153\subsection{System State}

154

@@ -193,7 +193,7 @@ vAdd : (a : _) -> (n : _) -> (c : Num a) ->

193\useverb{vAddImpT}

194

195\noindent

196−For \tFN{vAdd}, we record that \texttt{a} and \texttt{n} are implicit,

196+For \tFN{vAdd}, the state records that \texttt{a} and \texttt{n} are implicit,

197\texttt{c} is a constraint, and \texttt{xs} and \texttt{ys} are explicit. When

198the elaborator encounters an application of \tFN{vAdd}, it knows that unless these arguments

199are given explicitly, the application must be expanded.

@@ -264,7 +264,7 @@ keeping $\vx$ at the head:

264}

265

266An obvious difficulty is in ensuring that names are unique throughout a proof term.

267−In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic

267+The implementation ensures that any hole created by the $\MO{Claim}$ tactic

268has a unique name by checking against existing names in scope and modifying

269the name if necessary. In this paper, we will assume that all created names are fresh.

270

@@ -296,13 +296,14 @@ For example, consider the following proof term:

296}

297

298\noindent

299−If $\vx$ is in focus (i.e., at the head of the hole queue) and we attempt to

299+If $\vx$ is in focus (i.e., at the head of the hole queue) and the elaborator

300+attempts to

300$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:

301$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:

301

302

302\begin{itemize}

303\begin{itemize}

303\item $\Check\:42\:\mq\:\TC{Int}$

304\item $\Check\:42\:\mq\:\TC{Int}$

304\item Unifying $\TC{Int}$ with $\vA$ (the type of $\vx$) is only possible if

305\item Unifying $\TC{Int}$ with $\vA$ (the type of $\vx$) is only possible if

305−$\vA\:=\:\TC{Int}$, so we solve $\vA$.

306+$\vA\:=\:\TC{Int}$, so solve $\vA$.

306\end{itemize}

307\end{itemize}

307

308

308\noindent

309\noindent

@@ -328,6 +329,10 @@ the guess is substituted into its scope:

328}

329}

330}

330

331

332+The two step process, with $\MO{Fill}$ followed by $\MO{Solve}$, allows the elaborator

333+to work safely with incomplete terms, since an incomplete guess binding has no

334+computational force. Once a term is complete in a guess binding, it may be substituted into the

335+scope of the binding safely.

331In each of these tactics, if any step fails, or the term in focus does not take

336In each of these tactics, if any step fails, or the term in focus does not take

332the correct form (e.g. is not a guess in the case of $\MO{Solve}$ or not a hole

337the correct form (e.g. is not a guess in the case of $\MO{Solve}$ or not a hole

333in the case of $\MO{Claim}$ and $\MO{Fill}$, the entire tactic fails. We can

338in the case of $\MO{Claim}$ and $\MO{Fill}$, the entire tactic fails. We can

@@ -347,8 +352,8 @@ problem) and is handled by $\MO{Try}$.

347

352

348\subsubsection{Creating binders}

353\subsubsection{Creating binders}

349

354

350−We also define primitive tactics for constructing binders. We can create a $\lambda$

355+We also define primitive tactics for constructing binders. Creating a $\lambda$

351−binding if the goal normalises to a function type:

356+binding requires that the goal normalises to a function type:

352

357

353\DM{

358\DM{

354\PA{\A\A}{

359\PA{\A\A}{

@@ -362,7 +367,7 @@ binding if the goal normalises to a function type:

362}

367}

363

368

364\noindent

369\noindent

365−We can create a $\forall$ binding if the goal is a $\TC{Set}$:

370+Creating a $\forall$ binding requires that the goal is a $\TC{Set}$:

366

371

367\DM{

372\DM{

368\PA{\A\A}{

373\PA{\A\A}{

@@ -376,7 +381,7 @@ We can create a $\forall$ binding if the goal is a $\TC{Set}$:

376}

381}

377

382

378\noindent

383\noindent

379−To create a $\LET$ binding, we give a type and a value.

384+Creating a $\LET$ binding requires a type and a value.

380

385

381\DM{

386\DM{

382\PA{\A\A}{

387\PA{\A\A}{

@@ -392,8 +397,8 @@ To create a $\LET$ binding, we give a type and a value.

392}

397}

393

398

394Each of these tactics require the term in focus to be of the form $\hole{\vx}{\vT}\SC\vx$.

399Each of these tactics require the term in focus to be of the form $\hole{\vx}{\vT}\SC\vx$.

395−This is important, because if the scope of the binding was an arbitrary expression $\ve$,

400+This is important, because if the scope of the binding were an arbitrary expression $\ve$,

396−the binder would be scoped across this whole expression rather than the subexpression

401+the binder would be scoped across this \emph{whole} expression rather than the subexpression

397$\vx$ as intended.

402$\vx$ as intended.

398The $\MO{attack}$ tactic ensures that a hole

403The $\MO{attack}$ tactic ensures that a hole

399is in the appropriate form, creating a new hole $\vh$ which is placed at the head

404is in the appropriate form, creating a new hole $\vh$ which is placed at the head

@@ -779,7 +784,7 @@ There are two cases to consider when elaborating applications:

779\item Applying an expression, which does not have implicit arguments, to an argument.

784\item Applying an expression, which does not have implicit arguments, to an argument.

780\end{itemize}

785\end{itemize}

781

786

782−In the first case, we must expand the application to include implicit arguments.

787+In the first case, the elaborator must expand the application to include implicit arguments.

783For example \texttt{vAdd xs ys} is expanded to

788For example \texttt{vAdd xs ys} is expanded to

784\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments

789\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments

785\texttt{a} and \texttt{n} and a type class instance argument. The meta-operation

790\texttt{a} and \texttt{n} and a type class instance argument. The meta-operation

@@ -825,9 +830,8 @@ arguments first.

825Elaborating a global function application makes a $\MO{Claim}$ for each argument

830Elaborating a global function application makes a $\MO{Claim}$ for each argument

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

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

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

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

828−elaboration tries again in the opposite order. Finally, we resolve any type

833+elaboration tries again in the opposite order. Finally, any type

829−class instance arguments with the built-in $\MO{Instance}$ tactic (see Section

834+class instance arguments are resolved with the built-in $\MO{Instance}$ tactic.

830−\ref{sect:instance}).

831

835

832\DM{

836\DM{

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

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

@@ -860,9 +864,9 @@ in detail in Section \ref{sect:instance}.

860

864

861To elaborate a simple function application, of an arbitrary expression to an arbitrary

865To elaborate a simple function application, of an arbitrary expression to an arbitrary

862argument, we need not worry about implicit arguments or class constraints. Instead,

866argument, we need not worry about implicit arguments or class constraints. Instead,

863−we simply elaborate the function and argument, and apply the results. Since elaboration

867+the function and argument are elaborated, and the results applied. Since elaboration

864−is type directed, however, we do need to construct an appropriate type for the function.

868+is type directed, however, there must be an appropriate type for the function.

865−As before, we try elaboration in two orders, as we may learn something from elaborating

869+As before, elaboration tries two orders, as it may learn something from elaborating

866the function or argument which helps with unification:

870the function or argument which helps with unification:

867

871

868\DM{

872\DM{

@@ -897,8 +901,8 @@ current proof state. $\MO{Elab}$ uses $\ttinterp{\cdot}$ to help translate

897

901

898\subsubsection{Elaborating Type Declarations}

902\subsubsection{Elaborating Type Declarations}

899

903

900−To elaborate a type declaration, we simply create a new proof state,

904+Elaborating a type declaration involves creating a new proof state,

901−translate the \IdrisM{} type to a \TT{} type, then add the resulting type

905+translating the \IdrisM{} type to a \TT{} type, then adding the resulting type

902as a \TT{} declaration:

906as a \TT{} declaration:

903

907

904\DM{

908\DM{

@@ -916,10 +920,10 @@ into the context.

916

920

917\subsubsection{Elaborating Data Types}

921\subsubsection{Elaborating Data Types}

918

922

919−To elaborate a data declaration, we need to elaborate the type declaration itself,

923+Elaborating a data declaration involves elaborating the type declaration itself,

920as a normal type declaration. This ensures that the type is in scope when

924as a normal type declaration. This ensures that the type is in scope when

921−elaborating the constructor types. We then use the results to build a \TT{} data

925+elaborating the constructor types. Then using the results, the elaborator

922−declaration.

926+adds a \TT{} data declaration.

923

927

924\DM{

928\DM{

925\AR{

929\AR{

@@ -942,7 +946,7 @@ declaration.

942

946

943\subsubsection{Elaborating Pattern Matching}

947\subsubsection{Elaborating Pattern Matching}

944

948

945−To elaborate a pattern matching definition, we work clause by clause, elaborating

949+Elaborating a pattern matching definition works clause by clause, elaborating

946the left and right hand sides in turn. $\MO{ElabClause}$ returns the elaborated

950the left and right hand sides in turn. $\MO{ElabClause}$ returns the elaborated

947left and right hand sides, and may have the side effect of adding entries

951left and right hand sides, and may have the side effect of adding entries

948to the global context, such as definitions in $\iwhere$ clauses.

952to the global context, such as definitions in $\iwhere$ clauses.

@@ -952,17 +956,17 @@ First, let us consider the simplest case, with no $\iwhere$ clause:

952\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?

956\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?

953}

957}

954

958

955−How do we elaborate the left hand side, given that elaboration is type directed, and

959+How does the left hand side get elaborated, given that elaboration is type directed, and

956−we do not know its type until after we have elaborated it?

960+its type is not known until after elaboration?

957−We can achieve this without any change to the elaborator by defining

961+This can be achieved without any change to the elaborator by defining

958a type $\TC{Infer}$:

962a type $\TC{Infer}$:

959

963

960\DM{

964\DM{

961\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}

965\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}

962}

966}

963

967

964−Now to elaborate the left hand side, we elaborate $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and

968+Now elaboration of the left hand side proceeds by elaborating $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and

965−extract the value and unified type when complete.

969+extracting the value and unified type when complete.

966

970

967\DM{

971\DM{

968\AR{

972\AR{

@@ -984,8 +988,8 @@ This infers a type for the left hand side, creating pattern variable bindings. T

984it elaborates the right hand side using the inferred type of the left hand side

988it elaborates the right hand side using the inferred type of the left hand side

985and the inferred pattern bindings, which are retrieved from the state with the

989and the inferred pattern bindings, which are retrieved from the state with the

986$\MO{Patterns}$ operation. Finally, it returns a pattern clause in \TT{} form.

990$\MO{Patterns}$ operation. Finally, it returns a pattern clause in \TT{} form.

987−To elaborate a collection of pattern clauses, we simply map $\MO{ElabClause}$ over

991+Elaborating a collection of pattern clauses then proceeds by mapping $\MO{ElabClause}$ over

988−the clauses and add the resulting collection to \TT{}.

992+the clauses and adding the resulting collection to \TT{}.

989

993

990\DM{

994\DM{

991\AR{

995\AR{

@@ -998,9 +1002,9 @@ the clauses and add the resulting collection to \TT{}.

998}

1002}

999

1003

1000Elaborating a clause is made only slightly more complex by the presence of

1004Elaborating a clause is made only slightly more complex by the presence of

1001−$\iwhere$ clauses. In this case, we elaborate the left hand side, add the pattern

1005+$\iwhere$ clauses. In this case, after elaborating the left hand side, the pattern

1002−bound variables as extra arguments to the declarations in the $\iwhere$ block,

1006+bound variables are added as extra arguments to the declarations in the $\iwhere$ block,

1003−and recursively elaborate before elaborating the right hand side.

1007+which are then recursively elaborated before the right hand side.

1004

1008

1005\DM{

1009\DM{

1006\AR{

1010\AR{

@@ -1028,7 +1032,7 @@ the right hand side $\ve$ to use the lifted definitions, rather than the origina

1028\subsubsection{Elaborating the \texttt{with} rule}

1032\subsubsection{Elaborating the \texttt{with} rule}

1029

1033

1030The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.

1034The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.

1031−To translate this into \TT{}, we need to construct an auxiliary top level

1035+Translating this into \TT{} involves constructing an auxiliary top level

1032definition for

1036definition for

1033the intermediate pattern match. For example, recall \tFN{natToBin}:

1037the intermediate pattern match. For example, recall \tFN{natToBin}:

1034

1038

@@ -1055,8 +1059,7 @@ natToBin' (S (j + j)) odd = True :: natToBin j

1055

1059

1056\useverb{natToBinwp}

1060\useverb{natToBinwp}

1057

1061

1058−The difference when using the \texttt{with} rule is that there is no need for

1062+\noindent

1059−the explicit type declaration for the auxiliary function \texttt{natToBin}.

1060Elaboration of \texttt{with} builds the type declaration and auxiliary function

1063Elaboration of \texttt{with} builds the type declaration and auxiliary function

1061automatically:

1064automatically:

1062

1065

@@ -1115,8 +1118,8 @@ a type class declaration elaborates to a record type containing all of the funct

1115in the class, and an instance is simply an instance of the record. The methods

1118in the class, and an instance is simply an instance of the record. The methods

1116are translated to top level functions which extract the relevant function from the

1119are translated to top level functions which extract the relevant function from the

1117dictionary.

1120dictionary.

1118−For example, for the \texttt{Show} type class, we translate the \texttt{class}

1121+For example, for the \texttt{Show} type class, the \texttt{class}

1119−declaration to:

1122+declaration is translated to:

1120

1123

1121\begin{SaveVerbatim}{showdata}

1124\begin{SaveVerbatim}{showdata}

1122

1125

@@ -1145,7 +1148,7 @@ showNat = instanceShow show' where

1145

1148

1146The call to \tFN{show} in the body of the instance uses the top level \tFN{show}

1149The call to \tFN{show} in the body of the instance uses the top level \tFN{show}

1147function, with the type class instance resolved by the elaborator.

1150function, with the type class instance resolved by the elaborator.

1148−Where instances have constraints, we can simply pass these constraints on to

1151+Where instances have constraints, these constraints are passed on to

1149the function declaration for the instance. For example, for \texttt{Show (List a)}:

1152the function declaration for the instance. For example, for \texttt{Show (List a)}:

1150

1153

1151\begin{SaveVerbatim}{showlista}

1154\begin{SaveVerbatim}{showlista}

@@ -1160,9 +1163,9 @@ showList = instanceShow show' where

1160\useverb{showlista}

1163\useverb{showlista}

1161

1164

1162\noindent

1165\noindent

1163−Where classes have constraints, we can again pass the

1166+Where classes have constraints, the

1164−constraints on to the data type declaration, and leave resolving the

1167+constraints are again passed on to the data type declaration, and resolved by the

1165−constraints to the elaborator. For example, for \texttt{Ord}:

1168+elaborator. For example, for \texttt{Ord}:

1166

1169

1167\begin{SaveVerbatim}{eqorda}

1170\begin{SaveVerbatim}{eqorda}

1168

1171

@@ -1183,6 +1186,9 @@ data Ord : Set -> Set where

1183 instanceOrd : Eq a => (compare : a -> a -> Ordering) ->

1186 instanceOrd : Eq a => (compare : a -> a -> Ordering) ->

1184 (max : a -> a -> a) -> Ord a

1187 (max : a -> a -> a) -> Ord a

1185

1188

1189+\end{SaveVerbatim}

1190+

1191+\begin{SaveVerbatim}{orddatab}

1186compare : Ord a -> a -> a -> Ordering

1192compare : Ord a -> a -> a -> Ordering

1187compare (instanceOrd compare' max') = compare'

1193compare (instanceOrd compare' max') = compare'

1188

1194

@@ -1192,8 +1198,11 @@ max (instanceOrd compare' max') = max'

1192\end{SaveVerbatim}

1198\end{SaveVerbatim}

1193\useverb{orddata}

1199\useverb{orddata}

1194

1200

1201+\useverb{orddatab}

1202+

1203+\noindent

1195−We also add functions to retrieve parent classes from a dictionary, to assist

1204+The elaborator also adds functions to retrieve parent classes from a dictionary, to assist

1196−with type class resolution. In this case, we add:

1205+with type class resolution. In this case:

1197

1206

1198\begin{SaveVerbatim}{ordparent}

1207\begin{SaveVerbatim}{ordparent}

1199

1208

@@ -1204,7 +1213,7 @@ OrdEq (instanceOrd {{eq}} compare' max') = eq

1204\useverb{ordparent}

1213\useverb{ordparent}

1205

1214

1206\noindent

1215\noindent

1207−In general, we elaborate \texttt{class} declarations as follows:

1216+In general, \texttt{class} declarations are elaborated as follows:

1208

1217

1209\DM{

1218\DM{

1210\AR{

1219\AR{

@@ -1242,7 +1251,7 @@ In general, we elaborate \texttt{class} declarations as follows:

1242}

1251}

1243

1252

1244\noindent

1253\noindent

1245−Then we elaborate \texttt{instance} declarations as follows:

1254+Then \texttt{instance} declarations are elaborated as follows:

1246

1255

1247\DM{

1256\DM{

1248\AR{

1257\AR{

@@ -1275,7 +1284,7 @@ constructing programs in \TT{}.

1275

1284

1276\label{sect:instance}

1285\label{sect:instance}

1277

1286

1278−When elaborating applications, recall that we fill in implicit arguments by

1287+When elaborating applications, recall that implicit arguments are filled in by

1279unification, and type class constraints by an $\MO{Instance}$ tactic which searches

1288unification, and type class constraints by an $\MO{Instance}$ tactic which searches

1280the context for an instance of the required type class.

1289the context for an instance of the required type class.

1281

1290

@@ -1298,9 +1307,9 @@ basic primitive for proof search, and is defined as follows:

1298}

1307}

1299}

1308}

1300

1309

1301−For example, in the following function, we resolve the type class constraint required

1310+For example, in the following function, the type class constraint required for

1302−for the $\texttt{>}$ operator by finding an instance for \texttt{Ord a} in the local

1311+the $\texttt{>}$ operator is resolved by finding an instance for \texttt{Ord a}

1303−context:

1312+in the local context:

1304

1313

1305\begin{SaveVerbatim}{ordlocal}

1314\begin{SaveVerbatim}{ordlocal}

1306

1315

@@ -1344,11 +1353,11 @@ we constrain the search by recording which instances are defined for each type c

1344and by ensuring that a recursive call of $\MO{Instance}$ is either searching for

1353and by ensuring that a recursive call of $\MO{Instance}$ is either searching for

1345a different class, or a structurally smaller instance of the current class.

1354a different class, or a structurally smaller instance of the current class.

1346

1355

1347−For example, in the following function, we resolve the constraints required by the

1356+For example, in the following function, the constraints required by the

1348−\tFN{show} function by a global search which locates a \tTC{Show} instance for

1357+\tFN{show} function are resolved by a global search which locates a \tTC{Show}

1349−\tTC{List a}, which in turn requires a \tTC{Show} instance for \texttt{a}.

1358+instance for \tTC{List a}, which in turn requires a \tTC{Show} instance for

1350−In this case \texttt{a} is instantiated by \tTC{Int}, so we finish by locating

1359+\texttt{a}. In this case \texttt{a} is instantiated by \tTC{Int}, so resolution finishes

1351−a \tTC{Show} instance for \tTC{Int}:

1360+by locating a \tTC{Show} instance for \tTC{Int}:

1352

1361

1353\begin{SaveVerbatim}{showinst}

1362\begin{SaveVerbatim}{showinst}

1354

1363

@@ -1428,8 +1437,8 @@ append_rec a m n x xs ys = app xs ys

1428\end{SaveVerbatim}

1437\end{SaveVerbatim}

1429\useverb{appendrec_def}

1438\useverb{appendrec_def}

1430

1439

1431−To elaborate a metavariable, we simply add a new top level definition, and apply

1440+Elaborating a metavariable involves adding a new top level definition which is applied

1432−it to the current context:

1441+to all of the variables in local scope.

1433

1442

1434\DM{

1443\DM{

1435\ttinterp{\mvar{\vx}}\:\mq\:

1444\ttinterp{\mvar{\vx}}\:\mq\:

@@ -1445,8 +1454,9 @@ it to the current context:

1445

1454

1446A \texttt{case} expression allows pattern matching on intermediate values. The difficulty

1455A \texttt{case} expression allows pattern matching on intermediate values. The difficulty

1447in elaborating \texttt{case} expressions is that \TT{} allows matching only on

1456in elaborating \texttt{case} expressions is that \TT{} allows matching only on

1448−\emph{top level} values. To elaborate a \texttt{case} expression, therefore,

1457+\emph{top level} values. Elaborating a \texttt{case} expression, therefore,

1449−we create a new top level function standing for the expression, and apply it. The natural

1458+involves creating a new top level function standing for the expression, and applying it.

1459+The natural

1450way to implement this is to use a metavariable. For example, we have already seen

1460way to implement this is to use a metavariable. For example, we have already seen

1451\texttt{lookup\_default}:

1461\texttt{lookup\_default}:

1452

1462

@@ -1467,9 +1477,9 @@ lookup_default_case i xs def (Just x) = x

1467\end{SaveVerbatim}

1477\end{SaveVerbatim}

1468\useverb{listlookupmv}

1478\useverb{listlookupmv}

1469

1479

1470−To elaborate a $\icase$ expression, we begin by \texttt{let} binding the scrutinee of

1480+To elaborate a $\icase$ expression involves \texttt{let} binding the scrutinee of

1471the $\icase$ expression and creating a metavariable $\VV{xcase}$ to implement the

1481the $\icase$ expression and creating a metavariable $\VV{xcase}$ to implement the

1472−pattern matching. We then build a new pattern matching definition for $\VV{xcase}$

1482+pattern matching. Then the elaborator builds a new pattern matching definition for $\VV{xcase}$

1473and elaborate it:

1483and elaborate it:

1474

1484

1475\DM{

1485\DM{

impl-paper/hll.tex+23−23

@@ -39,8 +39,8 @@ main = putStrLn ("The answer is " ++ show x)

39\noindent

40Like Haskell, the main function

41is called \texttt{main}, and input and output is managed with an \texttt{IO}

42−monad. Unlike Haskell, however, we use a single colon \texttt{:} for type

42+monad. Unlike Haskell, however, a single colon indicates \texttt{:} a type

43−declarations, emphasising the importance of types,

43+declaration, emphasising the importance of types,

44and \remph{all} functions must have a top level type

45declaration. This is due to type inference being, in general,

46undecidable for languages with

@@ -189,7 +189,7 @@ reverse {a} xs = revAcc [] xs where

189

190A standard example of a dependent type is the type of ``lists with length'',

191conventionally called ``vectors'' in the dependently typed programming

192−literature. In \Idris{}, we declare vectors as follows:

192+literature. In \Idris{}, vectors are declared as follows:

193

194\begin{SaveVerbatim}{vect}

195

@@ -201,24 +201,24 @@ data Vect : Set -> Nat -> Set where

201\useverb{vect}

202

203\noindent

204−Note that we have used the same constructor names as for \tTC{List}. Ad-hoc

204+Note that this uses the same constructor names as for \tTC{List}. Ad-hoc

205name overloading such as this is accepted by \Idris{}, provided that the names

206are declared in different namespaces (in practice, normally in different modules).

207Ambiguous constructor names are resolved by type.

208

209This declares a family of types, which requires a different form of declaration

210from the simple type declarations above. It resembles a Haskell GADT

211−declaration: we explicitly state the type

211+declaration: it explicitly states the type

212of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

213argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}

214is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

215constructor targets a different part of the family of types. \tDC{Nil} can only

216be used to construct vectors with zero length, and \tDC{::} to construct

217−vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element

217+vectors with non-zero length. The type of \tDC{::} states explicitly that an element

218of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})

219combine to make a vector of length \texttt{S k}.

220

221−We can define functions on dependent types such as \tTC{Vect} in the same way

221+Functions on dependent types such as \tTC{Vect} are declared in the same way

222as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.

223The type of a function over \tTC{Vect} will describe what happens to the

224lengths of the vectors involved. For example, \tFN{++}, defined in the

@@ -302,7 +302,7 @@ index : Fin n -> Vect a n -> a

302It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector

303with \texttt{n} elements of type \texttt{a}. But there are also two names,

304\texttt{n} and \texttt{a}, which are not declared explicitly. These are \emph{implicit}

305−arguments to \texttt{index}. We could also write the type of \texttt{index} as:

305+arguments to \texttt{index}. The type of \texttt{index} could also be written as:

306

307\begin{SaveVerbatim}{vindeximppl}

308

@@ -312,8 +312,8 @@ index : {a:_} -> {n:_} -> Fin n -> Vect a n -> a

312\useverb{vindeximppl}

313

314\noindent

315−Here we have given bindings for \texttt{a} and \texttt{n} with placeholders for

315+This gives bindings for \texttt{a} and \texttt{n} with placeholders for

316−their types, to be inferred by the machine. We could also give the types explicitly:

316+their types, to be inferred by the machine. These types could also be given explicitly:

317

318\begin{SaveVerbatim}{vindeximpty}

319

@@ -341,7 +341,7 @@ index {a=Int} {n=2} fO (2 :: 3 :: Nil)

341

342\noindent

343In fact, any argument, implicit or explicit, may be given a name. For example,

344−we could have declared the type of \texttt{index} as:

344+the type of \texttt{index} could be declared as:

345

346\begin{SaveVerbatim}{vindexn}

347

@@ -439,10 +439,10 @@ instance Show a => Show (Vect a n) where

439\textbf{Remark: } The type of the auxiliary function \texttt{show'} is

440important. The type variables \texttt{a} and \texttt{n} which are part of the

441instance declaration for \texttt{Show (Vect a n)} are fixed across the entire

442−instance declaration. As a result, we do not have to constrain \texttt{a}

442+instance declaration. As a result, \texttt{a} need not be constrained

443−again. Furthermore, it means that if we use \texttt{n} in the type, it refers

443+again. Furthermore, it means that if \texttt{n} is used again in the type, it refers

444to the (fixed) length of the outermost list \texttt{xs}. Therefore,

445−we use a different name for the length \texttt{n'} in \texttt{show'}.

445+there is a different name for the length \texttt{n'} in \texttt{show'}.

446

447Like Haskell type classes, default definitions can be given in the class declaration.

448Otherwise, all methods must be given in an instance. For example, there is an

@@ -498,8 +498,8 @@ mirror xs = let xs' = rev xs in

498\useverb{letb}

499

500\noindent

501−We can also pattern match in \texttt{let} bindings. For example, we can extract

501+Pattern matching is also supported in \texttt{let} bindings. For example, extracting

502−fields from a record as follows, as well as by pattern matching at the top level:

502+fields from a record can be achieved as follows, as well as by pattern matching at the top level:

503

504\begin{SaveVerbatim}{letp}

505

@@ -517,7 +517,7 @@ Another way of inspecting intermediate values of \emph{simple} types

517is to use a \texttt{case} expression.

518For example, \texttt{list\_lookup}

519looks up an index in a list, returning \texttt{Nothing} if the index is out

520−of bounds. We can use this to write \texttt{lookup\_default}, which

520+of bounds. This can be used this to write \texttt{lookup\_default}, which

521looks up an index and returns a default value if the index is out of bounds:

522

523\begin{SaveVerbatim}{listlookup}

@@ -546,7 +546,7 @@ determined \emph{without} type checking the \texttt{case}-expression itself.

546

547Since types can depend on values, the form of some arguments can be determined

548by the value of others. For example, if we were to write down the implicit

549−length arguments to \texttt{(++)}, we'd see that the form of the length argument was

549+length arguments to \texttt{(++)}, we would see that the form of the length argument was

550determined by whether the vector was empty or not:

551

552\begin{SaveVerbatim}{appdep}

@@ -563,13 +563,13 @@ If \texttt{n} was a successor in the \texttt{[]} case, or zero in the

563\texttt{::} case, the definition

564would not be well typed.

565

566−Often, we need to match on the result of an intermediate computation

566+Often, matching is required on the result of an intermediate computation

567with a dependent type.

568\Idris{} provides a construct for this, the \texttt{with} rule,

569inspired by views in \Epigram~\cite{McBride2004a},

570which takes account of the

571fact that matching on a value in a dependently typed language can affect what

572−we know about the forms of other values.

572+is known about the forms of other values.

573

574For example, a \texttt{Nat} is either even or odd.

575If it is even it will

@@ -598,8 +598,8 @@ parity : (n:Nat) -> Parity n

598\useverb{parityty}

599

600\noindent

601−Using this, we can write a function which converts a natural number to a list

601+Using this, a function which converts a natural number to a list

602−of binary digits (least significant first) as follows, using the \texttt{with}

602+of binary digits (least significant first) is written as follows, using the \texttt{with}

603rule:

604

605\begin{SaveVerbatim}{natToBin}

@@ -619,7 +619,7 @@ because the result

619of \texttt{parity k} depends on \texttt{k}.

620So, as well as the patterns for the result of the

621intermediate computation (\texttt{even} and \texttt{odd}) right of the

622−\texttt{$\mid$}, we also write how

622+\texttt{$\mid$}, the definition also expresses how

623the results affect the other patterns left of the $\mid$. Note that there is a

624function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---

625this is allowed

impl-paper/intro.tex+2−2

@@ -7,7 +7,7 @@ the intended meaning; \emph{dependent} types, where types may be predicated

7on values, allow a programmer to give a program a \emph{precise} type and

8hence have increased confidence of its correctness.

9The \Idris{} language

10−\cite{Brady2011a} aims to take this ideas further, by providing support for

10+\cite{Brady2011a} aims to take this idea further, by providing support for

11verification of \emph{general purpose} systems software. In contrast to Agda and Coq,

12which have arisen from the theorem proving community, \Idris{} takes Haskell as

13its main influence. Recent Haskell extensions such as GADTs and type families have

@@ -75,7 +75,7 @@ core language \TT{} and its typing rules, covering expressions, data types

75and pattern matching; Section \ref{sect:elaboration} describes the method

76for translating \Idris{} to \TT{}, beginning with a restricted language

77\IdrisM{} before extending to higher level features; Section

78−\ref{sect:delab} describes the process for translating back to \Idris{}

78+\ref{sect:delab} describes the process for translating \TT{} back to \Idris{}

79and properties of the translation; finally,

80Section \ref{sect:related} discusses related work and Section \ref{sect:conclusion}

81concludes.

impl-paper/typechecking.tex+14−14

@@ -7,11 +7,11 @@ High level \Idris{} programs, as described in Section \ref{sect:hll}, are

7\TT{} is a dependently typed $\lambda$-calculus with inductive families

8and pattern matching definitions similar to UTT~\cite{luo1994}, and building

9on an earlier implementation, \Ivor{}~\cite{Brady2006b}.

10−We keep the

10+The

11−core language as small as is reasonably possible, which has several advantages: it is

11+core language is kept as small as is reasonably possible, which has several advantages: it is

12easy to type check, since type checking dependent type theory is well understood

13~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping

14−the core language small increases our confidence that these important components of

14+the core language small increases confidence that these important components of

15the language are correct. In this section, we describe \TT{} and

16its semantics.

@@ -26,7 +26,7 @@ The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:

26type of types, and may be extended with other primitives.

27\end{itemize}

29−We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,

29+The function space $\all{\vx}{\vS}\SC\vT$ may also be written as $(\vx\Hab\vS)\to\vT$,

30or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with

31the high level language. Universe levels on sets ($\Type_i$) may be left implicit and

32inferred by the machine~\cite{pollack1990implicit}.

@@ -93,7 +93,7 @@ with a $\LET$ binding.

93\end{itemize}

95\noindent

96−We use the following contextual closure rule to reduce a $\LET$ binding by creating

96+The following contextual closure rule reduces a $\LET$ binding by creating

97a $\delta$-reducible expression:

99\DM{

@@ -366,7 +366,7 @@ the variable may provide enough information for the clause to match.

366In order to implement pattern matching, we must separate the \remph{accessible} and

367\remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible

368to match against it) if it is constructor headed, or a variable. Inaccessible patterns

369−are converted to ``match anything'' patterns. We convert clauses to matchable pattern

369+are converted to ``match anything'' patterns. Clauses are converted to matchable pattern

370clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.

371We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the

372$\MO{Pat}$ operation across a list of arguments.

@@ -433,8 +433,8 @@ $\vx$ requires.

433 \MoRet{

434 \AR{

435 \Success\:\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Success\:(\tx,\tv)$)}\\

436− \Blocked\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\

436+ \Blocked\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\

437− \Failure\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\

437+ \Failure\;\;\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\

438 }

439 } \\

440& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\

@@ -444,8 +444,8 @@ $\vx$ requires.

444& \MO{Match} & (\vc ; \tc) & \ve &

445 \MoRet{

446 \AR{

447− \Success\:\vx\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\

447+ \Success\;\vx\;\;\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\

448− \Blocked\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\

448+ \Blocked\hg\;\;\;\;\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\

449 \MO{Match}\:\tc\:\ve\hg\mbox{(otherwise)}

450 }

451 } \\

@@ -587,10 +587,10 @@ are a convenient abstraction for building proofs and programs by \remph{refineme

587\end{itemize}

588

589The idea behind the \Idris{} elaborator, therefore, is to use the high level program

590−to direct \demph{tactics} to build \TT{} programs by refinement. We implement the

590+to direct \demph{tactics} to build \TT{} programs by refinement. The

591−elaborator as an Embedded Domain Specific Language (EDSL) in Haskell.

591+elaborator is implemented as an Embedded Domain Specific Language (EDSL) in Haskell.

592−In the remainder

592+The remainder

593−of this paper, we describe the EDSL, and demonstrate how it can be used to implement

593+of this paper describes the EDSL and demonstrates how it is used to implement

594all of the high level features of \Idris{}.

595

596