0af8a2e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Work on implementation paper; tutorial fixes

commit0af8a2ee9f2899693164617bfe2534025a424fb5 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 7 Mar 2012, 10:39 (15 years ago) parent8d4a93b

11 files changed+936−215

compare with master

unifiedsplit

CHANGELOG+9 impl-paper/hll.tex+614 impl-paper/impldtp.tex+2 impl-paper/intro.tex+11 impl-paper/library.bib+236−184 impl-paper/macros.ltx+4 impl-paper/typechecking.tex+30−1 tutorial/classes.tex+1−1 tutorial/intro.tex+1−1 tutorial/miscellany.tex+1−1 tutorial/typesfuns.tex+27−27

CHANGELOG+9

@@ -1,3 +1,12 @@

1+New in 0.9.3:

2+-------------

4+User visible changes:

6+Internal changes:

8+* Normalise before forcing to catch more forceable arguments

110New in 0.9.2:

211-------------

312

impl-paper/hll.tex+614

@@ -1 +1,615 @@

11\section{\Idris{} --- the High Level Language}

3+\label{sect:hll}

5+In this section, we give a brief introduction to programming in \Idris{}.

6+A more detailed tutorial is available~\cite{idristutorial}.

8+\subsection{Preliminaries}

10+\Idris{} defines several primitive types: \tTC{Int}, \tTC{Integer} and

11+\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for

12+text manipulation, and \tTC{Ptr} which represents foreign pointers.

13+There are also several data types declared in the library, including

14+\tTC{Bool}, with values \tDC{True} and \tDC{False}. All of the usual

15+arithmetic and comparison operators are defined for the primitive types,

16+and are overloaded using type classes.

17+

18+An \Idris{} program consists of a module declaration, followed by an optional

19+list of imports and a collection of definitions and declarations, a simple example

20+of which is shown in Figure \ref{constprims}. Like Haskell, the main function

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

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

23+declarations, and \remph{all} functions must have a top level type

24+declaration, since type inference is in general undecidable for languages with

25+dependent types.

26+

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

28+declared in this module are \texttt{main.x} and \texttt{main.main}.

29+

30+\begin{SaveVerbatim}{constprims}

31+

32+module main

33+

34+x : Int

35+x = 42

36+

37+main : IO ()

38+main = putStrLn ("The answer is " ++ show x)

39+

40+\end{SaveVerbatim}

41+\codefig{constprims}{A simple \Idris{} module}

42+

43+\subsection{Types and Functions}

44+

45+Data types are declared in a similar way to Haskell data types, with a similar

46+syntax. Natural numbers and lists, for example, are declared as follows in the

47+library.

48+

49+\begin{SaveVerbatim}{natlist}

50+

51+data Nat = O | S Nat -- Natural numbers

52+ -- (zero and successor)

53+data List a = Nil | (::) a (List a) -- Polymorphic lists

54+

55+\end{SaveVerbatim}

56+\useverb{natlist}

57+

58+The above declarations are taken from the standard library. Unary natural

59+numbers can be either zero, or

60+the successor of another natural number (\texttt{S k}).

61+Lists can either be empty (\texttt{Nil})

62+or a value added to the front of another list (\texttt{x :: xs}).

63+In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators

64+such as this can be added using a fixity declaration, as follows:

65+

66+\begin{SaveVerbatim}{infixcons}

67+

68+infixr 10 ::

69+

70+\end{SaveVerbatim}

71+\useverb{infixcons}

72+

73+\noindent

74+Functions, data constructors and type constuctors may all be given infix

75+operators as names. They may be used in prefix form if enclosed in brackets,

76+e.g. \tDC{(::)}.

77+

78+\subsection{Functions}

79+

80+Functions are implemented by pattern matching, again using a similar syntax to

81+Haskell. Some natural number arithmetic functions can be

82+defined as follows, again taken from the standard library:

83+

84+\begin{SaveVerbatim}{natfns}

85+

86+-- Unary addition

87+plus : Nat -> Nat -> Nat

88+plus O y = y

89+plus (S k) y = S (plus k y)

90+

91+-- Unary multiplication

92+mult : Nat -> Nat -> Nat

93+mult O y = O

94+mult (S k) y = plus y (mult k y)

95+

96+\end{SaveVerbatim}

97+\useverb{natfns}

98+

99+\noindent

100+The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded

101+for use by \texttt{Nat}, and are implemented

102+using the above functions. Unlike Haskell, there is no restriction on whether

103+types and function names must begin with a capital letter or not. Function

104+names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},

105+\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are

106+all part of the same namespace.

107+

108+\Idris{} has an interactive prompt, at which we can test these functions:

109+

110+\begin{SaveVerbatim}{fntest}

111+

112+Idris> plus (S (S O)) (S (S O))

113+S (S (S (S O))) : Nat

114+Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))

115+S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat

116+

117+\end{SaveVerbatim}

118+\useverb{fntest}

119+

120+\noindent

121+Like arithmetic operations, integer literals are also overloaded using type classes,

122+meaning that we can also test the functions as follows:

123+

124+\begin{SaveVerbatim}{fntest}

125+

126+Idris> plus 2 2

127+S (S (S (S O))) : Nat

128+Idris> mult 3 (plus 2 2)

129+S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat

130+

131+\end{SaveVerbatim}

132+\useverb{fntest}

133+

134+\subsubsection{\texttt{where} clauses}

135+

136+Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,

137+to define a function which reverses a list, we can use an auxiliary function which

138+accumulates the new, reversed list, and which does not need to be visible globally:

139+

140+\begin{SaveVerbatim}{revwhere}

141+

142+reverse : List a -> List a

143+reverse xs = revAcc [] xs where

144+ revAcc : List a -> List a -> List a

145+ revAcc acc [] = acc

146+ revAcc acc (x :: xs) = revAcc (x :: acc) xs

147+

148+\end{SaveVerbatim}

149+\useverb{revwhere}

150+

151+\noindent

152+Indentation is significant --- functions in the \texttt{where} block must be indented

153+further than the outer function.

154+

155+\textbf{Scope:}

156+Any names which are visible in the outer scope are also visible in the \texttt{where}

157+clause (unless they have been redefined, such as \texttt{xs} here).

158+\emph{However}, names which appear in the type are \emph{not} in scope. In particular,

159+in the above example, the \texttt{a} in the top level type and the \texttt{a} in the

160+auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required

161+behaviour, the \texttt{a} can be brought into scope as follows:

162+

163+\begin{SaveVerbatim}{revwhereb}

164+

165+reverse : List a -> List a

166+reverse {a} xs = revAcc [] xs where

167+ revAcc : List a -> List a -> List a

168+ ...

169+

170+\end{SaveVerbatim}

171+\useverb{revwhereb}

172+

173+\subsubsection{Dependent Types}

174+

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

176+conventionally called ``vectors''. In \Idris{}, we declare vectors as follows:

177+

178+\begin{SaveVerbatim}{vect}

179+

180+data Vect : Set -> Nat -> Set where

181+ Nil : Vect a O

182+ (::) : a -> Vect a k -> Vect a (S k)

183+

184+\end{SaveVerbatim}

185+\useverb{vect}

186+

187+\noindent

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

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

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

191+Ambiguous constructor names are resolved by type.

192+

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

194+different from the simple type declarations above. It resembles a Haskell GADT

195+declaration: we explicitly state the type

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

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

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

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

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

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

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

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

204+

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

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

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

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

209+library, appends two \tTC{Vect}s:

210+

211+\begin{SaveVerbatim}{vapp}

212+

213+(++) : Vect A n -> Vect A m -> Vect A (n + m)

214+(++) Nil ys = ys

215+(++) (x :: xs) ys = x :: xs ++ ys

216+

217+\end{SaveVerbatim}

218+\useverb{vapp}

219+

220+\subsubsection{The Finite Sets}

221+

222+Finite sets, as the name suggests, are sets with a finite number of elements.

223+They are declared as follows in the library:

224+

225+\begin{SaveVerbatim}{findecl}

226+

227+data Fin : Nat -> Set where

228+ fO : Fin (S k)

229+ fS : Fin k -> Fin (S k)

230+

231+\end{SaveVerbatim}

232+\useverb{findecl}

233+

234+\noindent

235+This declares

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

237+\texttt{fS n} as the

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

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

240+represents the number of elements in the set.

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

242+element of an empty set.

243+

244+A useful application of the \tTC{Fin} family is to represent bounded

245+natural numbers. Since the first \tTC{n} natural numbers form a finite

246+set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural

247+numbers bounded by \tTC{n}.

248+

249+For example, the following function which looks up an element in a \tTC{Vect},

250+by a bounded index given as a \tTC{Fin n}, is defined in the library:

251+

252+\begin{SaveVerbatim}{vindex}

253+

254+index : Fin n -> Vect a n -> a

255+index fO (x :: xs) = x

256+index (fS k) (x :: xs) = index k xs

257+

258+\end{SaveVerbatim}

259+\useverb{vindex}

260+

261+\noindent

262+This function looks up a value at a given location in a vector. The location is

263+bounded by the length of the vector (\texttt{n} in each case), so there is no

264+need for a run-time bounds check. The type checker guarantees that the location

265+is no larger than the length of the vector.

266+

267+Note also that there is no case for \texttt{Nil} here. It would be impossible

268+to add such a case ---

269+since there is no element of \texttt{Fin O}, and the location is a

270+\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to

271+look up an element in an empty vector would give a compile time type error,

272+since it would force \texttt{n} to be \tDC{O}.

273+

274+\subsubsection{Implicit Arguments}

275+

276+Let us take a closer look at the type of \texttt{index}:

277+

278+\begin{SaveVerbatim}{vindexty}

279+

280+index : Fin n -> Vect a n -> a

281+

282+\end{SaveVerbatim}

283+\useverb{vindexty}

284+

285+\noindent

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

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

288+\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}

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

290+

291+\begin{SaveVerbatim}{vindeximpty}

292+

293+index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a

294+

295+\end{SaveVerbatim}

296+\useverb{vindeximpty}

297+

298+\noindent

299+Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in

300+applications of \texttt{index}; their values can be inferred from the types of

301+the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter

302+or index in a type declaration, but which is otherwise free, will be automatically

303+bound as an implicit argument. Indeed, binding arguments in this way is the essence

304+of dependent types.

305+Implicit arguments can still be given explicitly in applications, using the syntax

306+\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:

307+

308+\begin{SaveVerbatim}{vindexexp}

309+

310+index {a=Int} {n=2} fO (2 :: 3 :: Nil)

311+

312+\end{SaveVerbatim}

313+\useverb{vindexexp}

314+

315+\noindent

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

317+we could have declared the type of \texttt{index} as:

318+

319+\begin{SaveVerbatim}{vindexn}

320+

321+index : (i:Fin n) -> (xs:Vect a n) -> a

322+

323+\end{SaveVerbatim}

324+\useverb{vindexn}

325+

326+\noindent

327+This can be useful for improving the readability of type signatures, particularly

328+where the name suggests the argument's purpose.

329+

330+\subsection{Type Classes}

331+

332+\Idris{} supports overloading in two ways. Firstly, as we have already seen with

333+this constructors of \texttt{List} and \texttt{Vect}, names

334+can be overloaded in an ad-hoc manner and resolved according to the context in which

335+they are used. This is mostly for convenience, to eliminate the need to decorate

336+constructor names in similarly structured data types, and eliminate explicit qualification

337+of ambiguous names where only one is well-typed.

338+

339+Secondly, \Idris{} implements \remph{type classes}. This allows a more principled approach

340+to overloading --- a type class gives a collection of overloaded operations which describe

341+the interface for \remph{instances} of that class.

342+

343+A simple example

344+is the \texttt{Show} type class, which is defined in the library and

345+provides an interface for converting values to

346+\texttt{String}s:

347+

348+\begin{SaveVerbatim}{showclass}

349+

350+class Show a where

351+ show : a -> String

352+

353+\end{SaveVerbatim}

354+\useverb{showclass}

355+

356+\noindent

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

358+\texttt{Show} class):

359+

360+\begin{SaveVerbatim}{showty}

361+

362+show : Show a => a -> String

363+

364+\end{SaveVerbatim}

365+\useverb{showty}

366+

367+An instance of a class

368+is defined with an \texttt{instance} declaration, which provides implementations of

369+the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}

370+could be defined as:

371+

372+\begin{SaveVerbatim}{shownat}

373+

374+instance Show Nat where

375+ show O = "O"

376+ show (S k) = "s" ++ show k

377+

378+Idris> show (S (S (S O)))

379+"sssO" : String

380+

381+\end{SaveVerbatim}

382+\useverb{shownat}

383+

384+\noindent

385+Only one instance of a class can be given for a type --- instances may not overlap.

386+Instance declarations can themselves have constraints. For example, to define a

387+\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}

388+instance for the element type, because we are going to use it to convert each element

389+to a \texttt{String}:

390+

391+\begin{SaveVerbatim}{showvec}

392+

393+instance Show a => Show (Vect a n) where

394+ show xs = "[" ++ show' xs ++ "]" where

395+ show' : Vect a n' -> String

396+ show' Nil = ""

397+ show' (x :: Nil) = show x

398+ show' (x :: xs) = show x ++ ", " ++ show' xs

399+

400+\end{SaveVerbatim}

401+\useverb{showvec}

402+

403+\noindent

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

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

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

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

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

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

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

411+

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

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

414+\texttt{Eq} class:

415+

416+\begin{SaveVerbatim}{eqdefault}

417+

418+class Eq a where

419+ (==) : a -> a -> Bool

420+ (/=) : a -> a -> Bool

421+

422+ x /= y = not (x == y)

423+ y == y = not (x /= y)

424+

425+\end{SaveVerbatim}

426+\useverb{eqdefault}

427+

428+\noindent

429+Classes can also be extended. A logical next step from an equality relation \texttt{Eq}

430+is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class

431+which inherits methods from \texttt{Eq} as well as defining some of its own:

432+

433+\begin{SaveVerbatim}{ord}

434+

435+data Ordering = LT | EQ | GT

436+

437+\end{SaveVerbatim}

438+\useverb{ord}

439+

440+\begin{SaveVerbatim}{eqord}

441+

442+class Eq a => Ord a where

443+ compare : a -> a -> Ordering

444+

445+ (<) : a -> a -> Bool

446+ (>) : a -> a -> Bool

447+ (<=) : a -> a -> Bool

448+ (>=) : a -> a -> Bool

449+ max : a -> a -> a

450+ min : a -> a -> a

451+

452+\end{SaveVerbatim}

453+\useverb{eqord}

454+

455+\subsection{Matching on intermediate values}

456+

457+\subsubsection{\texttt{let} bindings}

458+

459+Intermediate values can be calculated using \texttt{let} bindings:

460+

461+\begin{SaveVerbatim}{letb}

462+

463+mirror : List a -> List a

464+mirror xs = let xs' = rev xs in

465+ app xs xs'

466+

467+\end{SaveVerbatim}

468+\useverb{letb}

469+

470+\noindent

471+We can also do simple pattern matching in \texttt{let} bindings. For example, we can extract

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

473+

474+\begin{SaveVerbatim}{letp}

475+

476+data Person = MkPerson String Int

477+

478+showPerson : Person -> String

479+showPerson p = let MkPerson name age = p in

480+ name ++ " is " ++ show age ++ " years old"

481+

482+\end{SaveVerbatim}

483+\useverb{letp}

484+\subsubsection{\texttt{case} expressions}

485+

486+Another way of inspecting intermediate values of \emph{simple} types

487+is to use a \texttt{case} expression.

488+The following function, for example, splits a string into two at a given character:

489+

490+\begin{SaveVerbatim}{split}

491+

492+splitAt : Char -> String -> (String, String)

493+splitAt c x = case break (== c) x of

494+ (x, y) => (x, strTail y)

495+

496+\end{SaveVerbatim}

497+\useverb{split}

498+

499+\noindent

500+\texttt{break} is a library function which breaks a string into a pair of strings

501+at the point where the given function returns true. We then deconstruct the

502+pair it returns, and remove the first character of the second string.

503+

504+A \texttt{case} expression can match several cases, for example, to inspect an

505+intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which

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

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

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

509+

510+\begin{SaveVerbatim}{listlookup}

511+

512+lookup_default : Nat -> List a -> a -> a

513+lookup_default i xs def = case list_lookup i xs of

514+ Nothing => def

515+ Just x => x

516+

517+\end{SaveVerbatim}

518+\useverb{listlookup}

519+

520+The \texttt{case} construct is intended for simple analysis

521+of intermediate expressions to avoid the need to write auxiliary functions, and is

522+also used internally to implement pattern matching \texttt{let} and lambda bindings.

523+It will \emph{only} work if:

524+

525+\begin{itemize}

526+\item Each branch \emph{matches} a value of the same type, and \emph{returns} a

527+value of the same type.

528+\item The type of the result is ``known''. i.e. the type of the expression can be

529+determined \emph{without} type checking the \texttt{case}-expression itself.

530+\end{itemize}

531+

532+\subsubsection{The \texttt{with} rule}

533+

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

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

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

537+determined by whether the vector was empty or not:

538+

539+\begin{SaveVerbatim}{appdep}

540+

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

542+(++) {n=O} [] [] = []

543+(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

544+

545+\end{SaveVerbatim}

546+\useverb{appdep}

547+

548+\noindent

549+If \texttt{n} was a successor in the \texttt{[]} case, or zero in the

550+\texttt{::} case, the definition

551+would not be well typed.

552+

553+Often, we need to match on the result of an intermediate computation

554+with a dependent type.

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

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

557+which takes account of the

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

559+we know about the forms of other values.

560+

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

562+If it is even it will

563+be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s

564+plus one:

565+

566+\begin{SaveVerbatim}{parity}

567+

568+data Parity : Nat -> Set where

569+ even : Parity (n + n)

570+ odd : Parity (S (n + n))

571+

572+\end{SaveVerbatim}

573+\useverb{parity}

574+

575+\noindent

576+We say \texttt{Parity} is a \emph{view} of \texttt{Nat}.

577+It has a \emph{covering function} which tests whether

578+it is even or odd and constructs the predicate accordingly.

579+

580+\begin{SaveVerbatim}{parityty}

581+

582+parity : (n:Nat) -> Parity n

583+

584+\end{SaveVerbatim}

585+\useverb{parityty}

586+

587+\noindent

588+Using this, we can write a function which converts a natural number to a list

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

590+rule:

591+

592+\begin{SaveVerbatim}{natToBin}

593+

594+natToBin : Nat -> List Bool

595+natToBin O = Nil

596+natToBin k with (parity k)

597+ natToBin (j + j) | even = False :: natToBin j

598+ natToBin (S (j + j)) | odd = True :: natToBin j

599+

600+\end{SaveVerbatim}

601+\useverb{natToBin}

602+

603+\noindent

604+The value of the result of \texttt{parity k} affects the form of \texttt{k},

605+because the result

606+of \texttt{parity k} depends on \texttt{k}.

607+So, as well as the patterns for the result of the

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

609+\texttt{$\mid$}, we also write how

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

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

612+this is allowed

613+because another argument has determined the form of these patterns.

614+

615+

impl-paper/impldtp.tex+2

@@ -29,6 +29,8 @@

2929

3030\newcommand{\Ivor}{\textsc{Ivor}}

3131\newcommand{\Idris}{\textsc{Idris}}

32+\newcommand{\TT}{\textsf{TT}}

33+\newcommand{\TTdev}{\textsf{TT$_{dev}$}}

3234\newcommand{\Funl}{\textsc{Funl}}

3335\newcommand{\Agda}{\textsc{Agda}}

3436\newcommand{\LamPi}{$\lambda_\Pi$}

impl-paper/intro.tex+11

@@ -22,3 +22,14 @@ about making the language itself practical.

2222\end{itemize}

2323

2424Also note --- to be an expert user of a language requires good understanding of the internals.

25+

26+\subsection{Typographical conventions}

27+

28+We'll have \Idris{} programs, \TT{} programs and meta-operations (standing for

29+Haskell programs which operate on \Idris{} or \TT{} programs). Suggestion:

30+\Idris{} always in \texttt{texttt}, with \texttt{e$_i$} standing for

31+non-terminal expressions. \TT{} in mathematical notation and meta-operation

32+names either in \textsc{TextSC} or as $\interp{\cdot}$.

33+

34+Also we will show some interactions at the \texttt{Idris>} prompt, which can be identified

35+by the prompt.

impl-paper/library.bib+236−184

@@ -1,135 +1,17 @@

11Automatically generated by Mendeley 1.3.1

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

4−@inproceedings{Levitation2010,

5−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

6−booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},

7−doi = {10.1145/1932681.1863547},

8−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

9−isbn = {978-1-60558-794-3},

10−issn = {03621340},

11−keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

12−mendeley-tags = {Dependent Types},

13−month = sep,

14−number = {9},

15−pages = {3},

16−title = {{The gentle art of levitation}},

17−url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},

18−volume = {45},

19−year = {2010}

20−}

21−@article{Brady2006a,

22−author = {Brady, E and Hammond, K},

23−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

24−journal = {\ldots of the 5th international conference on \ldots},

25−keywords = {Dependent Types},

26−mendeley-tags = {Dependent Types},

27−title = {{A verified staged interpreter is a verified compiler}},

28−url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},

29−year = {2006}

30−}

31−@article{Chapman2005epigram,

32−author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},

33−file = {:Users/edwin/Documents/Papers/Chapman/2005 Chapman-Epigram reloaded a standalone typechecker.pdf:pdf},

34−journal = {Trends in Functional Programming},

35−publisher = {Intellect Books},

36−title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},

37−url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},

38−year = {2005}

39−}

40−@article{McBride2007,

41−author = {McBride, Conor and Paterson, Ross},

42−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

43−journal = {Journal of functional programming},

44−title = {{Applicative programming with effects}},

45−url = {http://journals.cambridge.org/abstract_S0956796807006326},

46−year = {2007}

47−}

48−@misc{dagand2011transporting,

49−author = {Dagand, Pierre-Evariste and McBride, Conor},

50−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

51−title = {{Transporting Functions across Ornaments}},

52−url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},

53−year = {2011}

54−}

55−@inproceedings{Brady2003,

56−author = {Brady, Edwin and McBride, Conor and McKinna, James},

57−booktitle = {Types for Proofs and Programs},

58−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

59−keywords = {Dependent Types},

60−mendeley-tags = {Dependent Types},

61−title = {{Inductive families need not store their indices}},

62−url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},

63−year = {2003}

64−}

65−@inproceedings{norell2009dependently,

66−author = {Norell, Ulf},

67−booktitle = {Advanced Functional Programming},

68−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

69−keywords = {Dependent Types},

70−mendeley-tags = {Dependent Types},

71−pages = {230--266},

72−publisher = {Springer},

73−title = {{Dependently typed programming in Agda}},

74−url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

75−year = {2009}

76−}

77−@article{mcbride2010ornamental,

78−author = {McBride, Conor},

79−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},

80−journal = {Journal of Functional Programming},

81−title = {{Ornamental algebras, algebraic ornaments}},

82−url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},

83−year = {2010}

84−}

85−@misc{Brady2012c,

86−author = {Brooks, Fred},

87−doi = {10.1093/epirev/mxr031},

88−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},

89−isbn = {9780321702081},

90−issn = {1478-6729},

91−number = {1},

92−pages = {NP},

93−pmid = {22215642},

94−title = {{The Design of Design Chapter 5}},

95−volume = {34}

96−}

97−@inproceedings{brady2011epic,

4+@misc{idristutorial,

985author = {Brady, Edwin},

99−booktitle = {Trends in Functional Programming ({TFP}’11)},

100−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2011 - Epic—A Library for Generating Compilers.pdf:pdf},

101−title = {{Epic --- A Library for Generating Compilers}},

102−url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},

103−year = {2011}

104−}

105−@inproceedings{chlipala2010ur,

106−author = {Chlipala, Adam},

107−booktitle = {ACM SIGPLAN Notices},

108−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

109−number = {6},

110−pages = {122--133},

111−publisher = {ACM},

112−title = {{Ur: statically-typed metaprogramming with type-level record computation}},

113−url = {http://dl.acm.org/citation.cfm?id=1806612},

114−volume = {45},

115−year = {2010}

116−}

117−@article{loh2010tutorial,

118−author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},

119−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},

120−journal = {Fundamenta Informaticae},

121−number = {2},

122−pages = {177--207},

123−publisher = {IOS Press},

124−title = {{A tutorial implementation of a dependently typed lambda calculus}},

125−url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},

126−volume = {102},

127−year = {2010}

6+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},

7+title = {{Programming in Idris : a tutorial}},

8+url = {http://idris-lang.org/tutorial},

9+year = {2012}

12810}

12911@inproceedings{Brady2010,

13012author = {Brady, Edwin and Hammond, Kevin},

13113booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},

132−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},

14+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},

13315isbn = {9781605587943},

13416keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},

13517mendeley-tags = {Dependent Types},

@@ -142,7 +24,7 @@ year = {2010}

14224@misc{The2012c,

14325author = {Robbins, A and Hannah, E and Lamb, L},

14426doi = {10.1093/epirev/mxr031},

145−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

27+file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

14628isbn = {9780596529833},

14729issn = {1478-6729},

14830pmid = {22215642},

@@ -151,7 +33,7 @@ title = {{Learning the vi and Vim Editors}}

15133@article{Haskell2012a,

15234author = {Biancuzzi, F and Warden, S},

15335doi = {10.1093/epirev/mxr031},

154−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

36+file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

15537isbn = {9780596801670},

15638issn = {1478-6729},

15739pmid = {22215642},

@@ -160,7 +42,7 @@ title = {{Masterminds of Programming Chapter 8}}

16042@inproceedings{Brady2006b,

16143author = {Brady, Edwin},

16244booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},

163−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

45+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

16446isbn = {978-3-540-74129-9},

16547month = sep,

16648pages = {145----162},

@@ -173,7 +55,7 @@ abstract = {This paper suggests that input and output are basic primitives of pr

17355author = {Hoare, C A R},

17456doi = {10.1016/0167-6423(87)90028-1},

17557editor = {McKeag, R M and Macnaghten, A M},

176−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

58+file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

17759isbn = {0131532715},

17860issn = {01676423},

17961journal = {Communications of the ACM},

@@ -192,7 +74,7 @@ address = {New York, New York, USA},

19274author = {Sheard, Tim},

19375booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},

19476doi = {10.1145/1088348.1088356},

195−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

77+file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

19678isbn = {159593071X},

19779keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},

19880month = sep,

@@ -206,7 +88,7 @@ year = {2005}

20688author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},

20789booktitle = {International Conference on Functional Programming},

20890doi = {10.1145/583852.581499},

209−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},

91+file = {:Users/edwin/Documents/Mendeley Desktop/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},

21092isbn = {1-58113-487-8},

21193issn = {03621340},

21294keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},

@@ -220,7 +102,7 @@ year = {2002}

220102}

221103@inproceedings{gibbons2011modularising,

222104author = {Gibbons, J. and Ko, H.S. and Others},

223−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

105+file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

224106title = {{Modularising inductive families}},

225107url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},

226108year = {2011}

@@ -230,7 +112,7 @@ abstract = {We describe an axiomatic extension to the Coq proof assistant, that

230112author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},

231113booktitle = {International Conference on Functional Programming},

232114doi = {10.1145/1411204.1411237},

233−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

115+file = {:Users/edwin/Documents/Mendeley Desktop/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

234116isbn = {9781595939197},

235117issn = {15232867},

236118keywords = {Dependent Types},

@@ -256,7 +138,7 @@ year = {2000}

256138@inproceedings{lempsink2009type,

257139author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},

258140booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},

259−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},

141+file = {:Users/edwin/Documents/Mendeley Desktop/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},

260142pages = {61--72},

261143publisher = {ACM},

262144title = {{Type-safe diff for families of datatypes}},

@@ -309,7 +191,7 @@ abstract = {In these lecture notes we give an introduction to functional program

309191author = {Bove, Ana and Dybjer, Peter},

310192booktitle = {Notes},

311193doi = {10.1007/978-3-642-03153-3_2},

312−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

194+file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

313195number = {February},

314196pages = {57--99},

315197publisher = {Springer},

@@ -321,7 +203,7 @@ year = {2008}

321203@inproceedings{madhavapeddy2010turning,

322204author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},

323205booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},

324−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

206+file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

325207publisher = {USENIX Association},

326208title = {{Turning down the LAMP: software specialisation for the cloud}},

327209url = {http://dl.acm.org/citation.cfm?id=1863114},

@@ -329,7 +211,7 @@ year = {2010}

329211}

330212@article{gordon2003authenticity,

331213author = {Gordon, A.D. and Jeffrey, A.},

332−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

214+file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

333215journal = {Journal of computer security},

334216number = {4},

335217pages = {451--520},

@@ -351,7 +233,7 @@ year = {2011}

351233@inproceedings{l,

352234author = {L\"{a}mmel, R. and Jones, S.P.},

353235booktitle = {ACM SIGPLAN Notices},

354−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},

236+file = {:Users/edwin/Documents/Mendeley Desktop/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},

355237number = {3},

356238pages = {26--37},

357239publisher = {ACM},

@@ -360,6 +242,33 @@ url = {http://dl.acm.org/citation.cfm?id=640136.604179},

360242volume = {38},

361243year = {2003}

362244}

245+@inproceedings{Levitation2010,

246+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

247+booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},

248+doi = {10.1145/1932681.1863547},

249+file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

250+isbn = {978-1-60558-794-3},

251+issn = {03621340},

252+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

253+mendeley-tags = {Dependent Types},

254+month = sep,

255+number = {9},

256+pages = {3},

257+title = {{The gentle art of levitation}},

258+url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},

259+volume = {45},

260+year = {2010}

261+}

262+@article{Brady2006a,

263+author = {Brady, E and Hammond, K},

264+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

265+journal = {\ldots of the 5th international conference on \ldots},

266+keywords = {Dependent Types},

267+mendeley-tags = {Dependent Types},

268+title = {{A verified staged interpreter is a verified compiler}},

269+url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},

270+year = {2006}

271+}

363272@inproceedings{bhargavan2010modular,

364273author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},

365274booktitle = {ACM Sigplan Notices},

@@ -374,7 +283,7 @@ year = {2010}

374283@inproceedings{stump2010resource,

375284author = {Stump, A. and Austin, E.},

376285booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},

377−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

286+file = {:Users/edwin/Documents/Mendeley Desktop/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

378287pages = {27--38},

379288publisher = {ACM},

380289title = {{Resource typing in Guru}},

@@ -383,7 +292,7 @@ year = {2010}

383292}

384293@phdthesis{norell2007thesis,

385294author = {Norell, Ulf},

386−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

295+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

387296keywords = {Dependent Types},

388297mendeley-tags = {Dependent Types},

389298publisher = {Citeseer},

@@ -392,6 +301,25 @@ title = {{Towards a practical programming language based on dependent type theor

392301url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},

393302year = {2007}

394303}

304+@article{Swierstra2011,

305+author = {Swierstra, W},

306+file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},

307+journal = {Journal of Functional Programming},

308+number = {6},

309+pages = {575----583},

310+title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},

311+url = {http://journals.cambridge.org/abstract_S0956796811000207},

312+volume = {21},

313+year = {2011}

314+}

315+@inproceedings{Sculthorpe2009,

316+author = {Sculthorpe, Neil and Nilsson, Henrik},

317+booktitle = {International Conference on Functional Programming ({ICFP} '09)},

318+file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf},

319+title = {{Safe functional reactive programming through dependent types}},

320+url = {http://dl.acm.org/citation.cfm?id=1596558},

321+year = {2009}

322+}

395323@article{Epstein2011,

396324author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},

397325institution = {Microsoft Research},

@@ -420,13 +348,22 @@ url = {http://dl.acm.org/citation.cfm?id=259019},

420348volume = {32},

421349year = {1997}

422350}

351+@article{Chapman2005epigram,

352+author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},

353+file = {:Users/edwin/Documents/Mendeley Desktop/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},

354+journal = {Trends in Functional Programming},

355+publisher = {Intellect Books},

356+title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},

357+url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},

358+year = {2005}

359+}

423360@article{Hughes1989,

424361abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},

425362author = {Hughes, J},

426363chapter = {2},

427364doi = {10.1093/comjnl/32.2.98},

428365editor = {Turner, David A},

429−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

366+file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

430367institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

431368isbn = {0201172364},

432369issn = {00104620},

@@ -441,7 +378,7 @@ year = {1989}

441378}

442379@article{marlow2006making,

443380author = {Marlow, S. and {Peyton Jones}, S.},

444−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},

381+file = {:Users/edwin/Documents/Mendeley Desktop/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},

445382journal = {Journal of Functional Programming},

446383number = {4-5},

447384pages = {415--449},

@@ -469,7 +406,7 @@ year = {2007}

469406}

470407@phdthesis{McBride1999,

471408author = {McBride, Conor},

472−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

409+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

473410keywords = {Dependent Types},

474411mendeley-tags = {Dependent Types},

475412school = {University of Edinburgh},

@@ -480,7 +417,7 @@ year = {1999}

480417@inproceedings{oury2008power,

481418author = {Oury, N. and Swierstra, W.},

482419booktitle = {International Conference on Functional Programming},

483−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

420+file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

484421keywords = {Dependent Types},

485422mendeley-tags = {Dependent Types},

486423number = {9},

@@ -500,17 +437,25 @@ title = {{Unembedding domain-specific languages}},

500437url = {http://dl.acm.org/citation.cfm?id=1596644},

501438year = {2009}

502439}

440+@article{McBride2007,

441+author = {McBride, Conor and Paterson, Ross},

442+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

443+journal = {Journal of functional programming},

444+title = {{Applicative programming with effects}},

445+url = {http://journals.cambridge.org/abstract_S0956796807006326},

446+year = {2007}

447+}

503448@misc{Abel1998,

504449author = {Abel, Andreas},

505450booktitle = {Language},

506−file = {:Users/edwin/Downloads/10.1.1.44.3494.pdf:pdf},

451+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

507452title = {{foetus - Termination Checker for Simple Functional Programs}},

508453year = {1998}

509454}

510455@inproceedings{Brady2005a,

511456author = {Brady, E and Hammond, K},

512457booktitle = {Implementation and Application of Functional \ldots},

513−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

458+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

514459keywords = {Dependent Types},

515460mendeley-tags = {Dependent Types},

516461title = {{A dependently typed framework for static analysis of program execution costs}},

@@ -520,15 +465,31 @@ year = {2005}

520465@misc{altenkirch2005dependent,

521466author = {Altenkirch, T. and McBride, C. and McKinna, J.},

522467booktitle = {Manuscript, available online},

523−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

468+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

524469title = {{Why dependent types matter}},

525470url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},

526471year = {2005}

527472}

473+@misc{dagand2011transporting,

474+author = {Dagand, Pierre-Evariste and McBride, Conor},

475+file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

476+title = {{Transporting Functions across Ornaments}},

477+url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},

478+year = {2011}

479+}

480+@inproceedings{bradyresource,

481+author = {Brady, Edwin and Hammond, Kevin},

482+booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},

483+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},

484+pages = {242----257},

485+title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},

486+url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},

487+year = {2012}

488+}

528489@misc{Resolution2012a,

529490author = {Fall, Kevin R and Stevens, W. Richard},

530491doi = {10.1093/epirev/mxr031},

531−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

492+file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

532493issn = {1478-6729},

533494pmid = {22215642},

534495title = {{TCP/IP Illustrated Volume 1 Chapter 11}}

@@ -536,7 +497,7 @@ title = {{TCP/IP Illustrated Volume 1 Chapter 11}}

536497@inproceedings{madhavapeddy2007melange,

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

538499booktitle = {ACM SIGOPS Operating Systems Review},

539−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},

500+file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},

540501number = {3},

541502pages = {101--114},

542503publisher = {ACM},

@@ -548,15 +509,24 @@ year = {2007}

548509@misc{The2012b,

549510author = {Brooks, Fred},

550511doi = {10.1093/epirev/mxr031},

551−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},

512+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},

552513isbn = {9780321702081},

553514issn = {1478-6729},

554515pmid = {22215642},

555516title = {{The Design of Design Chapter 1}}

556517}

518+@misc{Abadi1997,

519+author = {Abadi, Martin and Gordon, Andrew D},

520+booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},

521+file = {:Users/edwin/Documents/Mendeley Desktop/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},

522+pages = {36 -- 47},

523+title = {{A calculus for cryptographic protocols: The spi calculus}},

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

525+year = {1997}

526+}

557527@phdthesis{Brady2005,

558528author = {Brady, Edwin},

559−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming \ldots.pdf:pdf},

529+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},

560530keywords = {Dependent Types},

561531mendeley-tags = {Dependent Types},

562532school = {University of Durham},

@@ -567,7 +537,7 @@ year = {2005}

567537@inproceedings{swierstra2007beauty,

568538author = {Swierstra, W. and Altenkirch, T.},

569539booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},

570−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

540+file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

571541pages = {25--36},

572542publisher = {ACM},

573543title = {{Beauty in the beast}},

@@ -578,7 +548,7 @@ year = {2007}

578548abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.},

579549author = {McBride, Conor and McKinna, James},

580550doi = {10.1017/S0956796803004829},

581−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

551+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

582552issn = {09567968},

583553journal = {Journal of Functional Programming},

584554keywords = {Dependent Types},

@@ -596,7 +566,7 @@ abstract = {Cayenne is a Haskell-like language. The main difference between Hask

596566author = {Augustsson, Lennart},

597567booktitle = {International Conference on Functional Programming},

598568doi = {10.1097/MEG.0b013e328342f213},

599−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

569+file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

600570issn = {14735687},

601571keywords = {Depe,Dependent Types},

602572mendeley-tags = {Depe,Dependent Types},

@@ -611,7 +581,7 @@ year = {1998}

611581}

612582@article{fisher2006next,

613583author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},

614−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

584+file = {:Users/edwin/Documents/Mendeley Desktop/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

615585journal = {Journal of the ACM},

616586number = {2},

617587pages = {1--51},

@@ -626,7 +596,7 @@ abstract = {From the type of a polymorphic function we can derive a theorem that

626596author = {Wadler, Philip},

627597booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},

628598doi = {10.1145/99370.99404},

629−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Wadler - 1989 - Theorems for free!.pdf:pdf},

599+file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},

630600isbn = {0897913280},

631601number = {June},

632602pages = {347--359},

@@ -639,7 +609,7 @@ year = {1989}

639609@misc{Protocols2012a,

640610author = {Anderson, Ross},

641611doi = {10.1093/epirev/mxr031},

642−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},

612+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},

643613isbn = {9780470068526},

644614issn = {1478-6729},

645615pmid = {22215642},

@@ -648,7 +618,7 @@ title = {{Security Engineering Chapter 3}}

648618@inproceedings{barras2008implicit,

649619author = {Barras, B. and Bernardo, B.},

650620booktitle = {Foundations of Software Science and Computational Structures},

651−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},

621+file = {:Users/edwin/Documents/Mendeley Desktop/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},

652622pages = {365--379},

653623publisher = {Springer},

654624title = {{The implicit calculus of constructions as a programming language with dependent types}},

@@ -657,7 +627,7 @@ year = {2008}

657627}

658628@article{landin1966next,

659629author = {Landin, P.J.},

660−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Landin - 1966 - The next 700 programming languages.pdf:pdf},

630+file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},

661631journal = {Communications of the ACM},

662632number = {3},

663633pages = {157--166},

@@ -670,16 +640,26 @@ year = {1966}

670640@misc{Brady2012b,

671641author = {Brooks, Fred},

672642doi = {10.1093/epirev/mxr031},

673−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},

643+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},

674644isbn = {9780321702081},

675645issn = {1478-6729},

676646pmid = {22215642},

677647title = {{The Design of Design Chapter 2}}

678648}

649+@inproceedings{Brady2003,

650+author = {Brady, Edwin and McBride, Conor and McKinna, James},

651+booktitle = {Types for Proofs and Programs},

652+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

653+keywords = {Dependent Types},

654+mendeley-tags = {Dependent Types},

655+title = {{Inductive families need not store their indices}},

656+url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},

657+year = {2003}

658+}

679659@misc{Nodes2012a,

680660author = {Brooks, Fred},

681661doi = {10.1093/epirev/mxr031},

682−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},

662+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},

683663isbn = {9780321702081},

684664issn = {1478-6729},

685665pmid = {22215642},

@@ -688,7 +668,7 @@ title = {{The Design of Design Chapter 3}}

688668@article{Abel2010,

689669abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},

690670author = {Abel, Andreas},

691−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

671+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

692672journal = {EPTCS},

693673pages = {1--15},

694674title = {{MiniAgda: Integrating Sized and Dependent Types}},

@@ -698,7 +678,7 @@ year = {2010}

698678}

699679@book{Bird2010,

700680author = {Bird, Richard},

701−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

681+file = {:Users/edwin/Documents/Mendeley Desktop/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

702682isbn = {9780521513388},

703683title = {{Pearls of Functional Algorithm Design}},

704684year = {2010}

@@ -706,13 +686,25 @@ year = {2010}

706686@inproceedings{czarnecki2004dsl,

707687author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},

708688booktitle = {Domain-Specific Program Generation},

709−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},

689+file = {:Users/edwin/Documents/Mendeley Desktop/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},

710690pages = {51--72},

711691publisher = {Springer},

712692title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},

713693url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},

714694year = {2004}

715695}

696+@inproceedings{norell2009dependently,

697+author = {Norell, Ulf},

698+booktitle = {Advanced Functional Programming},

699+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

700+keywords = {Dependent Types},

701+mendeley-tags = {Dependent Types},

702+pages = {230--266},

703+publisher = {Springer},

704+title = {{Dependently typed programming in Agda}},

705+url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

706+year = {2009}

707+}

716708@article{danielsson2011parsing,

717709author = {Danielsson, N. and Norell, U.},

718710journal = {Implementation and Application of Functional Languages},

@@ -738,7 +730,7 @@ year = {2003}

738730@article{Altenkirch2010a,

739731abstract = {We begin by revisiting the idea of using a universe of types to write generic programs in a dependently typed setting by constructing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Positive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach presented here we are able to represent all of Epigrams datatypes within Epigram including the universe of datatypes itself.},

740732author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},

741−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

733+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

742734journal = {Citeseer},

743735publisher = {Citeseer},

744736title = {{Generic Programming with Dependent Types}},

@@ -747,14 +739,14 @@ year = {2010}

747739}

748740@phdthesis{Okasaki1996,

749741author = {Okasaki, Chris},

750−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

742+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

751743school = {Carnegie Mellon University},

752744title = {{Purely Functional Data Structures}},

753745year = {1996}

754746}

755747@misc{altenkirch2008nσ,

756748author = {Altenkirch, T. and Oury, N.},

757−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

749+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

758750title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},

759751url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},

760752year = {2008}

@@ -764,7 +756,7 @@ address = {New York, New York, USA},

764756author = {Brady, Edwin},

765757booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},

766758doi = {10.1145/1929529.1929536},

767−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

759+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

768760isbn = {9781450304870},

769761keywords = {Dependent Types,data description,dependent types},

770762mendeley-tags = {Dependent Types},

@@ -776,16 +768,24 @@ year = {2011}

776768}

777769@article{Steiner1988,

778770author = {Steiner, JG},

779−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

771+file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

780772journal = {Proc. Winter USENIX Conference},

781773title = {{Kerberos: An authentication service for open network systems}},

782774url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},

783775year = {1988}

784776}

777+@inproceedings{Fournet2011,

778+author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},

779+booktitle = {Foundations of security analysis and design {VI}},

780+file = {:Users/edwin/Documents/Mendeley Desktop/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},

781+title = {{Cryptographic verification by typing for a sample protocol implementation}},

782+url = {http://www.springerlink.com/index/V168041M46658R73.pdf},

783+year = {2010}

784+}

785785@inproceedings{augustsson2008paradise,

786786author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},

787787booktitle = {International Conference on Functional Programming},

788−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

788+file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

789789number = {9},

790790pages = {225--228},

791791publisher = {ACM},

@@ -796,13 +796,13 @@ year = {2008}

796796}

797797@misc{Bloat,

798798author = {Brooks, Fred},

799−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},

799+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},

800800isbn = {9780321702081},

801801title = {{The Design of Design Chapter 4}}

802802}

803803@article{burrows1990,

804804author = {Burrows, Michael and Abadi, Martin and Needham, Roger},

805−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

805+file = {:Users/edwin/Documents/Mendeley Desktop/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

806806journal = {ACM Transactions on Computer Systems},

807807pages = {18----36},

808808title = {{A logic of authentication}},

@@ -815,7 +815,7 @@ abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your pe

815815address = {London},

816816author = {{The Mendeley Support Team}},

817817booktitle = {Mendeley Desktop},

818−file = {:Applications/Mendeley Desktop.app/Contents/Resources/FAQ.pdf:pdf},

818+file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

819819keywords = {Mendeley,how-to,user manual},

820820pages = {1--16},

821821publisher = {Mendeley Ltd.},

@@ -823,10 +823,18 @@ title = {{Getting Started with Mendeley}},

823823url = {http://www.mendeley.com},

824824year = {2011}

825825}

826+@article{mcbride2010ornamental,

827+author = {McBride, Conor},

828+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},

829+journal = {Journal of Functional Programming},

830+title = {{Ornamental algebras, algebraic ornaments}},

831+url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},

832+year = {2010}

833+}

826834@misc{Interface2012a,

827835author = {Kreibich, Jay A.},

828836doi = {10.1093/epirev/mxr031},

829−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

837+file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

830838isbn = {9781449394592},

831839issn = {1478-6729},

832840pmid = {22215642},

@@ -834,7 +842,7 @@ title = {{Using SQLite Chapter 7}}

834842}

835843@misc{pollack1997believe,

836844author = {Pollack, R.},

837−file = {:Users/edwin/Documents/Papers/Pollack/1997 Pollack-How to Believe a Machine-Checked.pdf:pdf},

845+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},

838846title = {{How to believe a machine-checked proof}},

839847url = {http://books.google.co.uk/books?hl=en&lr=&id=pLnKggT_In4C&oi=fnd&pg=PA205&dq=how+to+believe+a+machine+checked+proof&ots=c2OI8krqqA&sig=EF3QonGFVdOpYdKO1KmW6ljCkjY},

840848year = {1997}

@@ -842,16 +850,28 @@ year = {1997}

842850@inproceedings{ko2011modularising,

843851author = {Ko, H.S. and Gibbons, J.},

844852booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},

845−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

853+file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

846854pages = {13--24},

847855publisher = {ACM},

848856title = {{Modularising inductive families}},

849857url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},

850858year = {2011}

851859}

860+@misc{Brady2012c,

861+author = {Brooks, Fred},

862+doi = {10.1093/epirev/mxr031},

863+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},

864+isbn = {9780321702081},

865+issn = {1478-6729},

866+number = {1},

867+pages = {NP},

868+pmid = {22215642},

869+title = {{The Design of Design Chapter 5}},

870+volume = {34}

871+}

852872@article{mcbride2008functional,

853873author = {McBride, C. and Paterson, R.},

854−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},

874+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},

855875journal = {Journal of functional programming},

856876number = {1},

857877pages = {1--13},

@@ -866,7 +886,7 @@ abstract = {The recent success of languages like Agda and Coq demonstrates the p

866886author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas},

867887doi = {10.1007/978-3-642-12251-4_5},

868888editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},

869−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

889+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

870890isbn = {9783642122507},

871891journal = {Computing},

872892number = {Sheard 2005},

@@ -881,7 +901,7 @@ year = {2010}

881901@inproceedings{morris2006exploring,

882902author = {Morris, P. and Altenkirch, T. and McBride, C.},

883903booktitle = {Types for Proofs and Programs},

884−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

904+file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

885905pages = {252--267},

886906publisher = {Springer},

887907title = {{Exploring the regular tree types}},

@@ -893,7 +913,7 @@ abstract = {Note: OCR errors may be found in this Reference List extracted from

893913author = {Xi, Hongwei and Pfenning, Frank},

894914booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},

895915doi = {10.1145/292540.292560},

896−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

916+file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

897917isbn = {1581130953},

898918issn = {07439016},

899919keywords = {Dependent Types},

@@ -912,7 +932,7 @@ abstract = {The use of monads to structure functional programs is described. Mon

912932author = {Wadler, Philip},

913933doi = {10.1007/3-540-59451-5_2},

914934editor = {Jeuring, Johan and Meijer, Erik},

915−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Wadler - 2001 - Monads for functional programming.pdf:pdf},

935+file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},

916936isbn = {3540594515},

917937issn = {03029743},

918938journal = {Advanced Functional Programming},

@@ -925,6 +945,14 @@ url = {http://www.springerlink.com/index/715264614rh13340.pdf},

925945volume = {925},

926946year = {2001}

927947}

948+@inproceedings{brady2011epic,

949+author = {Brady, Edwin},

950+booktitle = {Trends in Functional Programming ({TFP}’11)},

951+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

952+title = {{Epic --- A Library for Generating Compilers}},

953+url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},

954+year = {2011}

955+}

928956@inproceedings{taha2004gentle,

929957author = {Taha, W.},

930958booktitle = {Domain-Specific Program Generation},

@@ -934,10 +962,22 @@ title = {{A gentle introduction to multi-stage programming}},

934962url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},

935963year = {2004}

936964}

965+@inproceedings{chlipala2010ur,

966+author = {Chlipala, Adam},

967+booktitle = {ACM SIGPLAN Notices},

968+file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

969+number = {6},

970+pages = {122--133},

971+publisher = {ACM},

972+title = {{Ur: statically-typed metaprogramming with type-level record computation}},

973+url = {http://dl.acm.org/citation.cfm?id=1806612},

974+volume = {45},

975+year = {2010}

976+}

937977@inproceedings{McBride2004b,

938978author = {McBride, Conor and McKinna, James},

939979booktitle = {Haskell Workshop},

940−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

980+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

941981title = {{I am not a number : I am a free variable}},

942982year = {2004}

943983}

@@ -952,9 +992,21 @@ url = {http://dl.acm.org/citation.cfm?id=1065046},

952992volume = {40},

953993year = {2005}

954994}

995+@article{loh2010tutorial,

996+author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},

997+file = {:Users/edwin/Documents/Mendeley Desktop/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},

998+journal = {Fundamenta Informaticae},

999+number = {2},

1000+pages = {177--207},

1001+publisher = {IOS Press},

1002+title = {{A tutorial implementation of a dependently typed lambda calculus}},

1003+url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},

1004+volume = {102},

1005+year = {2010}

1006+}

9551007@article{Okasaki1993,

9561008author = {Okasaki, Chris},

957−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

1009+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

9581010journal = {Journal of functional programming},

9591011title = {{Red-Black Trees in A Functional Setting}},

9601012year = {1993}

@@ -962,7 +1014,7 @@ year = {1993}

9621014@misc{Attacks2012a,

9631015author = {Anderson, Ross},

9641016doi = {10.1093/epirev/mxr031},

965−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

1017+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

9661018isbn = {9780470068526},

9671019issn = {1478-6729},

9681020number = {1},

@@ -975,7 +1027,7 @@ volume = {34}

9751027abstract = {We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.},

9761028author = {Xi, Hongwei and Pfenning, Frank},

9771029doi = {10.1145/277652.277732},

978−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},

1030+file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},

9791031isbn = {0897919874},

9801032issn = {03621340},

9811033journal = {ACM Sigplan Notices},

impl-paper/macros.ltx+4

@@ -116,6 +116,10 @@

116116\newcommand{\RW}[1]{\underline{\textrm{#1}}}

117117\newcommand{\MO}[1]{\mbox{\textsc{#1}}}

118118

119+\newcommand{\tTC}[1]{\texttt{#1}}

120+\newcommand{\tDC}[1]{\texttt{#1}}

121+\newcommand{\tFN}[1]{\texttt{#1}}

122+

119123\newcommand{\HF}[1]{\mathtt{#1}}

120124

121125\newcommand{\MV}[1]{\nhole\mathit{#1}}

impl-paper/typechecking.tex+30−1

@@ -1,6 +1,19 @@

11\section{The Core Type Theory}

3−\DM{

3+High level \Idris{} programs, as described in Section \ref{sect:hll} are

4+\remph{elaborated} to a small core language, \TT{}, then type checked. We keep the

5+core language as small as is reasonable. This has several advantages: it is

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

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

8+the language small increases our confidence that these important components of

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

10+its semantics.

11+

12+\subsection{\TT{} syntax}

13+

14+The syntax of \TT{} expressions is given in Figure \ref{ttsyn}.

15+

16+\FFIG{

417\begin{array}{rll@{\hg}|rll}

518\vt ::= & \Type_i & (\mbox{type universes}) &

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

@@ -15,4 +28,20 @@

1528

1629\end{array}

1730}

31+{\TT{} expression syntax}

32+{ttsyn}

33+

34+\subsection{Evaluation rules}

35+

36+\subsection{Typing rules}

37+

38+\subsection{The Development Calculus \TTdev}

39+

40+\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.

41+

42+\subsection{The $\MO{Elab}$ meta-language}

43+

1844

45+\begin{itemize}

46+\item $\MO{Check}\:\vt\:\cq\:(\vt, \vt)$

47+\end{itemize}

tutorial/classes.tex+1−1

@@ -138,7 +138,7 @@ missing, and there is a default definition for it, then the default is used inst

138138

139139Classes can also be extended. A logical next step from an equality relation \texttt{Eq}

140140is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class

141−which inherits method from \texttt{Eq} as well as defining some of its own:

141+which inherits methods from \texttt{Eq} as well as defining some of its own:

142142

143143\begin{SaveVerbatim}{ord}

144144

tutorial/intro.tex+1−1

@@ -46,7 +46,7 @@ app : Vect a n -> Vect a m -> Vect a (n + m)

4646This tutorial introduces \Idris{}, a general purpose functional

4747programming language with dependent types.

4848The goal of the \Idris{} project is to build a dependently typed language suitable

49−for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language

49+for verifiable \emph{systems} programming. To this end, \Idris{} is a compiled language

5050which aims to generate efficient executable code. It also has a lightweight foreign

5151function interface which allows easy interaction with external C libraries.

5252

tutorial/miscellany.tex+1−1

@@ -10,7 +10,7 @@ foriegn function interface, and the universe hierarchy.

1010We have already seen implicit arguments, which allows arguments to be omitted when

1111they can be inferred by the type checker, e.g.

1212

13−\useverb{vlookupimpty}

13+\useverb{vindeximpty}

1414

1515\noindent

1616In other situations, it may be possible to infer arguments not by type checking but

tutorial/typesfuns.tex+27−27

@@ -97,7 +97,7 @@ such as this can be added using a fixity declaration, as follows:

9797

9898\begin{SaveVerbatim}{infixcons}

9999

100−infixr 7 ::

100+infixr 10 ::

101101

102102\end{SaveVerbatim}

103103\useverb{infixcons}

@@ -105,7 +105,7 @@ infixr 7 ::

105105\noindent

106106Functions, data constructors and type constuctors may all be given infix

107107operators as names. They may be used in prefix form if enclosed in brackets,

108−e.g. (::). Infix operators can use any of the symbols:

108+e.g. \tDC{(::)}. Infix operators can use any of the symbols:

109109

110110\begin{SaveVerbatim}{infixsyms}

111111

@@ -150,7 +150,7 @@ names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},

150150\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are

151151all part of the same namespace.

152152

153−We can test these functions at the Idris prompt:

153+We can test these functions at the \Idris{} prompt:

154154

155155\begin{SaveVerbatim}{fntest}

156156

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

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

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

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

257−be used to construct vectors with zero length, and \tDC{::} to constructor

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

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

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

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

@@ -275,7 +275,7 @@ library, appends two \tTC{Vect}s:

275275\useverb{vapp}

276276

277277\noindent

278−The type of \tFN{app} states that the resulting vector's length will be the sum of

278+The type of \tFN{(++)} states that the resulting vector's length will be the sum of

279279the input lengths. If we get the definition wrong in such a way that this does

280280not hold, \Idris{} will not accept the definition. For example:

281281

@@ -339,14 +339,14 @@ numbers bounded by \tTC{n}.

339339For example, the following function which looks up an element in a \tTC{Vect},

340340by a bounded index given as a \tTC{Fin n}, is defined in the prelude:

341341

342−\begin{SaveVerbatim}{vlookup}

342+\begin{SaveVerbatim}{vindex}

343343

344−lookup : Fin n -> Vect a n -> a

345−lookup fO (x :: xs) = x

346−lookup (fS k) (x :: xs) = lookup k xs

344+index : Fin n -> Vect a n -> a

345+index fO (x :: xs) = x

346+index (fS k) (x :: xs) = index k xs

347347

348348\end{SaveVerbatim}

349−\useverb{vlookup}

349+\useverb{vindex}

350350

351351\noindent

352352This function looks up a value at a given location in a vector. The location is

@@ -362,54 +362,54 @@ since it would force \texttt{n} to be \tDC{O}.

362362

363363\subsubsection{Implicit Arguments}

364364

365−Let us take a closer look at the type of \texttt{lookup}:

365+Let us take a closer look at the type of \texttt{index}:

366366

367−\begin{SaveVerbatim}{vlookupty}

367+\begin{SaveVerbatim}{vindexty}

368368

369−lookup : Fin n -> Vect a n -> a

369+index : Fin n -> Vect a n -> a

370370

371371\end{SaveVerbatim}

372−\useverb{vlookupty}

372+\useverb{vindexty}

373373

374374\noindent

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

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

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

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

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

379379

380−\begin{SaveVerbatim}{vlookupimpty}

380+\begin{SaveVerbatim}{vindeximpty}

381381

382−lookup : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a

382+index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a

383383

384384\end{SaveVerbatim}

385−\useverb{vlookupimpty}

385+\useverb{vindeximpty}

386386

387387\noindent

388388Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in

389−applications of \texttt{lookup}; their values can be inferred from the types of

389+applications of \texttt{index}; their values can be inferred from the types of

390390the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter

391391or index in a type declaration, but which is otherwise free, will be automatically

392392bound as an implicit argument.

393393Implicit arguments can still be given explicitly in applications, using

394−{a=value} and {n=value}, for example:

394+\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:

395395

396−\begin{SaveVerbatim}{vlookupexp}

396+\begin{SaveVerbatim}{vindexexp}

397397

398−lookup {a=Int} {n=2} fO (2 :: 3 :: Nil)

398+index {a=Int} {n=2} fO (2 :: 3 :: Nil)

399399

400400\end{SaveVerbatim}

401−\useverb{vlookupexp}

401+\useverb{vindexexp}

402402

403403\noindent

404404In fact, any argument, implicit or explicit, may be given a name. We could have

405−declared the type of \texttt{lookup} as:

405+declared the type of \texttt{index} as:

406406

407−\begin{SaveVerbatim}{vlookupn}

407+\begin{SaveVerbatim}{vindexn}

408408

409−lookup : (i:Fin n) -> (xs:Vect a n) -> a

409+index : (i:Fin n) -> (xs:Vect a n) -> a

410410

411411\end{SaveVerbatim}

412−\useverb{vlookupn}

412+\useverb{vindexn}

413413

414414\noindent

415415It is a matter of taste whether you want to do this --- sometimes it can help