7574d09 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Lots of implementation paper revisions

7574d09Edwin Brady14 years ago

papers/impl-paper/conclusions.tex+4−2

compare with master

unifiedsplit

@@ -126,8 +126,10 @@ it is possible to expose tactics to the programmer. This opens up

126the possibility of implementing domain specific decision procedures, or

127implementing user defined tactics in a style similar to Coq's \texttt{Ltac}

128language \cite{Delahaye2000}. Although \TT{} is primarily intended as a core

129−language for \Idris{}, its rich type system also allows it to capture a number

129+language for \Idris{}, its rich type system also means that it could be used

130−of high level languages, especially when augmented with primitive operators.

130+as a core language for other high level languages, especially when augmented

131+with primitive operators, and used to express additional properties of those

132+languages.

131

133

132We have not discussed the performance of the elaboration

134We have not discussed the performance of the elaboration

133algorithm, or described how \Idris{} compiles to executable code. In practice,

135algorithm, or described how \Idris{} compiles to executable code. In practice,

papers/impl-paper/delab.tex+3−3

@@ -77,12 +77,12 @@ which arguments are implicit or constraint arguments:

77\end{array}

78\medskip\\

79\begin{array}{ll}

80−\MO{UnelabTyDecl}\:\vi\:(\all{\vx}{\vT}\SC\ve)

80+\MO{UnelabTyDecl}\:\vi\:(\all{\vy}{\vT}\SC\ve)

81−\mq & \piimp{\vx}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\

81+\mq & \piimp{\vy}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\

82 & \hg\mbox{(if the $i$th argument to $\vx$ is an implicit argument)} \\

83 & \piconst{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\

84 & \hg\mbox{(if the $i$th argument to $\vx$ is a constraint argument)} \\

85− & \piexp{\vx}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\

85+ & \piexp{\vy}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\

86 & \hg\mbox{(otherwise)} \\

87\end{array}

88}

papers/impl-paper/elaboration.tex+102−73

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

180

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

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

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

183+In an existing proof state $(\vC, \Delta, \ve, \vP, \vQ)$,

184$\MO{NewTerm}\;\vt$ discards the proof term and hole queue, and

185updates the proof state to:

186

@@ -217,6 +217,9 @@ may fail. We have the following primitive meta-operations:

217$\Gamma$, returning its type.

218$\MO{Check}$ will fail

219if the expression is not well-typed.

220+\item $\MO{Convert}_\Gamma\;\ve_1\;\ve_2$, which checks that the well-typed

221+expressions $\ve_1$ and $\ve_2$ respect the cumulativity relation

222+(i.e. $\Gamma\proves\ve_1\cumul\ve_2$), and fails otherwise.

220\item $\Eval\;\ve$, which evaluates a well-typed expression $\ve$ relative to a context

223\item $\Eval\;\ve$, which evaluates a well-typed expression $\ve$ relative to a context

221$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,

224$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,

222but does not reduce definitions which are not total.

225but does not reduce definitions which are not total.

@@ -226,19 +229,20 @@ which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which

226holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative

229holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative

227to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).

230to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).

228\item $\Subst\;\vx\;\ve$, which instantiates a hole $\vx$ directly with a term

231\item $\Subst\;\vx\;\ve$, which instantiates a hole $\vx$ directly with a term

229−$\ve$, typically arising from unification.

232+$\ve$, typically arising from unification and removes $\vx$ from the hole

233+queue.

230\end{itemize}

234\end{itemize}

231

235

232\noindent

236\noindent

233−Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$

237+Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$,

234−and $\MO{NextHole}$

238+$\MO{NextHole}$ and $\MO{RemoveHole}$

235operations which manipulate and inspect

239operations which manipulate and inspect

236the hole queue. $\MO{Focus}\;\vn$ moves a hole to the head of the hole queue:

240the hole queue. $\MO{Focus}\;\vn$ moves a hole to the head of the hole queue:

237

241

238\DM{

242\DM{

239\MO{Focus}\;\vn\;=\;\RW{do}\;\AR{

243\MO{Focus}\;\vn\;=\;\RW{do}\;\AR{

240−(\vC,\Delta,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\

244+(\vC,\Delta,\ve,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\

241−\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ;\vQ')\\

245+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vn;\vQ;\vQ')\\

242}

246}

243}

247}

244

248

@@ -248,25 +252,31 @@ end of the hole queue:

248

252

249\DM{

253\DM{

250\MO{Unfocus}\;=\;\RW{do}\;\AR{

254\MO{Unfocus}\;=\;\RW{do}\;\AR{

251−(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\

255+(\vC,\Delta,\ve,\vP,\vn;\vQ)\gets\MO{Get}\\

252−\MO{Put}\;(\vC,\Delta,\vP,\vQ;\vn)\\

256+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vQ;\vn)\\

253}

257}

254}

258}

255

259

256\noindent

260\noindent

257$\MO{NewHole}$ declares that a new hole has been created and is to be solved

261$\MO{NewHole}$ declares that a new hole has been created and is to be solved

258−next, and $\MO{NextHole}$ returns the next hole to be solved:

262+next; $\MO{NextHole}$ returns the next hole to be solved, and $\MO{RemoveHole}$

263+removes a hole from the head of the queue:

259

264

260\DM{

265\DM{

261\AR{

266\AR{

262\MO{NewHole}\;=\;\RW{do}\;\AR{

267\MO{NewHole}\;=\;\RW{do}\;\AR{

263(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\

268(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\

264−\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ)\\

269+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vn;\vQ)\\

265}

270}

266\\

271\\

267\MO{NextHole}\;=\;\RW{do}\;\AR{

272\MO{NextHole}\;=\;\RW{do}\;\AR{

268−(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\

273+(\vC,\Delta,\ve,\vP,\vn;\vQ)\gets\MO{Get}\\

269−\MO{Return}\;\vn

274+\RW{return}\;\vn

275+}

276+\\

277+\MO{RemoveHole}\;=\;\RW{do}\;\AR{

278+(\vC,\Delta,\ve,\vP,\vn;\vQ)\gets\MO{Get}\\

279+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vQ)

270}

280}

271}

281}

272}

282}

@@ -278,18 +288,21 @@ form:

278

288

279\DM{

289\DM{

280\PA{\A\A}{

290\PA{\A\A}{

281−\MO{Tactic}_\Gamma & \;\vec{\VV{args}} & \;\vt & \MoRet{\vt'}

291+\MO{Tac}_\Gamma & \;\vec{\VV{args}} & \;\vt & \MoRet{\RW{do}\;\AR{

292+\ldots\\

293+\RW{return}\:\vt'}

294+}

282}

295}

283}

296}

284

297

285−A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed

298+A tactic $\MO{Tac}$ takes a sequence of zero or more arguments

286−by the sub-term $\vt$ on which it is operating. It runs relative to a context

299+$\vec{\VV{args}}$ followed by the sub-term $\vt$ on which it is operating. It

287−$\Gamma$ which contains all the bindings and pattern bindings in scope at that

300+runs relative to a context $\Gamma$ which contains all the bindings and pattern

288−point in the term. The sub-term $\vt$ will either be a hole binding

301+bindings in scope at that point in the term. The sub-term $\vt$ will either be

289−$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The

302+a hole binding $\hole{\vx}{\vT}\SC\ve$ or a guess binding

290−tactic returns a new term $\vt'$ which can take any form, provided it is

303+$\guess{\vx}{\vT}{\vv}\SC\ve$. The tactic returns a new term $\vt'$ which can

291−well-typed, with a type convertible to the type of $\vt$.

304+take any form, provided it is well-typed, with a type convertible to the type

292−Tactics may also have the side effect of updating the proof state,

305+of $\vt$. Tactics may also have the side effect of updating the proof state,

293therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.

306therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.

294

307

295Tactics are executed by a higher level meta-operation $\MO{Tactic}$,

308Tactics are executed by a higher level meta-operation $\MO{Tactic}$,

@@ -321,23 +334,23 @@ tactic.

321& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)

334& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)

322& \MoRet{

335& \MoRet{

323\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

336\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

324−\lam{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\lam{\vx}{\vT'})\;\ve}

337+\RW{return}\;(\lam{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\lam{\vx}{\vT'})\;\ve)}

325}

338}

326\\

339\\

327& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)

340& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)

328& \MoRet{

341& \MoRet{

329\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

342\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

330−\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve}

343+\RW{return}\;(\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve)}

331}

344}

332\\

345\\

333& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)

346& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)

334& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\

347& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\

335\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

348\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

336−\LET\;\vx\defq\vt'\Hab\vT'\SC

349+\RW{return}\;(\LET\;\vx\defq\vt'\Hab\vT'\SC

337−\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve}} \\

350+\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve)}} \\

338& \MO{Tactic'} & \Gamma & (\vf\;\va) &

351& \MO{Tactic'} & \Gamma & (\vf\;\va) &

339−\MoRet{\MO{Return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\

352+\MoRet{\RW{return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\

340−& \MO{Tactic'} & \Gamma & \vt & \MoRet{\MO{Return}\;\vt}

353+& \MO{Tactic'} & \Gamma & \vt & \MoRet{\RW{return}\;\vt}

341}

354}

342}

355}

343}

356}

@@ -385,7 +398,7 @@ resolve the existing problems with $\MO{ReUnify}$.

385\AR{

398\AR{

386(\tx=\te,\tp)\gets\PrimUnify\;\ve_1\;\ve_2\\

399(\tx=\te,\tp)\gets\PrimUnify\;\ve_1\;\ve_2\\

387\vec{\MO{Subst}}\;\tx\;\te\\

400\vec{\MO{Subst}}\;\tx\;\te\\

388−\MO{SubstProblems}\;(\tx=\te)\\

401+\MO{SubstProblems}\;\tx\;\te\\

389(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\

402(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\

390\vec{\MO{ReUnify}}\;\tP

403\vec{\MO{ReUnify}}\;\tP

391}

404}

@@ -395,7 +408,7 @@ resolve the existing problems with $\MO{ReUnify}$.

395\MO{ReUnify}\;(\Gamma,\ve_1,\ve_2)\;=\;\RW{do}\;\AR{

408\MO{ReUnify}\;(\Gamma,\ve_1,\ve_2)\;=\;\RW{do}\;\AR{

396(\tx=\te,\tp)\Gets\PrimUnify\;\ve_1\;\ve_2\\

409(\tx=\te,\tp)\Gets\PrimUnify\;\ve_1\;\ve_2\\

397\vec{\MO{Subst}}\;\tx\;\te\\

410\vec{\MO{Subst}}\;\tx\;\te\\

398−\MO{Return}\;\tp

411+\RW{return}\;\tp

399}

412}

400}

413}

401}

414}

@@ -413,14 +426,16 @@ keeping $\vx$ at the head:

413\DM{

426\DM{

414\PA{\A\A}{

427\PA{\A\A}{

415\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &

428\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &

429+ \MoRet{\RW{do}\;\AR{\MO{NewHole}\;\vy\\

416− \MoRet{\RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\

430+ \RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve}} \\

417}

431}

418}

432}

419

433

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

434+An obvious difficulty is in ensuring that names are unique throughout a proof

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

435+term. The implementation ensures that any hole created by the $\MO{NewHole}$

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

436+operation has a unique name by checking against existing names in scope and

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

437+modifying the name if necessary. In this paper, we will assume that all created

438+names are fresh.

424

439

425The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal

440The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal

426with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to

441with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to

@@ -474,12 +489,14 @@ Therefore the resulting proof term is:

474

489

475The $\MO{Solve}$ tactic operates on a guess binding. If the guess is \remph{pure}, i.e., it

490The $\MO{Solve}$ tactic operates on a guess binding. If the guess is \remph{pure}, i.e., it

476is a \TT{} term containing no hole or guess bindings, then the value attached to

491is a \TT{} term containing no hole or guess bindings, then the value attached to

477−the guess is substituted into its scope:

492+the guess is substituted into its scope, and the corresponding hole removed

493+from the hole queue:

478

494

479\DM{

495\DM{

480\PA{\A}{

496\PA{\A}{

481\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &

497\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &

498+ \MoRet{\RW{do}\;\AR{\MO{RemoveHole}\\

482− \MoRet{\RW{return}\;\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\;\vv$)}}

499+ \RW{return}\;\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\;\vv$)}}}

483}

500}

484}

501}

485

502

@@ -523,13 +540,15 @@ binding requires that the goal normalises to a function type:

523}

540}

524

541

525\noindent

542\noindent

526−Creating a $\forall$ binding requires that the goal is a $\TC{Type}$:

543+Creating a $\forall$ binding requires that the goal type converts

544+with $\TC{Type}$:

527

545

528\DM{

546\DM{

529\PA{\A\A}{

547\PA{\A\A}{

530\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &

548\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &

531 \MoRet{\RW{do}\;\AR{

549 \MoRet{\RW{do}\;\AR{

532− \Type\;\leftarrow\;\Check\;\vS\\

550+ \vV\;\leftarrow\;\Check\;\vS\\

551+ \MO{Convert}_\Gamma\;\vV\;\Type\\

533 \RW{return}\;\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx

552 \RW{return}\;\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx

534 }

553 }

535 }

554 }

@@ -543,7 +562,8 @@ Creating a $\LET$ binding requires a type and a value.

543\PA{\A\A}{

562\PA{\A\A}{

544\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &

563\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &

545 \MoRet{\RW{do}\;\AR{

564 \MoRet{\RW{do}\;\AR{

546− \Type\;\leftarrow\;\Check\;\vS\\

565+ \vV\;\leftarrow\;\Check\;\vS\\

566+ \MO{Convert}_\Gamma\;\vV\;\Type\\

547 \vS'\;\leftarrow\;\Check\;\vv\\

567 \vS'\;\leftarrow\;\Check\;\vv\\

548 \Unify\;\vS\;\vS'\\

568 \Unify\;\vS\;\vS'\\

549 \RW{return}\;\LET\;\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx

569 \RW{return}\;\LET\;\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx

@@ -798,11 +818,11 @@ Note in particular that each tactic which introduces a guess ($\MO{Fill}$

798and $\MO{Solve}$ is closed with a $\MO{Solve}$).

818and $\MO{Solve}$ is closed with a $\MO{Solve}$).

799

819

800Setting up elaboration in this way, with a proof state captured in a monad,

820Setting up elaboration in this way, with a proof state captured in a monad,

801−and a primitive collection of tactics,

821+and a primitive collection of tactics, makes it easy to derive more complex

802−makes it easy to derive more complex tactics for elaborating higher level language constructs,

822+tactics for elaborating higher level language constructs, in much the same way

803−in much the same way as the \texttt{Ltac} language in Coq. As a result, the

823+as the \texttt{Ltac} language in Coq~\cite{Delahaye2000}. As a result, the

804−description of elaboration of

824+description of elaboration of a language construct (or a program such as

805−a language construct (or a program such as $\FN{id}$) bears a strong resemblance to

825+$\FN{id}$) bears a strong resemblance to

806a Coq proof script.

826a Coq proof script.

807

827

808\FFIG{

828\FFIG{

@@ -865,11 +885,9 @@ The system state is a tuple, $(\vC,\vA,\vI)$, containing:

865\item Type class information, $\vI$, containing method signatures and dictionaries for type classes

885\item Type class information, $\vI$, containing method signatures and dictionaries for type classes

866\end{itemize}

886\end{itemize}

867

887

868−In the implementation, the system state is captured in a monad, \texttt{Idris}.

888+In the implementation, the system state is captured in a monad, \texttt{Idris},

869−This monad includes additional information such as syntax overloadings,

889+which includes additional information such as syntax overloadings, command line

870−command line options, and optimisations, which do not concern us here. Elaboration

890+options, and optimisations, which do not concern us here.

871−of expressions requires access to the system state in particular in order to expand

872−implicit arguments and resolve type classes.

873

891

874For each global name, $\vA$ records whether its arguments are explicit, implicit,

892For each global name, $\vA$ records whether its arguments are explicit, implicit,

875or type class constraints. For example, recall the declaration

893or type class constraints. For example, recall the declaration

@@ -996,7 +1014,7 @@ We will use a subset of full \Idris{}, which we call \IdrisM{}, to explain

996elaboration of expressions. \IdrisM{} expression syntax is given in Figure

1014elaboration of expressions. \IdrisM{} expression syntax is given in Figure

997\ref{idrism} and declaration syntax given in Figure \ref{idrismd}.

1015\ref{idrism} and declaration syntax given in Figure \ref{idrismd}.

998\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without

1016\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without

999−tuple syntax, \texttt{do}-notation or infix operators --- and with implicit

1017+\texttt{do}-notation or infix operators --- and with implicit

1000arguments in types bound explicitly

1018arguments in types bound explicitly

1001(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\va\;\vn$

1019(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\va\;\vn$

1002instead of simply $\Vect\;\va\;\vn$).

1020instead of simply $\Vect\;\va\;\vn$).

@@ -1147,7 +1165,9 @@ $\vV$ and $\vX$.

1147\ttinterp{\ve}

1165\ttinterp{\ve}

1148}

1166}

1149}

1167}

1150−\subsubsection{Elaborating applications}

1168+\subsubsection{Elaborating Applications}

1169+

1170+\label{sect:elabapps}

1151

1171

1152There are two cases to consider when elaborating applications:

1172There are two cases to consider when elaborating applications:

1153

1173

@@ -1200,17 +1220,21 @@ Finally, any type class instance arguments are resolved with the

1200built-in $\MO{Instance}$ tactic.

1220built-in $\MO{Instance}$ tactic.

1201

1221

1202\DM{

1222\DM{

1203−\ttinterp{\vx\;\ta}\;\mq\;

1204\AR{

1223\AR{

1224+\ttinterp{\vx\;\ta}\;\mq\;

1205\RW{do}\;

1225\RW{do}\;

1206\AR{

1226\AR{

1207(\tn,\tv)\;\gets\;\MO{Expand}\;\vx\;\ta\\

1227(\tn,\tv)\;\gets\;\MO{Expand}\;\vx\;\ta\\

1208\vec{\MO{Claim}}\;(\tn\Hab\tT)\\

1228\vec{\MO{Claim}}\;(\tn\Hab\tT)\\

1209\MO{Fill}\;\vx\;\tn\\

1229\MO{Fill}\;\vx\;\tn\\

1210−\vec{\MO{Focus}}\;\tn;\;\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\

1230+\vec{\MO{ElabArg}}\;\tn\;\tv\hg\mbox{(for non-placeholder $\vv$)}\\

1211\MO{Solve} \\

1231\MO{Solve} \\

1212\vec{\MO{Instance}}\;\tn\hg\mbox{(for type class constraint argument $\vn$)}

1232\vec{\MO{Instance}}\;\tn\hg\mbox{(for type class constraint argument $\vn$)}

1213}

1233}

1234+\medskip

1235+\\

1236+\MO{ElabArg}\;\vn\;\vv\;\mq\;

1237+\MO{Focus}\;\vn;\;\ttinterp{\vv}

1214}

1238}

1215}

1239}

1216

1240

@@ -1220,10 +1244,10 @@ context, then recursively searches the global context. $\MO{Instance}$ is covere

1220in detail in Section \ref{sect:instance}.

1244in detail in Section \ref{sect:instance}.

1221

1245

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

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

1223−arbitrary argument, we need not worry about implicit arguments or class

1247+arbitrary argument (possibly with a dependent type), we need not worry about

1224−constraints. Instead, the function and argument are elaborated, and the results

1248+implicit arguments or class constraints. Instead, the function and argument are

1225−applied. Since elaboration is type directed, however, there must be an

1249+elaborated, and the results applied. Since elaboration is type directed,

1226−appropriate type for the function.

1250+however, there must be an appropriate type for the function.

1227

1251

1228\DM{

1252\DM{

1229\ttinterp{\ve\;\va}\;\mq\;\RW{do}\;

1253\ttinterp{\ve\;\va}\;\mq\;\RW{do}\;

@@ -1446,24 +1470,25 @@ ftest' n False x = ...

1446

1470

1447\noindent

1471\noindent

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

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

1449−automatically. It checks the left hand side, resulting in a set of patterns

1473+automatically. The elaborator checks the left hand side, resulting in a set of

1474+patterns $\tp$, then infers a type $\vW$ for the expression $\vw$. The patterns

1450−$\tp$, then splits these patterns into those necessary to type

1475+$\tp$ are then split into those necessary to type $\vW$, and the rest ($\tp_w$

1451−$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using

1476+and $\tp_n$ respectively) using

1452$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over

1477$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over

1453−the matched expression $\ve$ in the types of $\tp_n$.

1478+the matched expression $\vw$ in the types of $\tp_n$.

1454$\MO{Abstract}\;\ve\;\vw\;\vp$ simply replaces any occurrence of $\vw$ in

1479$\MO{Abstract}\;\ve\;\vw\;\vp$ simply replaces any occurrence of $\vw$ in

1455$\vp$ with the name $\ve$.

1480$\vp$ with the name $\ve$.

1456

1481

1457\DM{

1482\DM{

1458\AR{

1483\AR{

1459−\MO{ElabClause}\;(\vx\;\ttt\;\iwith\;\ve\;\vec{\VV{pclause}})\;\mq\\

1484+\MO{ElabClause}\;(\vx\;\ttt\;\iwith\;\vw\;\vec{\VV{pclause}})\;\mq\\

1460\hg\hg\edo{

1485\hg\hg\edo{

1461\MO{NewProof}\;\TC{Infer};\;

1486\MO{NewProof}\;\TC{Infer};\;

1462\ttinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\

1487\ttinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\

1463\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\

1488\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\

1464\tp\gets\MO{Patterns}\\

1489\tp\gets\MO{Patterns}\\

1465\MO{NewTerm}\;\TC{Infer};\;

1490\MO{NewTerm}\;\TC{Infer};\;

1466−\ttinterp{\DC{MkInfer}\;\_\;\ve}\\

1491+\ttinterp{\DC{MkInfer}\;\_\;\vw}\\

1467\DC{MkInfer}\;\vW\;\vw'\gets\MO{Term}\\

1492\DC{MkInfer}\;\vW\;\vw'\gets\MO{Term}\\

1468(\tp_w,\tp_n)\;\gets\;\MO{SplitContext}\;\vW\;\tp\\

1493(\tp_w,\tp_n)\;\gets\;\MO{SplitContext}\;\vW\;\tp\\

1469\MO{TTDecl}\;(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\;\ve\;\vw'\;\tp_{n}\to\vT)\\

1494\MO{TTDecl}\;(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\;\ve\;\vw'\;\tp_{n}\to\vT)\\

@@ -1508,7 +1533,9 @@ Therefore, a type class declaration elaborates to a record type containing all

1508of the functions in the class, and an instance is simply an instance of the

1533of the functions in the class, and an instance is simply an instance of the

1509record. The methods are translated to top level functions which extract the

1534record. The methods are translated to top level functions which extract the

1510relevant function from the dictionary. For example, for the \texttt{Show} type

1535relevant function from the dictionary. For example, for the \texttt{Show} type

1511−class, the \texttt{class} declaration is translated to:

1536+class, the \texttt{class} declaration is translated (in the elaborated code,

1537+using the surface \Idris{} syntax for readability)

1538+to:

1512

1539

1513\begin{SaveVerbatim}{showdata}

1540\begin{SaveVerbatim}{showdata}

1514

1541

@@ -1670,8 +1697,9 @@ constructing programs in \TT{}.

1670\label{sect:instance}

1697\label{sect:instance}

1671

1698

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

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

1700+unification as described in Section \ref{sect:elabapps}, and type class

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

1701+constraints by an $\MO{Instance}$ tactic which searches the context for an

1674−the context for an instance of the required type class.

1702+instance of the required type class.

1675

1703

1676The $\MO{Instance}$ tactic begins by trying to find a solution in the local context,

1704The $\MO{Instance}$ tactic begins by trying to find a solution in the local context,

1677using the $\MO{Trivial}$ tactic, which attempts

1705using the $\MO{Trivial}$ tactic, which attempts

@@ -1788,9 +1816,9 @@ the vector append function, containing a metavariable \texttt{append\_rec}:

1788

1816

1789\begin{SaveVerbatim}{vappmv}

1817\begin{SaveVerbatim}{vappmv}

1790

1818

1791−(++) : Vect A n -> Vect A m -> Vect A (n + m)

1819+(++) : Vect a n -> Vect a m -> Vect a (n + m)

1792−(++) Nil ys = ys

1820+Nil ++ ys = ys

1793−(++) (x :: xs) ys = x :: ?append_rec

1821+(x :: xs) ++ ys = x :: ?append_rec

1794

1822

1795\end{SaveVerbatim}

1823\end{SaveVerbatim}

1796\useverb{vappmv}

1824\useverb{vappmv}

@@ -1862,10 +1890,11 @@ lookup_default_case i xs def (Just x) = x

1862\end{SaveVerbatim}

1890\end{SaveVerbatim}

1863\useverb{listlookupmv}

1891\useverb{listlookupmv}

1864

1892

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

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

1894+of the $\icase$ expression, introducing a new name $\VV{scrutinee}$, and

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

1895+creating a metavariable $\VV{xcase}$ to implement the pattern matching. Then

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

1896+the elaborator builds a new pattern matching definition for $\VV{xcase}$ and

1868−and elaborate it:

1897+elaborates it:

1869

1898

1870\DM{

1899\DM{

1871\AR{

1900\AR{

papers/impl-paper/hll.tex+10−13

@@ -5,7 +5,8 @@

5\Idris{} is

6a pure functional programming language with dependent types. It is

7eagerly evaluated by default, and compiled via the Epic supercombinator

8−library \cite{brady2011epic}.

8+library~\cite{brady2011epic}, with irrelevant values and proof terms

9+automatically erased~\cite{Brady2003,Brady2005}.

9In this section, I will give a brief introduction to programming in \Idris{},

10In this section, I will give a brief introduction to programming in \Idris{},

10covering the most important features. A full tutorial is available elsewhere

11covering the most important features. A full tutorial is available elsewhere

11\cite{idristutorial}.

12\cite{idristutorial}.

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

38\useverb{constprims}

39\useverb{constprims}

40\noindent

41\noindent

41−Like Haskell, the main function

42+Like Haskell, the main function is called \texttt{main}, and input and output

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

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

43+is managed with an \texttt{IO} monad. Unlike Haskell, however, \remph{all} top

44−signature, emphasising the importance of types,

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

46−signature. This is due to type inference being, in general,

44+level functions must have a type signature. This is due to type inference

47−undecidable for languages with

45+being, in general, undecidable for languages with dependent types.

48−dependent types.

50A module declaration also opens a \remph{namespace}. The fully qualified names

47A module declaration also opens a \remph{namespace}. The fully qualified names

51declared in this module are \texttt{Main.x} and \texttt{Main.main}.

48declared in this module are \texttt{Main.x} and \texttt{Main.main}.

@@ -171,7 +168,7 @@ Any names which are visible in the outer scope are also visible in the

171\texttt{where} clause (unless they are redefined in the \texttt{where} clause,

168\texttt{where} clause (unless they are redefined in the \texttt{where} clause,

172such as \texttt{xs} here). A name which appears only in the type will be in

169such as \texttt{xs} here). A name which appears only in the type will be in

173scope in the \texttt{where} clause if it is a \remph{parameter} to one of the

170scope in the \texttt{where} clause if it is a \remph{parameter} to one of the

174−types, i.e. it is fixed across the entire structure. In particular, this means

171+types, i.e. it is fixed across the entire data structure. In particular, this means

175that the \texttt{a} in the definition of \texttt{reverse} above is the

172that the \texttt{a} in the definition of \texttt{reverse} above is the

176\remph{same} \texttt{a} as in the definition of \texttt{revAcc}, as \texttt{a}

173\remph{same} \texttt{a} as in the definition of \texttt{revAcc}, as \texttt{a}

177is a parameter of \texttt{List}.

174is a parameter of \texttt{List}.

@@ -206,7 +203,7 @@ of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

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

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

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

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

208The distinction between parameters and indices is that a parameter is fixed

205The distinction between parameters and indices is that a parameter is fixed

209−across an entire structure, whereas an index may vary.

206+across an entire data structure, whereas an index may vary.

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

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

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

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

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

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

@@ -247,7 +244,7 @@ This declares

247\tDC{fO} as the zeroth element of a finite set with \texttt{S k} elements;

244\tDC{fO} as the zeroth element of a finite set with \texttt{S k} elements;

248\texttt{fS n} as the

245\texttt{fS n} as the

249\texttt{n+1}th element of a finite set with \texttt{S k} elements.

246\texttt{n+1}th element of a finite set with \texttt{S k} elements.

250−\tTC{Fin} is indexed by a \tTC{Nat}, which

247+\tTC{Fin} is indexed by \tTC{Nat}, which

251represents the number of elements in the set.

248represents the number of elements in the set.

252Neither constructor targets \texttt{Fin O}, because we cannot construct an

249Neither constructor targets \texttt{Fin O}, because we cannot construct an

253element of an empty set.

250element of an empty set.

@@ -412,7 +409,7 @@ class Show a where

412\useverb{showclass}

409\useverb{showclass}

413

410

414\noindent

411\noindent

415−This generates a function of the following type (which we call a \emph{method} of the

412+This declares a function of the following type (which we call a \emph{method} of the

416\texttt{Show} class):

413\texttt{Show} class):

417

414

418\begin{SaveVerbatim}{showty}

415\begin{SaveVerbatim}{showty}

papers/impl-paper/impldtp.tex+6−6

@@ -54,7 +54,7 @@

56\title

57−[Idris, a General Purpose Dependently Typed Programm Language]

57+[Idris, a General Purpose Dependently Typed Programming Language]

58{Idris, a General Purpose Dependently Typed Programming Language:

59Design and Implementation}

60%Implementing General Purpose Dependently Typed Programming Languages}

@@ -74,8 +74,8 @@ Many components of a dependently typed programming language are by now well

74understood, for example the underlying type theory, type checking, unification and

75evaluation. How to combine these components into a realistic and usable high

76level language is, however, folklore, discovered anew by successive

77−language implementations. In this paper, I describe the implementation of a

77+language implementations. In this paper, I describe the implementation of

78−new dependently typed functional programming language, \Idris{}.

78+\Idris{}, a new dependently typed functional programming language.

79\Idris{} is intended to be a \emph{general purpose} programming language

80and as such provides high level concepts such as implicit syntax,

81type classes and \texttt{do} notation.

@@ -133,9 +133,9 @@ implementation of new high level language constructs.

133

134This work was funded by the Scottish Informatics and Computer Science Alliance

135(SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE). My thanks to

136−Philip H\"{o}lzenspies, Kevin Hammond and Vilhelm Sj\"{o}berg for their

136+Philip H\"{o}lzenspies, Kevin Hammond, Vilhelm Sj\"{o}berg and Falko Spiller

137−comments on an earlier draft of this paper, and to the anonymous referees for

137+for their comments on an earlier draft of this paper, and to the anonymous

138−their many insightful and constructive comments.

138+referees for their many insightful and constructive comments.

139

140\bibliographystyle{jfp}

141\bibliography{library.bib}

papers/impl-paper/intro.tex+2−2

@@ -4,7 +4,7 @@ Dependently typed programming languages, such as Agda \cite{norell2007thesis}

4and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach

5to ensuring the correctness of software. Type checking ensures a program has

6the intended meaning; \emph{dependent} types, where types may be predicated

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

7+on values, allow a programmer to give a program a more precise type and

8hence have increased confidence of its correctness.

9The \Idris{} language

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

@@ -121,7 +121,7 @@ This illustrates some basic features of \Idris{}:

121

122\begin{itemize}

123\item A single colon is used for type signatures, and a double colon for the

124−cons operator.

124+cons operator, emphasising the importance of types.

125\item Functions are defined by pattern matching, with a top level type signature.

126Names which are free in the type signature (\texttt{a} and \texttt{n}) here

127are implicitly bound.

papers/impl-paper/library.bib+20−12

@@ -1,18 +1,13 @@

1Automatically generated by Mendeley 1.6

2Any changes to this file will be lost if it is regenerated by Mendeley.

4−@techreport{Haskell98,

4+@inproceedings{Delahaye,

5−abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},

5+author = {Delahaye, David},

6−author = {{Peyton Jones}, Simon},

6+booktitle = {Proceedings of Logic for Programming and Automated Reasoning ({LPAR})},

7−booktitle = {Language},

7+file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/A Tactic Language for the System Coq/Delahaye - A Tactic Language for the System Coq - 2000(3).pdf:pdf},

8−editor = {Jones, Simon Peyton},

8+title = {{A Tactic Language for the System Coq}},

9−isbn = {0521826144},

9+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.9062},

10−number = {1},

11−publisher = {Cambridge University Press},

12−title = {{Haskell 98 Language and Libraries: The Revised Report}},

13−url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},

14−volume = {13},

15−year = {2002}

10+year = {2000}

16}

11}

17@inproceedings{McBride2006,

12@inproceedings{McBride2006,

18author = {McBride, C and Goguen, H and McKinna, J},

13author = {McBride, C and Goguen, H and McKinna, J},

@@ -146,6 +141,19 @@ author = {Walt, Paul Van Der and Swierstra, Wouter},

146file = {:Users/edwin/Documents/Mendeley Desktop/Walt, Swierstra/Engineering Proof by Reflection in Agda/Walt, Swierstra - Engineering Proof by Reflection in Agda - Unknown.pdf:pdf},

141file = {:Users/edwin/Documents/Mendeley Desktop/Walt, Swierstra/Engineering Proof by Reflection in Agda/Walt, Swierstra - Engineering Proof by Reflection in Agda - Unknown.pdf:pdf},

147title = {{Engineering Proof by Reflection in Agda}}

142title = {{Engineering Proof by Reflection in Agda}}

148}

143}

144+@techreport{Haskell98,

145+abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},

146+author = {{Peyton Jones}, Simon},

147+booktitle = {Language},

148+editor = {Jones, Simon Peyton},

149+isbn = {0521826144},

150+number = {1},

151+publisher = {Cambridge University Press},

152+title = {{Haskell 98 Language and Libraries: The Revised Report}},

153+url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},

154+volume = {13},

155+year = {2002}

156+}

149@inproceedings{madhavapeddy2007melange,

157@inproceedings{madhavapeddy2007melange,

150author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},

158author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},

151booktitle = {ACM SIGOPS Operating Systems Review},

159booktitle = {ACM SIGOPS Operating Systems Review},

papers/impl-paper/typechecking.tex+27−23

@@ -20,9 +20,9 @@ its semantics.

20The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:

22\begin{itemize}

23−\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.

23+\item \demph{Terms}, $\vt$, which can be variables, bindings, applications or constants.

24−\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.

24+\item \demph{Bindings}, $\vb$, which can be lambda abstractions, let bindings, or function spaces.

25−\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the

25+\item \demph{Constants}, $\vc$, which can be integer or string literals, or $\Type_i$, the

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

27\end{itemize}

@@ -33,8 +33,8 @@ inferred by the machine~\cite{pollack1990implicit}.

34\FFIG{

35\begin{array}{rll@{\hg}rll}

36−\vt ::= & \vc & (\mbox{constant}) &

36+\mbox{Terms,}\;\vt ::= & \vc & (\mbox{constant}) &

37−\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\

37+\;\mbox{Binders,}\;\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\

39 \mid & \vx & (\mbox{variable}) &

40 \mid & \LET\;\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\

@@ -47,7 +47,7 @@ inferred by the machine~\cite{pollack1990implicit}.

47% & & &

48% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\

49\medskip\\

50− \vc ::= & \Type_i & (\mbox{type universes}) \\

50+\mbox{Constants,}\;\vc ::= & \Type_i & (\mbox{type universes}) \\

51 \mid & \vi & (\mbox{integer literal}) \\

52 \mid & \VV{str} & (\mbox{string literal}) \\

53\end{array}

@@ -93,8 +93,9 @@ by one of the following schemes:

94\begin{itemize}

95\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for

96+the bound variable.

96−the bound variable. We define $\beta$-contraction simply by replacing the $\lambda$-binding

97+%We define $\beta$-contraction simply by replacing the $\lambda$-binding

97−with a $\LET$ binding.

98+%with a $\LET$ binding.

98\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.

99\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.

99\end{itemize}

100\end{itemize}

100

101

@@ -122,7 +123,9 @@ reduction rules.

122\begin{array}{lc}

123\begin{array}{lc}

123\beta\mathrm{-contraction} &

124\beta\mathrm{-contraction} &

124\Axiom{

125\Axiom{

125−\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\;\vs\leadsto\LET\;\vx\defq\vs\Hab\vS\SC\vt

126+\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\;\vs\leadsto

127+\vt[\vs/\vx]

128+%\LET\;\vx\defq\vs\Hab\vS\SC\vt

126} \\

129} \\

127\delta\mathrm{-contraction} &

130\delta\mathrm{-contraction} &

128\Axiom{

131\Axiom{

@@ -141,10 +144,11 @@ reduction rules.

141

144

142\label{sect:typerules}

145\label{sect:typerules}

143

146

144−The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.

147+The type inference rules for \TT{} expressions are given in Figure

145−These rules use the \demph{cumulativity} relation, defined in

148+\ref{typerules}. These rules use the \demph{cumulativity} relation, defined in

146−Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,

149+Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe

147−to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at

150+level, to prevent Girard's paradox~\cite{coquand1986analysis}. There is an

151+infinite hierarchy of predicative universes. Cumulativity allows programs at

148lower universe levels to inhabit higher universe levels. In practice, universe levels

152lower universe levels to inhabit higher universe levels. In practice, universe levels

149can be left implicit (and will be left implicit in the rest of this paper) ---

153can be left implicit (and will be left implicit in the rest of this paper) ---

150the type checker generates a graph of constraints between universe levels (such

154the type checker generates a graph of constraints between universe levels (such

@@ -513,7 +517,7 @@ trees~\cite{Augustsson1985}.

513{Metatheoretic properties of \TT{}}

517{Metatheoretic properties of \TT{}}

514{metatheory}

518{metatheory}

515

519

516−We assume that \TT{} respects the usual metatheoretic properties, as shown in

520+We conjecture that \TT{} respects the usual metatheoretic properties, as shown in

517Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property

521Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property

518(i.e. that distinct reduction sequences lead to the same normal form);

522(i.e. that distinct reduction sequences lead to the same normal form);

519\demph{subject reduction} (i.e. that computation preserves type); the

523\demph{subject reduction} (i.e. that computation preserves type); the

@@ -536,9 +540,10 @@ takes a simple but pragmatic and effective approach to termination checking:

536any functions which do not satisfy a syntactic constraint on recursive calls

540any functions which do not satisfy a syntactic constraint on recursive calls

537are marked as \emph{partial}. Additionally, any function which calls a partial

541are marked as \emph{partial}. Additionally, any function which calls a partial

538function or uses a data type which is not strictly positive is also marked as

542function or uses a data type which is not strictly positive is also marked as

539−partial. The syntactic constraint we use is that a recursive call in a pattern

543+partial. We use the size change principle~\cite{Lee2001} to determine whether

540−clause must have an argument which is structurally smaller than an input

544+(possibly mutually defined) recursive functions are guaranteed to

545+terminate.

541−argument in the same position. \TT{} also marks functions which do not cover

546+\TT{} also marks functions which do not cover

542all possible inputs as partial. This totality checking is independent of the

547all possible inputs as partial. This totality checking is independent of the

543rest of the type theory, and can be extended.

548rest of the type theory, and can be extended.

544

549

@@ -601,11 +606,12 @@ vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

601\end{SaveVerbatim}

606\end{SaveVerbatim}

602\useverb{vAddImpSolve}

607\useverb{vAddImpSolve}

603

608

604−Finally, to build the \TT{} definition, we need to find the type of each pattern variable

609+Finally, to build the \TT{} definition, we need to find the type of each

605−and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},

610+pattern variable and state it explicitly. This leads to the following

606−switching to \TT{} notation from the ASCII \Idris{} syntax.

611+\TT{} definition, switching to \TT{} notation from the ASCII \Idris{}

612+syntax:

607

613

608−\FFIG{

614+\DM{

609\AR{

615\AR{

610\FN{vAdd} \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\;\va\to

616\FN{vAdd} \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\;\va\to

611 \Vect\;\va\;\vn\to\Vect\;\va\;\vn\to\Vect\;\va\;\vn\\

617 \Vect\;\va\;\vn\to\Vect\;\va\;\vn\to\Vect\;\va\;\vn\\

@@ -626,8 +632,6 @@ switching to \TT{} notation from the ASCII \Idris{} syntax.

626}

632}

627}

633}

628}

634}

629−{Pairwise addition of vectors in \TT{}}

630−{ttvadd}

631

635

632\subsubsection{An Observation: Programming vs Theorem Proving}

636\subsubsection{An Observation: Programming vs Theorem Proving}

633

637