cda1274 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #613 from jfdm/tutorial

Changes to tutorial.

commitcda12747567d86906aa1183e05783f560445c52c authorEdwin Brady <edwin.brady@gmail.com> dateWed 13 Nov 2013, 07:36 (13 years ago) parent3c2443e 32e29e1

20 files changed+768−1194

compare with master

unifiedsplit

.gitignore+2

@@ -21,3 +21,5 @@ tutorial/*.blg

2121tutorial/*.log

2222tutorial/*.out

2323tutorial/*.toc

24+tutorial/*.fdb_latexmk

25+tutorial/*.fls

tutorial/Makefile+1−4

@@ -2,9 +2,7 @@ PAPER = idris-tutorial

33all: ${PAPER}.pdf

5−TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \

6− classes.tex modules.tex interp.tex views.tex theorems.tex \

7− provisional.tex syntax.tex conclusions.tex miscellany.tex dsl.tex

5+TEXFILES = ${PAPER}.tex content/*.tex

97DIAGS =

108

@@ -13,7 +11,6 @@ SOURCES = ${TEXFILES} ${DIAGS} macros.ltx library.ltx literature.bib

1311DITAA = java -jar ~/Downloads/ditaa.jar

1412

1513${PAPER}.pdf: ${SOURCES}

16−# dvipdf ${PAPER}.dvi

1714 pdflatex ${PAPER}

1815 -bibtex ${PAPER}

1916 -pdflatex ${PAPER}

tutorial/conf.ltx+6−1

@@ -1,6 +1,11 @@

1−

21%% This file contains configurations of used packages

3+\lstset{%

4+ basicstyle=\ttfamily,

5+ xleftmargin=\parindent,

6+ tabsize=2

7+}

510% Configuration of hyperref (to not use colors):

611\hypersetup{

tutorial/classes.tex → tutorial/content/classes.texrenamed+66−163

@@ -14,24 +14,18 @@ is the \texttt{Show} type class, which is defined in the prelude and

1414provides an interface for converting values to

1515\texttt{String}s:

1616

17−\begin{SaveVerbatim}{showclass}

18−

17+\begin{code}

1918class Show a where

2019 show : a -> String

21−

22−\end{SaveVerbatim}

23−\useverb{showclass}

20+\end{code}

2421

2522\noindent

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

2724\texttt{Show} class):

2825

29−\begin{SaveVerbatim}{showty}

30−

26+\begin{code}

3127show : Show a => a -> String

32−

33−\end{SaveVerbatim}

34−\useverb{showty}

28+\end{code}

3529

3630\noindent

3731We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},

@@ -40,17 +34,16 @@ is defined with an \texttt{instance} declaration, which provides implementations

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

4135could be defined as:

4236

43−\begin{SaveVerbatim}{shownat}

44−

37+\begin{code}

4538instance Show Nat where

4639 show Z = "Z"

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

41+\end{code}

4842

43+\begin{lstlisting}

4944Idris> show (S (S (S Z)))

5045"sssO" : String

51−

52−\end{SaveVerbatim}

53−\useverb{shownat}

46+\end{lstlisting}

5447

5548\noindent

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

@@ -59,17 +52,14 @@ Instance declarations can themselves have constraints. For example, to define a

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

6053to a \texttt{String}:

6154

62−\begin{SaveVerbatim}{showvec}

63−

55+\begin{code}

6456instance Show a => Show (Vect n a) where

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

6658 show' : Vect n a -> String

6759 show' Nil = ""

6860 show' (x :: Nil) = show x

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

70−

71−\end{SaveVerbatim}

72−\useverb{showvec}

62+\end{code}

7363

7464%\noindent

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

@@ -85,21 +75,17 @@ instance Show a => Show (Vect n a) where

8575The library defines an \texttt{Eq} class which provides an interface for comparing

8676values for equality or inequality, with instances for all of the built-in types:

8777

88−\begin{SaveVerbatim}{eqbasic}

89−

78+\begin{code}

9079class Eq a where

9180 (==) : a -> a -> Bool

9281 (/=) : a -> a -> Bool

93−

94−\end{SaveVerbatim}

95−\useverb{eqbasic}

82+\end{code}

9683

9784\noindent

9885To declare an instance of a type, we have to give definitions of all of the methods.

9986For example, for an instance of \texttt{Eq} for \texttt{Nat}:

10087

101−\begin{SaveVerbatim}{eqnat}

102−

88+\begin{code}

10389instance Eq Nat where

10490 Z == Z = True

10591 (S x) == (S y) = x == y

@@ -107,9 +93,7 @@ instance Eq Nat where

10793 (S x) == Z = False

10894

10995 x /= y = not (x == y)

110−

111−\end{SaveVerbatim}

112−\useverb{eqnat}

96+\end{code}

11397

11498\noindent

11599It is hard to imagine many cases where the \texttt{/=} method will be anything other

@@ -117,17 +101,14 @@ than the negation of the result of applying the \texttt{==} method. It is theref

117101convenient to give a default definition for each method in the class

118102declaration, in terms of the other method:

119103

120−\begin{SaveVerbatim}{eqdefault}

121−

104+\begin{code}

122105class Eq a where

123106 (==) : a -> a -> Bool

124107 (/=) : a -> a -> Bool

125108

126109 x /= y = not (x == y)

127110 y == y = not (x /= y)

128−

129−\end{SaveVerbatim}

130−\useverb{eqdefault}

111+\end{code}

131112

132113\noindent

133114A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}

@@ -140,15 +121,11 @@ Classes can also be extended. A logical next step from an equality relation \tex

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

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

142123

143−\begin{SaveVerbatim}{ord}

144−

124+\begin{code}

145125data Ordering = LT | EQ | GT

126+\end{code}

146127

147−\end{SaveVerbatim}

148−\useverb{ord}

149−

150−\begin{SaveVerbatim}{eqord}

151−

128+\begin{code}

152129class Eq a => Ord a where

153130 compare : a -> a -> Ordering

154131

@@ -158,9 +135,7 @@ class Eq a => Ord a where

158135 (>=) : a -> a -> Bool

159136 max : a -> a -> a

160137 min : a -> a -> a

161−

162−\end{SaveVerbatim}

163−\useverb{eqord}

138+\end{code}

164139

165140\noindent

166141The \texttt{Ord} class allows us to compare two values and determine their ordering.

@@ -171,24 +146,18 @@ increasing order, provided that the element type of the list is in the \texttt{O

171146We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the

172147function type to the right of the fat arrow:

173148

174−\begin{SaveVerbatim}{sortty}

175−

149+\begin{code}

176150sort : Ord a => List a -> List a

177−

178−\end{SaveVerbatim}

179−\useverb{sortty}

151+\end{code}

180152

181153\noindent

182154Functions, classes and instances can have multiple constraints. Multiple constaints are

183155written in brackets in a comma separated list, for example:

184156

185−\begin{SaveVerbatim}{sortshow}

186−

157+\begin{code}

187158sortAndShow : (Ord a, Show a) => List a -> String

188159sortAndShow xs = show (sort xs)

189−

190−\end{SaveVerbatim}

191−\useverb{sortshow}

160+\end{code}

192161

193162\subsection{Monads and \texttt{do}-notation}

194163

@@ -200,14 +169,11 @@ and the parameters can have \remph{any} type.

200169If the type of the parameter is not \texttt{Type}, we need to give an explicit type

201170declaration. For example:

202171

203−\begin{SaveVerbatim}{monad}

204−

172+\begin{code}

205173class Monad (m : Type -> Type) where

206174 return : a -> m a

207175 (>>=) : m a -> (a -> m b) -> m b

208−

209−\end{SaveVerbatim}

210−\useverb{monad}

176+\end{code}

211177

212178\noindent

213179The \texttt{Monad} class allows us to encapsulate binding and computation, and is the

@@ -224,30 +190,24 @@ basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a

224190\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.

225191We can also define an instance for \texttt{Maybe}, as follows:

226192

227−\begin{SaveVerbatim}{maybemonad}

228−

193+\begin{code}

229194instance Monad Maybe where

230195 return = Just

231196

232197 Nothing >>= k = Nothing

233198 (Just x) >>= k = k x

234−

235−\end{SaveVerbatim}

236−\useverb{maybemonad}

199+\end{code}

237200

238201\noindent

239202Using this we can, for example, define a function which adds two

240203\texttt{Maybe Int}s, using the monad to encapsulate the error handling:

241204

242−\begin{SaveVerbatim}{maybeadd}

243−

205+\begin{code}

244206m_add : Maybe Int -> Maybe Int -> Maybe Int

245207m_add x y = do x' <- x -- Extract value from x

246208 y' <- y -- Extract value from y

247209 return (x' + y') -- Add them

248−

249−\end{SaveVerbatim}

250−\useverb{maybeadd}

210+\end{code}

251211

252212\noindent

253213This function will extract the values from \texttt{x} and \texttt{y}, if they

@@ -255,29 +215,23 @@ are available, or return \texttt{Nothing} if they are not. Managing the

255215\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the

256216\texttt{do} notation.

257217

258−\begin{SaveVerbatim}{maybeaddt}

259−

218+\begin{lstlisting}

260219*classes> m_add (Just 20) (Just 22)

261220Just 42 : Maybe Int

262221*classes> m_add (Just 20) Nothing

263222Nothing : Maybe Int

264−

265−\end{SaveVerbatim}

266−\useverb{maybeaddt}

223+\end{lstlisting}

267224

268225\subsubsection*{Monad comprehensions}

269226

270227The list comprehension notation we saw in Section \ref{sec:listcomp} is more

271228general, and applies to anything which is an instance of \texttt{MonadPlus}:

272229

273−\begin{SaveVerbatim}{monadplus}

274−

230+\begin{code}

275231class Monad m => MonadPlus (m : Type -> Type) where

276232 mplus : m a -> m a -> m a

277233 mzero : m a

278−

279−\end{SaveVerbatim}

280−\useverb{monadplus}

234+\end{code}

281235

282236\noindent

283237In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where

@@ -295,32 +249,24 @@ any qualifier

295249\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using

296250the following function:

297251

298−\begin{SaveVerbatim}{guardq}

299−

252+\begin{code}

300253guard : MonadPlus m => Bool -> m ()

301−

302−\end{SaveVerbatim}

303−\useverb{guardq}

254+\end{code}

304255

305256\noindent

306257Then the comprehension is converted to \texttt{do} notation:

307258

308−\begin{SaveVerbatim}{comptrans}

309−

259+\begin{code}

310260do { qual1; qual2; ...; qualn; return exp; }

311−

312−\end{SaveVerbatim}

313−\useverb{comptrans}

261+\end{code}

314262

315263\noindent

316264Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:

317265

318−\begin{SaveVerbatim}{maddb}

319−

266+\begin{code}

320267m_add : Maybe Int -> Maybe Int -> Maybe Int

321268m_add x y = [ x' + y' | x' <- x, y' <- y ]

322−\end{SaveVerbatim}

323−\useverb{maddb}

269+\end{code}

324270

325271\subsection{Idiom brackets}

326272

@@ -333,26 +279,20 @@ First, let us revisit \texttt{m\_add} above. All it is really doing is applying

333279an operator to two values extracted from Maybe Ints. We could abstract out the

334280application:

335281

336−\begin{SaveVerbatim}{mapp}

337−

282+\begin{code}

338283m_app : Maybe (a -> b) -> Maybe a -> Maybe b

339284m_app (Just f) (Just a) = Just (f a)

340285m_app _ _ = Nothing

341−

342−\end{SaveVerbatim}

343−\useverb{mapp}

286+\end{code}

344287

345288\noindent

346289Using this, we can write an alternative \texttt{m\_add} which uses this alternative

347290notion of function application, with explicit calls to \texttt{m\_app}:

348291

349−\begin{SaveVerbatim}{maddb}

350−

292+\begin{code}

351293m_add' : Maybe Int -> Maybe Int -> Maybe Int

352294m_add' x y = m_app (m_app (Just (+)) x) y

353−

354−\end{SaveVerbatim}

355−\useverb{maddb}

295+\end{code}

356296

357297\noindent

358298Rather than having to insert \texttt{m\_app} everywhere there is an

@@ -360,44 +300,35 @@ application, we can use \remph{idiom brackets} to do the job for us. To do

360300this, we use the \texttt{Applicative} class, which captures the notion of

361301application for a data type:

362302

363−\begin{SaveVerbatim}{applicative}

364−

303+\begin{code}

365304infixl 2 <$>

366305

367306class Applicative (f : Type -> Type) where

368307 pure : a -> f a

369308 (<$>) : f (a -> b) -> f a -> f b

370−

371−\end{SaveVerbatim}

372−\useverb{applicative}

309+\end{code}

373310

374311\noindent

375312\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where

376313\texttt{<\$>} is defined in the same way as \texttt{m\_app} above:

377314

378−\begin{SaveVerbatim}{maybeapp}

379−

315+\begin{code}

380316instance Applicative Maybe where

381317 pure = Just

382318

383319 (Just f) <$> (Just a) = Just (f a)

384320 _ <$> _ = Nothing

385−

386−\end{SaveVerbatim}

387−\useverb{maybeapp}

321+\end{code}

388322

389323\noindent

390324Using \remph{idiom brackets} we can use this instance as follows, where a function

391325application \texttt{[| f a1 ... an |]}

392326is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:

393327

394−\begin{SaveVerbatim}{maddc}

395−

328+\begin{code}

396329m_add' : Maybe Int -> Maybe Int -> Maybe Int

397330m_add' x y = [| x + y |]

398−

399−\end{SaveVerbatim}

400−\useverb{maddc}

331+\end{code}

401332

402333\subsubsection{An error-handling interpreter}

403334

@@ -405,43 +336,34 @@ Idiom notation is commonly useful when defining evaluators. McBride and

405336Paterson describe such an evaluator~\cite{idioms}, for a language similar to

406337the following:

407338

408−\begin{SaveVerbatim}{idiomexpr}

409−

339+\begin{code}

410340data Expr = Var String -- variables

411341 | Val Int -- values

412342 | Add Expr Expr -- addition

413−

414−\end{SaveVerbatim}

415−\useverb{idiomexpr}

343+\end{code}

416344

417345\noindent

418346Evaluation will take place relative to a context mapping variables (represented as

419347\texttt{String}s) to integer values, and can possibly fail. We define a data type

420348\texttt{Eval} to wrap an evaluator:

421349

422−\begin{SaveVerbatim}{evalctxt}

423−

350+\begin{code}

424351data Eval : Type -> Type where

425352 MkEval : (List (String, Int) -> Maybe a) -> Eval a

426−

427−\end{SaveVerbatim}

428−\useverb{evalctxt}

353+\end{code}

429354

430355\noindent

431356Wrapping the evaluator in a data type means we will be able to make it an instance

432357of a type class later. We begin by defining a function to retrieve values from

433358the context during evaluation:

434359

435−\begin{SaveVerbatim}{fetch}

436−

360+\begin{code}

437361fetch : String -> Eval Int

438362fetch x = MkEval (\e => fetchVal e) where

439363 fetchVal : List (String, Int) -> Maybe Int

440364 fetchVal [] = Nothing

441365 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

442−

443−\end{SaveVerbatim}

444−\useverb{fetch}

366+\end{code}

445367

446368\noindent

447369When defining an evaluator for the language, we will be applying functions in

@@ -451,8 +373,7 @@ Before \texttt{Eval} can be an instance of

451373\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of

452374\texttt{Functor}:

453375

454−\begin{SaveVerbatim}{}

455−

376+\begin{code}

456377instance Functor Eval where

457378 fmap f (MkEval g) = MkEval (\e => fmap f (g e))

458379

@@ -463,20 +384,13 @@ instance Applicative Eval where

463384 app : Maybe (a -> b) -> Maybe a -> Maybe b

464385 app (Just fx) (Just gx) = Just (fx gx)

465386 app _ _ = Nothing

466−

467−\end{SaveVerbatim}

468−\useverb{}

469−

470−\begin{SaveVerbatim}{grr}

471−<$>

472−\end{SaveVerbatim}

387+\end{code}

473388

474389\noindent

475390Evaluating an expression can now make use of the idiomatic application to handle

476391errors:

477392

478−\begin{SaveVerbatim}{evalexpr}

479−

393+\begin{code}

480394eval : Expr -> Eval Int

481395eval (Var x) = fetch x

482396eval (Val x) = [| x |]

@@ -485,9 +399,7 @@ eval (Add x y) = [| eval x + eval y |]

485399runEval : List (String, Int) -> Expr -> Maybe Int

486400runEval env e = case eval e of

487401 MkEval envFn => envFn env

488−

489−\end{SaveVerbatim}

490−\useverb{evalexpr}

402+\end{code}

491403

492404\subsection{Named Instances}

493405

@@ -495,16 +407,13 @@ It can be desirable to have multiple instances of a type class, for example to p

495407alternative methods for sorting or printing values. To achieve this, instances can

496408be \remph{named} as follows:

497409

498−\begin{SaveVerbatim}{myord}

499−

410+\begin{code}

500411instance [myord] Ord Nat where

501412 compare Z (S n) = GT

502413 compare (S n) Z = LT

503414 compare Z Z = EQ

504415 compare (S x) (S y) = compare @{myord} x y

505−

506−\end{SaveVerbatim}

507−\useverb{myord}

416+\end{code}

508417

509418\noindent

510419This declares an instance as normal, but with an explicit name, \texttt{myord}.

@@ -513,25 +422,19 @@ The syntax \texttt{compare @\{myord\}} gives an explicit instance to

513422We can use this, for example, to sort a list of \texttt{Nat}s in reverse.

514423Given the following list:

515424

516−\begin{SaveVerbatim}{myordlist}

517−

425+\begin{code}

518426testList : List Nat

519427testList = [3,4,1]

520−

521−\end{SaveVerbatim}

522−\useverb{myordlist}

428+\end{code}

523429

524430\noindent

525431\ldots we can sort it using the default \texttt{Ord} instance, then the named

526432instance \texttt{myord} as follows, at the \Idris{} prompt:

527433

528−\begin{SaveVerbatim}{myordlistrun}

529−

434+\begin{lstlisting}

530435*named_instance> show (sort testList)

531436"[sO, sssO, ssssO]" : String

532437*named_instance> show (sort @{myord} testList)

533438"[ssssO, sssO, sO]" : String

534−

535−\end{SaveVerbatim}

536−\useverb{myordlistrun}

439+\end{lstlisting}

537440

tutorial/conclusions.tex → tutorial/content/conclusions.texrenamed

The content is the same.

tutorial/dsl.tex → tutorial/content/dsl.texrenamed+16−26

@@ -11,23 +11,25 @@ running concurrent processes safely~\cite{cbconc-fi}.

1111Unfortunately, the form of object language programs makes it rather hard to program

1212this way in practice. Recall the factorial program in \texttt{Expr} for example:

1313

14−\useverb{facttest}

14+\begin{code}

15+fact : Expr G (TyFun TyInt TyInt)

16+fact = Lam (If (Op (==) (Var stop) (Val 0))

17+ (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))

18+ (Var stop)))

19+\end{code}

1520

1621\noindent

1722Since this is a particularly useful pattern, \Idris{} provides syntax

1823overloading~\cite{res-dsl-padl12} to make it easier to program in such

1924object languages:

2025

21−\begin{SaveVerbatim}{exprdsl}

22−

26+\begin{code}

2327dsl expr

2428 lambda = Lam

2529 variable = Var

2630 index_first = stop

2731 index_next = pop

28−

29−\end{SaveVerbatim}

30−\useverb{exprdsl}

32+\end{code}

3133

3234\noindent

3335A \texttt{dsl} block describes how each syntactic construct is represented in an

@@ -38,55 +40,43 @@ de Bruijn index (i.e., to count how many bindings since the variable itself was

3840It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact}

3941as follows:

4042

41−\begin{SaveVerbatim}{factb}

42−

43+\begin{code}

4344fact : Expr G (TyFun TyInt TyInt)

4445fact = expr (\x => If (Op (==) x (Val 0))

4546 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))

46−

47−\end{SaveVerbatim}

48−\useverb{factb}

47+\end{code}

4948

5049\noindent

5150In this new version, \texttt{expr} declares that the next expression will be overloaded.

5251We can take this further, using idiom brackets, by declaring:

5352

54−\begin{SaveVerbatim}{idiomexpr}

55−

53+\begin{code}

5654(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

5755(<$>) = \f, a => App f a

5856

5957pure : Expr G a -> Expr G a

6058pure = id

61−

62−\end{SaveVerbatim}

63−\useverb{idiomexpr}

59+\end{code}

6460

6561\noindent

6662Note that there is no need for these to be part of an instance of \texttt{Applicative},

6763since idiom bracket notation translates directly to the names \texttt{<\$>} and

6864\texttt{pure}, and ad-hoc type-directed overloading is allowed. We can now say:

6965

70−\begin{SaveVerbatim}{factc}

71−

66+\begin{code}

7267fact : Expr G (TyFun TyInt TyInt)

7368fact = expr (\x => If (Op (==) x (Val 0))

7469 (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))

75−

76−\end{SaveVerbatim}

77−\useverb{factc}

70+\end{code}

7871

7972\noindent

8073With some more ad-hoc overloading and type class instances, and a new

8174syntax rule, we can even go as far as:

8275

83−\begin{SaveVerbatim}{factd}

84−

76+\begin{code}

8577syntax IF [x] THEN [t] ELSE [e] = If x t e

8678

8779fact : Expr G (TyFun TyInt TyInt)

8880fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)

89−

90−\end{SaveVerbatim}

91−\useverb{factd}

81+\end{code}

9282

tutorial/interp.tex → tutorial/content/interp.texrenamed+61−143

@@ -1,5 +1,4 @@

11\section{Example: The Well-Typed Interpreter}

2−

32\label{sect:interp}

54In this section, we'll use the features we've seen so far to write a larger

@@ -9,27 +8,21 @@ construct. We will use the dependent type system to ensure that any programs

98which can be represented are well-typed. First, let us define the types in the

109language. We have integers, booleans, and functions, represented by \texttt{Ty}:

1110

12−\begin{SaveVerbatim}{tydecl}

13−

11+\begin{code}

1412data Ty = TyInt | TyBool | TyFun Ty Ty

15−

16−\end{SaveVerbatim}

17−\useverb{tydecl}

13+\end{code}

1814

1915\noindent

2016We can write a function to translate these representations to a concrete \Idris{}

2117type --- remember that types are first class, so can be calculated just like

2218any other value:

2319

24−\begin{SaveVerbatim}{interpty}

25−

20+\begin{code}

2621interpTy : Ty -> Type

2722interpTy TyInt = Int

2823interpTy TyBool = Bool

2924interpTy (TyFun A T) = interpTy A -> interpTy T

30−

31−\end{SaveVerbatim}

32−\useverb{interpty}

25+\end{code}

3326

3427\noindent

3528We're going to define a representation of our language in such a way that only

@@ -38,31 +31,24 @@ expressions by their type and the types of local variables (the context), which

3831we'll be using regularly as an implicit argument, so we define everything

3932in a \texttt{using} block:

4033

41−\begin{SaveVerbatim}{usingg}

42−

34+\begin{code}

4335using (G:Vect n Ty)

44−

45−\end{SaveVerbatim}

46−\useverb{usingg}

36+\end{code}

4737

4838\noindent

4939The full representation of expressions is given in Figure \ref{exprty}. They are

5040indexed by the types of the local variables, and the type of the expression itself:

5141

52−\begin{SaveVerbatim}{exprdecl}

53−

42+\begin{code}

5443data Expr : Vect n Ty -> Ty -> Type

55−

56−\end{SaveVerbatim}

57−\useverb{exprdecl}

44+\end{code}

5845

5946\noindent

6047Since expressions are indexed by their type, we can read the typing rules of

6148the language from the definitions of the constructors. Let us look at each

6249constructor in turn.

6350

64−\begin{SaveVerbatim}{exprty}

65−

51+\begin{code}[caption={Expression representation},label=exprty]

6652data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

6753 stop : HasType fZ (t :: G) t

6854 pop : HasType k G t -> HasType (fS k) (u :: G) t

@@ -75,9 +61,7 @@ data Expr : Vect n Ty -> Ty -> Type where

7561 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

7662 Expr G c

7763 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

78−

79−\end{SaveVerbatim}

80−\codefig{exprty}{Expression representation}

64+\end{code}

8165

8266\noindent

8367We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.

@@ -85,14 +69,11 @@ Variables are represented by a proof of their membership in the context,

8569\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context

8670\texttt{G} has type \texttt{T}. This is defined as follows:

8771

88−\begin{SaveVerbatim}{hastype}

89−

72+\begin{code}

9073data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

9174 stop : HasType fZ (t :: G) t

9275 pop : HasType k G t -> HasType (fS k) (u :: G) t

93−

94−\end{SaveVerbatim}

95−\useverb{hastype}

76+\end{code}

9677

9778\noindent

9879We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,

@@ -101,12 +82,9 @@ well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{sto

10182refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,

10283via the \texttt{Var} constructor:

10384

104−\begin{SaveVerbatim}{varcon}

105−

85+\begin{code}

10686Var : HasType i G t -> Expr G t

107−

108−\end{SaveVerbatim}

109−\useverb{varcon}

87+\end{code}

11088

11189\noindent

11290So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},

@@ -118,58 +96,43 @@ definition and the use.

11896\noindent

11997A value carries a concrete representation of an integer:

12098

121−\begin{SaveVerbatim}{valcon}

122−

99+\begin{code}

123100Val : (x : Int) -> Expr G TyInt

124−

125−\end{SaveVerbatim}

126−\useverb{valcon}

101+\end{code}

127102

128103\noindent

129104A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is

130105a new local variable of type \texttt{a}, which is expressed by the context index:

131106

132−\begin{SaveVerbatim}{lamcon}

133−

107+\begin{code}

134108Lam : Expr (a :: G) t -> Expr G (TyFun a t)

135−

136−\end{SaveVerbatim}

137−\useverb{lamcon}

109+\end{code}

138110

139111\noindent

140112Function application produces a value of type \texttt{t} given a function from

141113\texttt{a} to \texttt{t}

142114and a value of type \texttt{a}:

143115

144−\begin{SaveVerbatim}{appcon}

145−

116+\begin{code}

146117App : Expr G (TyFun a t) -> Expr G a -> Expr G t

147−

148−\end{SaveVerbatim}

149−\useverb{appcon}

118+\end{code}

150119

151120\noindent

152121We allow arbitrary binary operators, where the type of the operator

153122informs what the types of the arguments must be:

154123

155−\begin{SaveVerbatim}{opcon}

156−

124+\begin{code}

157125Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

158126 Expr G c

159−

160−\end{SaveVerbatim}

161−\useverb{opcon}

127+\end{code}

162128

163129\noindent

164130Finally, if expressions make a choice given a boolean. Each branch must

165131have the same type:

166132

167−\begin{SaveVerbatim}{ifcon}

168−

133+\begin{code}

169134If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

170−

171−\end{SaveVerbatim}

172−\useverb{ifcon}

135+\end{code}

173136

174137\noindent

175138When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as

@@ -179,8 +142,7 @@ to the vector of local variable types, we use the usual \texttt{::} and \texttt{

179142constructors so that we can use the usual list syntax. Given a proof that a variable

180143is defined in the context, we can then produce a value from the environment:

181144

182−\begin{SaveVerbatim}{envtype}

183−

145+\begin{code}

184146data Env : Vect n Ty -> Type where

185147 Nil : Env Nil

186148 (::) : interpTy a -> Env G -> Env (a :: G)

@@ -188,12 +150,9 @@ data Env : Vect n Ty -> Type where

188150lookup : HasType i G t -> Env G -> interpTy t

189151lookup stop (x :: xs) = x

190152lookup (pop k) (x :: xs) = lookup k xs

153+\end{code}

191154

192−\end{SaveVerbatim}

193−\useverb{envtype}

194−

195−\begin{SaveVerbatim}{interpdef}

196−

155+\begin{code}[caption={Intepreter definition},label=interpdef]

197156interp : Env G -> Expr G t -> interpTy t

198157interp env (Var i) = lookup i env

199158interp env (Val x) = x

@@ -202,65 +161,48 @@ interp env (App f s) = interp env f (interp env s)

202161interp env (Op op x y) = op (interp env x) (interp env y)

203162interp env (If x t e) = if interp env x then interp env t

204163 else interp env e

205−

206−\end{SaveVerbatim}

207−\codefig{interpdef}{Intepreter definition}

164+\end{code}

208165

209166\noindent

210167Given this, an interpreter (Figure \ref{interpdef})

211168is a function which translates an \texttt{Expr} into a

212169concrete \Idris{} value with respect to a specific environment:

213170

214−\begin{SaveVerbatim}{interpty}

215−

171+\begin{code}

216172interp : Env G -> Expr G t -> interpTy t

217−

218−\end{SaveVerbatim}

219−\useverb{interpty}

173+\end{code}

220174

221175\noindent

222176To translate a variable, we simply look it up in the environment:

223177

224−\begin{SaveVerbatim}{varinterp}

225−

178+\begin{code}

226179interp env (Var i) = lookup i env

227−

228−\end{SaveVerbatim}

229−\useverb{varinterp}

180+\end{code}

230181

231182\noindent

232183To translate a value, we just return the concrete representation of the value:

233184

234−\begin{SaveVerbatim}{valinterp}

235−

185+\begin{code}

236186interp env (Val x) = x

237−

238−\end{SaveVerbatim}

239−\useverb{valinterp}

187+\end{code}

240188

241189\noindent

242190Lambdas are more interesting. In this case, we construct a function which

243191interprets the scope of the lambda with a new value in the environment. So, a

244192function in the object language is translated to an \Idris{} function:

245193

246−\begin{SaveVerbatim}{laminterp}

247−

194+\begin{code}

248195interp env (Lam sc) = \x => interp (x :: env) sc

249−

250−\end{SaveVerbatim}

251−\useverb{laminterp}

196+\end{code}

252197

253198\noindent

254199For an application, we interpret the function and its argument and apply it

255200directly. We know that interpreting \texttt{f} must produce a function, because of its

256201type:

257202

258−\begin{SaveVerbatim}{appinterp}

259−

203+\begin{code}

260204interp env (App f s) = interp env f (interp env s)

261−

262−\end{SaveVerbatim}

263−\useverb{appinterp}

205+\end{code}

264206

265207\noindent

266208Operators and interpreters are, again, direct translations into the equivalent

@@ -268,39 +210,30 @@ Operators and interpreters are, again, direct translations into the equivalent

268210and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct

269211directly.

270212

271−\begin{SaveVerbatim}{opinterp}

272−

213+\begin{code}

273214interp env (Op op x y) = op (interp env x) (interp env y)

274215interp env (If x t e) = if interp env x then interp env t

275216 else interp env e

276−

277−\end{SaveVerbatim}

278−\useverb{opinterp}

217+\end{code}

279218

280219\noindent

281220We can make some simple test functions. Firstly, adding two inputs

282221\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:

283222

284−\begin{SaveVerbatim}{addtest}

285−

223+\begin{code}

286224add : Expr G (TyFun TyInt (TyFun TyInt TyInt))

287225add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))

288−

289−\end{SaveVerbatim}

290−\useverb{addtest}

226+\end{code}

291227

292228\noindent

293229More interestingly, we can write a factorial function. First, we write a \emph{lazy}

294230version of the \texttt{App} constructor, so that the recursive branch will only

295231be evaluated if necessary:

296232

297−\begin{SaveVerbatim}{lazyapp}

298−

233+\begin{code}

299234app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

300235app = \f, a => App f a

301−

302−\end{SaveVerbatim}

303−\useverb{lazyapp}

236+\end{code}

304237

305238\noindent

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

@@ -310,28 +243,22 @@ Then \texttt{fact}

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

311244is written as follows:

312245

313−\begin{SaveVerbatim}{facttest}

314−

246+\begin{code}

315247fact : Expr G (TyFun TyInt TyInt)

316248fact = Lam (If (Op (==) (Var stop) (Val 0))

317249 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))

318250 (Var stop)))

319−

320−\end{SaveVerbatim}

321−\useverb{facttest}

251+\end{code}

322252

323253To finish, we write a \texttt{main} program which interprets the factorial function

324254on user input:

325255

326−\begin{SaveVerbatim}{factmain}

327−

256+\begin{code}

328257main : IO ()

329258main = do putStr "Enter a number: "

330259 x <- getLine

331260 print (interp [] fact (cast x))

332−

333−\end{SaveVerbatim}

334−\useverb{factmain}

261+\end{code}

335262

336263\noindent

337264Here, \texttt{cast} is an overloaded function which converts a value from one

@@ -339,12 +266,11 @@ type to another if possible. Here, it converts a string to

339266an integer, giving 0 if the input is invalid. An example run of this program

340267at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

341268

342−\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}

343−

269+\begin{lstlisting}[caption={Running the well-typed interpreter}, label=factrun, escapechar=^]

344270$ idris interp.idr

345271 ____ __ _

346272 / _/___/ /____(_)____

347− / // __ / ___/ / ___/ Version ^version{}

273+ / // __ / ___/ / ___/ Version ^\version{}^

348274 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

349275 /___/\__,_/_/ /_/____/ Type :? for help

350276

@@ -353,22 +279,17 @@ Type checking ./interp.idr

353279Enter a number: 6

354280720

355281*interp>

356−

357−\end{SaveVerbatim}

358−\codefig{factrun}{Running the well-typed interpreter}

282+\end{lstlisting}

359283

360284\subsubsection*{Aside: \texttt{cast}}

361285

362286The prelude defines a type class \texttt{Cast} which allows conversion between

363287types:

364288

365−\begin{SaveVerbatim}{castclass}

366−

289+\begin{code}

367290class Cast from to where

368291 cast : from -> to

369−

370−\end{SaveVerbatim}

371−\useverb{castclass}

292+\end{code}

372293

373294\noindent

374295It is a \emph{multi-parameter} type class, defining the source type and object

@@ -381,34 +302,31 @@ they make sense.

381302

382303Recall the \texttt{so} data type:

383304

384−\useverb{sotype}

305+\begin{code}

306+data so : Bool -> Type where

307+ oh : so True

308+\end{code}

385309

386310\noindent

387311This requires its parameter to be a \texttt{True} value. One simple application of this

388312is to perform unit testing of functions at compile time. For example, we know that

389313\texttt{4! = 24} so we can set up a test case as follows:

390314

391−\begin{SaveVerbatim}{unitTestFac}

392−

315+\begin{code}

393316unitTestFac : so (interp [] fact 4 == 24)

394317unitTestFac = oh

395−

396−\end{SaveVerbatim}

397−\useverb{unitTestFac}

318+\end{code}

398319

399320\noindent

400321For the program to compile, the test case must pass. If we change \texttt{24} to \texttt{25},

401322say, we will get an error message like the following:

402323

403−\begin{SaveVerbatim}{unitTestErr}

404−

324+\begin{lstlisting}

405325Type checking ./interp.idr

406326interp.idr:64:Can't unify so True with so False

407327

408328Specifically:

409329 Can't unify True with False

410−

411−\end{SaveVerbatim}

412−\useverb{unitTestErr}

330+\end{lstlisting}

413331

414332

tutorial/intro.tex → tutorial/content/intro.texrenamed+2−5

@@ -35,12 +35,9 @@ concatenating two lists has the property that the resulting list's length is

3535the sum of the lengths of the two input lists. We can therefore give the following type

3636to the \texttt{app} function, which concatenates vectors:

3737

38−\begin{SaveVerbatim}{appendv}

39−

38+\begin{lstlisting}

4039app : Vect n a -> Vect m a -> Vect (n + m) a

41−

42−\end{SaveVerbatim}

43−\useverb{appendv}

40+\end{lstlisting}

4441

4542\noindent

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

tutorial/miscellany.tex → tutorial/content/miscellany.texrenamed+55−130

@@ -10,7 +10,9 @@ foreign function interface, type providers, code generation and the universe hie

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{vindeximpty}

13+\begin{code}

14+index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

15+\end{code}

1416

1517\noindent

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

@@ -18,17 +20,14 @@ by searching the context for an appropriate value, or constructing a proof. For

1820the following definition of \texttt{head} which requires a proof that the list is

1921non-empty

2022

21−\begin{SaveVerbatim}{safehead}

22−

23+\begin{code}

2324isCons : List a -> Bool

2425isCons [] = False

2526isCons (x :: xs) = True

2627

2728head : (xs : List a) -> (isCons xs = True) -> a

2829head (x :: xs) _ = x

29−

30−\end{SaveVerbatim}

31−\useverb{safehead}

30+\end{code}

3231

3332\noindent

3433If the list is statically known to be non-empty, either because its value is known or

@@ -36,13 +35,10 @@ because a proof already exists in the context, the proof can be constructed

3635automatically. Auto implicit arguments allow this to happen silently. We define

3736\texttt{head} as follows:

3837

39−\begin{SaveVerbatim}{headauto}

40−

38+\begin{code}

4139head : (xs : List a) -> {auto p : isCons xs = True} -> a

4240head (x :: xs) = x

43−

44−\end{SaveVerbatim}

45−\useverb{headauto}

41+\end{code}

4642

4743\noindent

4844The \texttt{auto} annotation on the implicit argument means that \Idris{} will

@@ -52,25 +48,19 @@ if a proof is not found.

5248Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof

5349is not found, it can be provided explicitly as normal:

5450

55−\begin{SaveVerbatim}{headapp}

56−

51+\begin{code}

5752head xs {p = ?headProof}

58−

59−\end{SaveVerbatim}

60−\useverb{headapp}

53+\end{code}

6154

6255\noindent

6356More generally, we can fill in implicit arguments with a default value by annotating

6457them with \texttt{default}. The definition above is equivalent to:

6558

66−\begin{SaveVerbatim}{defimp}

67−

59+\begin{code}

6860head : (xs : List a) ->

6961 {default proof { trivial; } p : isCons xs = True} -> a

7062head (x :: xs) = x

71−

72−\end{SaveVerbatim}

73−\useverb{defimp}

63+\end{code}

7464

7565\subsection{Implicit conversions}

7666

@@ -79,16 +69,13 @@ automatic conversion of values from one type to another when required to make

7969a term type correct. This is intended to increase convenience and reduce

8070verbosity. A contrived but simple example is the following:

8171

82−\begin{SaveVerbatim}{implicit}

83−

72+\begin{code}

8473implicit intString : Int -> String

8574intString = show

8675

8776test : Int -> String

8877test x = "Number " ++ x

89−

90−\end{SaveVerbatim}

91−\useverb{implicit}

78+\end{code}

9279

9380\noindent

9481In general, we cannot append an \texttt{Int} to a \texttt{String}, but the

@@ -111,17 +98,14 @@ extension of \texttt{.lidr} then it is assumed to be a literate file. In literat

11198programs, everything is assumed to be a comment unless the line begins with a

11299greater than sign \texttt{>}, for example:

113100

114−\begin{SaveVerbatim}{litidr}

115−

101+\begin{lstlisting}

116102> module literate

117103

118104This is a comment. The main program is below

119105

120106> main : IO ()

121107> main = putStrLn "Hello literate world!\n"

122−

123−\end{SaveVerbatim}

124−\useverb{litidr}

108+\end{lstlisting}

125109

126110\noindent

127111An additional restriction is that there must be a blank line between a program

@@ -137,12 +121,9 @@ as part of the prelude. For this, we assume a certain amount of knowledge of

137121C and the \texttt{gcc} compiler. First, we define a datatype which describes the external

138122types we can handle:

139123

140−\begin{SaveVerbatim}{foreignty}

141−

124+\begin{code}

143−

144−\end{SaveVerbatim}

145−\useverb{foreignty}

126+\end{code}

146127

147128\noindent

148129Each of these corresponds directly to a C type. Respectively: \texttt{int},

@@ -150,8 +131,7 @@ Each of these corresponds directly to a C type. Respectively: \texttt{int},

150131There is also a translation to a concrete \Idris{} type, described by the

151132following function:

152133

153−\begin{SaveVerbatim}{interpfty}

154−

134+\begin{code}

155135interpFTy : FTy -> Type

156136interpFTy FInt = Int

157137interpFTy FFloat = Float

@@ -159,62 +139,49 @@ interpFTy FChar = Char

159139interpFTy FString = String

160140interpFTy FPtr = Ptr

161141interpFTy FUnit = ()

162−

163−\end{SaveVerbatim}

164−\useverb{interpfty}

142+\end{code}

165143

166144\noindent

167145A foreign function is described by a list of input types and a return type, which

168146can then be converted to an \Idris{} type:

169147

170−\begin{SaveVerbatim}{ffunty}

171−

148+\begin{code}

172149ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

173−

174−\end{SaveVerbatim}

175−\useverb{ffunty}

150+\end{code}

176151

177152\noindent

178153A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an

179154\texttt{IO} type, for example:

180155

181−\begin{SaveVerbatim}{ftyex}

182−

156+\begin{lstlisting}

183157Idris> ForeignTy [FInt, FString] FString

184158Int -> String -> IO String : Type

185159

186160Idris> ForeignTy [FInt, FString] FUnit

187161Int -> String -> IO () : Type

188−

189−\end{SaveVerbatim}

190−\useverb{ftyex}

162+\end{lstlisting}

191163

192164\noindent

193165We build a call to a foreign function by giving the name of the function, a list of

194166argument types and the return type. The built in function \texttt{mkForeign}

195167converts this description to a function callable by \Idris{}

196168

197−\begin{SaveVerbatim}{mkForeign}

198−

169+\begin{code}

199170data Foreign : Type -> Type where

200171 FFun : String -> (xs:List FTy) -> (t:FTy) ->

201172 Foreign (ForeignTy xs t)

202173

203174mkForeign : Foreign x -> x

204−

205−\end{SaveVerbatim}

206−\useverb{mkForeign}

175+\end{code}

207176

208177\noindent

209178For example, the \texttt{putStr} function is implemented as follows, as a call to

210179an external function \texttt{putStr} defined in the run-time system:

211180

212−\begin{SaveVerbatim}{putStrex}

213−

181+\begin{code}

214182putStr : String -> IO ()

215183putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

216−\end{SaveVerbatim}

217−\useverb{putStrex}

184+\end{code}

218185

219186\subsubsection*{Include and linker directives}

220187

@@ -241,14 +208,11 @@ tested using the special REPL command \texttt{:x EXPR}, and C libraries can be

241208dynamically loaded in the interpreter by using the \texttt{:dynamic} command

242209or the \texttt{\%dynamic} directive. For example:

243210

244−\begin{SaveVerbatim}{xdynamic}

245−

211+\begin{lstlisting}

246212Idris> :dynamic libm.so

247213Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)

2482140.9995736030415051 : Float

249−

250−\end{SaveVerbatim}

251−\useverb{xdynamic}

215+\end{lstlisting}

252216

253217\subsection{Type Providers}

254218Idris type providers, inspired by F\#'s type providers, are a means of making

@@ -265,14 +229,10 @@ including as an index in types.

265229

266230Type providers are still an experimental extension. To enable the extension,

267231use the \texttt{\%language} directive:

268−\begin{SaveVerbatim}{languageProv}

269232

233+\begin{code}

270234%language TypeProviders

271−

272−\end{SaveVerbatim}

273−

274−\useverb{languageProv}

275−

235+\end{code}

276236

277237A provider \texttt{p} for some type \texttt{t} is simply an expression of type

278238\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type

@@ -282,8 +242,7 @@ reads a text file. If the file consists of the string \texttt{"Int"}, then the

282242type \texttt{Int} will be provided. Otherwise, it will provide the type

283243\texttt{Nat}.

284244

285−\begin{SaveVerbatim}{fromFile}

286−

245+\begin{code}

287246strToType : String -> Type

288247strToType "Int" = Int

289248strToType _ = Nat

@@ -291,21 +250,16 @@ strToType _ = Nat

291250fromFile : String -> IO (Provider Type)

292251fromFile fname = do str <- readFile fname

293252 return (Provide (strToType (trim str)))

294−

295−\end{SaveVerbatim}

296−\useverb{fromFile}

253+\end{code}

297254

298255We then use the \texttt{\%provide} directive:

299256

300−\begin{SaveVerbatim}{fromFileUse}

301−

257+\begin{code}

302258%provide (T1 : Type) with fromFile "theType"

303259

304260foo : T1

305261foo = 2

306−

307−\end{SaveVerbatim}

308−\useverb{fromFileUse}

262+\end{code}

309263

310264\noindent

311265If the file named \texttt{theType} consists of the word \texttt{Int}, then

@@ -317,13 +271,10 @@ then \texttt{T1} is defined as \texttt{t}. Otherwise, the result is an error.

317271

318272Our datatype \texttt{Provider t} has the following definition:

319273

320−\begin{SaveVerbatim}{providerdef}

321−

274+\begin{code}

322275data Provider a = Error String

323276 | Provide a

324−

325−\end{SaveVerbatim}

326−\useverb{providerdef}

277+\end{code}

327278

328279\noindent

329280We have already seen the \texttt{Provide} constructor. The \texttt{Error}

@@ -344,12 +295,9 @@ communicate with the \emph{JavaScript} ecosystem.

344295Code generation is split into two separate targets. To generate code that is

345296tailored for running in the browser issue the following command:

346297

347−\begin{SaveVerbatim}{jscodegen}

348−

298+\begin{lstlisting}[language=bash]

349299$ idris --codegen javascript hello.idr -o hello.js

350−

351−\end{SaveVerbatim}

352−\useverb{jscodegen}

300+\end{lstlisting}

353301

354302\noindent

355303The resulting file can be embedded into your HTML just like any other

@@ -359,14 +307,11 @@ The resulting file can be embedded into your HTML just like any other

359307Generating code for \emph{NodeJS} is slightly different. \Idris{} outputs

360308a \emph{JavaScript} file that can be directly executed via \texttt{node}.

361309

362−\begin{SaveVerbatim}{nodecodegen}

363−

310+\begin{lstlisting}[language=bash]

364311$ idris --codegen node hello.idr -o hello

365312$ ./hello

366313Hello world

367−

368−\end{SaveVerbatim}

369−\useverb{nodecodegen}

314+\end{lstlisting}

370315

371316\noindent

372317Take into consideration that the \emph{JavaScript} code generator is using

@@ -390,8 +335,7 @@ of \emph{JavaScript} code.

390335\noindent

391336One could use the primitive addition of \emph{JavaScript} like so:

392337

393−\begin{SaveVerbatim}{jsaddition}

394−

338+\begin{code}

395339module Main

396340

397341primPlus : Int -> Int -> IO Int

@@ -402,9 +346,7 @@ main = do

402346 a <- primPlus 1 1

403347 b <- primPlus 1 2

404348 print (a, b)

405−

406−\end{SaveVerbatim}

407−\useverb{jsaddition}

349+\end{code}

408350

409351\noindent

410352Notice that the \texttt{\%n} notation qualifies the position of the

@@ -416,14 +358,11 @@ instead.

416358Passing functions to a foreign function is very similar. Let's assume that

417359we want to call the following function from the \emph{JavaScript} world:

418360

419−\begin{SaveVerbatim}{jstwice}

420−

361+\begin{code}[language=c]

421362function twice(f, x) {

422363 return f(f(x));

423364}

424−

425−\end{SaveVerbatim}

426−\useverb{jstwice}

365+\end{code}

427366

428367\noindent

429368We obviously need to pass a function \texttt{f} here (we can infer it from

@@ -436,7 +375,7 @@ you give it something of type \texttt{FFunction}. The following example code

436375calls \texttt{twice} in \emph{JavaScript} and returns the result to our

437376\Idris{} program:

438377

439−\begin{SaveVerbatim}{jshof}

378+\begin{code}

440379module Main

441380

442381twice : (Int -> Int) -> Int -> IO Int

@@ -448,9 +387,7 @@ main : IO ()

448387main = do

449388 a <- twice (+1) 1

450389 print a

451−

452−\end{SaveVerbatim}

453−\useverb{jshof}

390+\end{code}

454391

455392\noindent

456393The program outputs \texttt{3}, just like we expected.

@@ -470,38 +407,29 @@ application written in \Idris{}.

470407Since values can appear in types and \emph{vice versa}, it is natural that types themselves

471408have types. For example:

472409

473−\begin{SaveVerbatim}{typetypes}

474−

410+\begin{lstlisting}

475411*universe> :t Nat

476412Nat : Type

477413*universe> :t Vect

478414Vect : Nat -> Type -> Type

479−

480−\end{SaveVerbatim}

481−\useverb{typetypes}

415+\end{lstlisting}

482416

483417\noindent

484418But what about the type of \texttt{Type}? If we ask \Idris{} it reports

485419

486−\begin{SaveVerbatim}{setset}

487−

420+\begin{lstlisting}

488421*universe> :t Type

489422Type : Type 1

490−

491−\end{SaveVerbatim}

492−\useverb{setset}

423+\end{lstlisting}

493424

494425\noindent

495426If \texttt{Type} were its own type, it would lead to an inconsitency

496427due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}

497428of types (or \emph{universes}):

498429

499−\begin{SaveVerbatim}{sethierarchy}

500−

430+\begin{code}

501431Type : Type 1 : Type 2 : Type 3 : ...

502−

503−\end{SaveVerbatim}

504−\useverb{sethierarchy}

432+\end{code}

505433

506434\noindent

507435Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that

@@ -511,16 +439,13 @@ constraints and reports an error if any inconsistencies are found. Ordinarily, a

511439programmer does not need to worry about this, but it does prevent (contrived)

512440programs such as the following:

513441

514−\begin{SaveVerbatim}{idid}

515−

442+\begin{code}

516443myid : (a : Type) -> a -> a

517444myid _ x = x

518445

519446idid : (a : Type) -> a -> a

520447idid = myid _ myid

521−

522−\end{SaveVerbatim}

523−\useverb{idid}

448+\end{code}

524449

525450\noindent

526451The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy

tutorial/modules.tex → tutorial/content/modules.texrenamed+20−50

@@ -10,8 +10,7 @@ tree type \texttt{BTree} (in a file \texttt{btree.idr}) and Figure

1010\ref{bstmain} gives a main program (in a file \texttt{bmain.idr} which uses the

1111\texttt{bst} module to sort a list.

1212

13−\begin{SaveVerbatim}{bstmod}

14−

13+\begin{code}[caption={Binary Tree module}, label=bstmod]

1514module btree

1615

1716data BTree a = Leaf

@@ -29,12 +28,9 @@ toList (Node l v r) = toList l ++ (v :: toList r)

2928toTree : Ord a => List a -> BTree a

3029toTree [] = Leaf

3130toTree (x :: xs) = insert x (toTree xs)

31+\end{code}

3232

33−\end{SaveVerbatim}

34−\codefig{bstmod}{Binary Tree module}

35−

36−\begin{SaveVerbatim}{bstmain}

37−

33+\begin{code}[caption={Binary Tree main program},label=bstmain]

3834module Main

3935

4036import btree

@@ -42,9 +38,7 @@ import btree

4238main : IO ()

4339main = do let t = toTree [1,8,2,7,9,3]

4440 print (toList t)

45−

46−\end{SaveVerbatim}

47−\codefig{bstmain}{Binary Tree main program}

41+\end{code}

4842

4943\noindent

5044The same names can be defined in multiple modules. This is possible because in practice names

@@ -96,8 +90,7 @@ to be \texttt{private}. For our \texttt{btree} module, it makes sense for the

9690tree data type and the functions to be exported as \texttt{abstract}, as we see in

9791Figure \ref{bstmodp}.

9892

99−\begin{SaveVerbatim}{bstmodp}

100−

93+\begin{code}[caption={Binary Tree module, with export modifiers}, label=bstmodp]

10194module btree

10295

10396abstract data BTree a = Leaf

@@ -118,20 +111,15 @@ abstract

118111toTree : Ord a => List a -> BTree a

119112toTree [] = Leaf

120113toTree (x :: xs) = insert x (toTree xs)

121−

122−\end{SaveVerbatim}

123−\codefig{bstmodp}{Binary Tree module, with export modifiers}

114+\end{code}

124115

125116\noindent

126117Finally, the default export mode can be changed with the \texttt{\%access} directive,

127118for example:

128119

129−\begin{SaveVerbatim}{access}

130−

120+\begin{code}

131121%access abstract

132−

133−\end{SaveVerbatim}

134−\useverb{access}

122+\end{code}

135123

136124\noindent

137125In this case, any function with no access modifier will be exported as \texttt{abstract},

@@ -143,8 +131,7 @@ Defining a module also defines a namespace implicitly. However, namespaces can a

143131be given \emph{explicitly}. This is most useful if you wish to overload names within

144132the same module:

145133

146−\begin{SaveVerbatim}{nsfoo}

147−

134+\begin{code}

148135module foo

149136

150137namespace x

@@ -154,78 +141,61 @@ namespace x

154141namespace y

155142 test : String -> String

156143 test x = x ++ x

157−

158−\end{SaveVerbatim}

159−\useverb{nsfoo}

144+\end{code}

160145

161146\noindent

162147This (admittedly contrived) module defines two functions with fully qualified names

163148\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their

164149types:

165150

166−\begin{SaveVerbatim}{usetest}

167−

151+\begin{lstlisting}

168152*foo> test 3

1691536 : Int

170154*foo> test "foo"

171155"foofoo" : String

172−

173−\end{SaveVerbatim}

174−\useverb{usetest}

156+\end{lstlisting}

175157

176158\subsection{Parameterised blocks}

177159

178160Groups of functions can be parameterised over a number of arguments using a

179161\texttt{parameters} declaration, for example:

180162

181−\begin{SaveVerbatim}{paramex}

182−

163+\begin{code}

183164parameters (x : Nat, y : Nat)

184165 addAll : Nat -> Nat

185166 addAll z = x + y + z

186−

187−\end{SaveVerbatim}

188−\useverb{paramex}

167+\end{code}

189168

190169\noindent

191170The effect of a \texttt{parameters} block is to add the declared parameters to every

192171function, type and data constructor within the block. Outside the block, the parameters

193172must be given explicitly:

194173

195−\begin{SaveVerbatim}{addall}

196−

174+\begin{lstlisting}

197175*params> :t addAll

198176addAll : Nat -> Nat -> Nat -> Nat

199−

200−\end{SaveVerbatim}

201−\useverb{addall}

177+\end{lstlisting}

202178

203179\noindent

204180Parameters blocks can be nested, and can also include data declarations, in

205181which case the parameters are added explicitly to all type and data

206182constructors. They may also be dependent types with implicit arguments:

207183

208−\begin{SaveVerbatim}{paramdata}

209−

184+\begin{code}

210185parameters (xs : Vect x a, y : Nat)

211186 data Vects : Type -> Type where

212187 MkVects : Vect a y -> Vects a

213188

214189 append : Vects a -> Vect (x + y) a

215190 append (MkVects ys) = xs ++ ys

216−

217−\end{SaveVerbatim}

218−\useverb{paramdata}

191+\end{code}

219192

220193\noindent

221194To use \texttt{Vects} or \texttt{append} outside the block, we must also

222195give the \texttt{xs} and \texttt{y} arguments. Here, we can use placeholders for

223196the values which can be inferred by the type checker:

224197

225−\begin{SaveVerbatim}{paramuse}

226−

198+\begin{lstlisting}

227199*params> show (append _ _ (MkVects [1,2,3] _ [4,5,6]))

228200"[1, 2, 3, 4, 5, 6]" : String

229−

230−\end{SaveVerbatim}

231−\useverb{paramuse}

201+\end{lstlisting}

tutorial/provisional.tex → tutorial/content/provisional.texrenamed+41−103

@@ -7,31 +7,25 @@ checker and the type of the program we have written will be different (in that

77they do not have the same normal form), but nevertheless provably equal. For

88example, recall the \texttt{parity} function:

10−\begin{SaveVerbatim}{pardecl}

11−

10+\begin{code}

1211data Parity : Nat -> Type where

1312 even : Parity (n + n)

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

1514

1615parity : (n:Nat) -> Parity n

17−

18−\end{SaveVerbatim}

19−\useverb{pardecl}

16+\end{code}

2017

2118\noindent

2219We'd like to implement this as follows:

2320

24−\begin{SaveVerbatim}{parfail}

25−

21+\begin{code}

2622parity : (n:Nat) -> Parity n

2723parity Z = even {n=Z}

2824parity (S Z) = odd {n=Z}

2925parity (S (S k)) with (parity k)

3026 parity (S (S (j + j))) | even = even {n=S j}

3127 parity (S (S (S (j + j)))) | odd = odd {n=S j}

32−

33−\end{SaveVerbatim}

34−\useverb{parfail}

28+\end{code}

3529

3630\noindent

3731This simply states that zero is even, one is odd, and recursively, the parity

@@ -40,13 +34,10 @@ Explicitly marking the value of \texttt{n} in

4034even and odd is necessary to help type inference. Unfortunately, the type

4135checker rejects this:

4236

43−\begin{SaveVerbatim}{parerror}

44−

37+\begin{code}

4538views.idr:12:Can't unify Parity (plus (S j) (S j)) with

4639Parity (S (S (plus j j)))

47−

48−\end{SaveVerbatim}

49−\useverb{parerror}

40+\end{code}

5041

5142\noindent

5243The type checker

@@ -54,8 +45,7 @@ is telling us that \texttt{(j+1)+(j+1)} and \texttt{2+j+j}

5445do not normalise to the same value.

5546This is because \texttt{plus} is defined by recursion on its first argument, and in the

5647second value, there is a successor symbol on the second argument, so this will

57−not help with reduction. These values are obviously equal --- how can we rewrite

58−the program to fix this problem?

48+not help with reduction. These values are obviously equal --- how can we rewrite the program to fix this problem?

5949

6050\subsection{Provisional definitions}

6151

@@ -76,17 +66,14 @@ except that they introduce the right hand side with a \texttt{?=} rathar than

7666\texttt{=}. We define

7767\texttt{parity} as follows:

7868

79−\begin{SaveVerbatim}{paritypro}

80−

69+\begin{code}

8170parity : (n:Nat) -> Parity n

8271parity Z = even {n=Z}

8372parity (S Z) = odd {n=Z}

8473parity (S (S k)) with (parity k)

8574 parity (S (S (j + j))) | even ?= even {n=S j}

8675 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

87−

88−\end{SaveVerbatim}

89−\useverb{paritypro}

76+\end{code}

9077

9178\noindent

9279When written in this form, instead of reporting a type error, \Idris{} will insert

@@ -94,29 +81,23 @@ a metavariable standing for a theorem which will correct the type error. \Idris{

9481tells us we have two proof obligations, with names generated from the module and

9582function names:

9683

97−\begin{SaveVerbatim}{prometas}

98−

84+\begin{lstlisting}

9985*views> :m

10086Global metavariables:

10187 [views.parity_lemma_2,views.parity_lemma_1]

102−

103−\end{SaveVerbatim}

104−\useverb{prometas}

88+\end{lstlisting}

10589

10690\noindent

10791The first of these has the following type:

10892

109−\begin{SaveVerbatim}{prolem1}

110−

93+\begin{lstlisting}

11194*views> :p views.parity_lemma_1

11295

11396---------------------------------- (views.parity_lemma_1) --------

11497{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))

11598

11699-views.parity_lemma_1>

117−

118−\end{SaveVerbatim}

119−\useverb{prolem1}

100+\end{lstlisting}

120101

121102\noindent

122103The two arguments are \texttt{j}, the variable in scope from the pattern match,

@@ -126,71 +107,55 @@ this value.

126107We can achieve this using the following theorem from

127108the prelude:

128109

129−\begin{SaveVerbatim}{plusnsm}

130−

110+\begin{code}

131111plusSuccRightSucc : (left : Nat) -> (right : Nat) ->

132112 S (left + right) = left + (S right)

133−

134−

135−\end{SaveVerbatim}

136−\useverb{plusnsm}

113+\end{code}

137114

138115\noindent

139116After applying \texttt{intro} twice, we have:

140117

141−\begin{SaveVerbatim}{prolemii}

142−

118+\begin{lstlisting}

143119-views.parity_lemma_1> intro

144120

145121 j : Nat

146122 value : Parity (S (plus j (S j)))

147123---------------------------------- (views.parity_lemma_1) --------

148124{hole2} : Parity (S (S (j + j)))

149−

150−\end{SaveVerbatim}

151−\useverb{prolemii}

125+\end{lstlisting}

152126

153127\noindent

154128We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.

155129

156−\begin{SaveVerbatim}{prolemcomp}

157−

130+\begin{lstlisting}

158131-views.parity_lemma_1> intro

159132

160133 j : Nat

161134 value : Parity (S (plus j (S j)))

162135---------------------------------- (views.parity_lemma_1) --------

163136{hole2} : Parity (S (S (plus j j)))

164−

165−\end{SaveVerbatim}

166−\useverb{prolemcomp}

137+\end{lstlisting}

167138

168139\noindent

169140Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,

170141to \texttt{j} and \texttt{j}, giving:

171142

172−\begin{SaveVerbatim}{prolemr}

173−

143+\begin{lstlisting}

174144-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)

175145

176146 j : Nat

177147 value : Parity (S (plus j (S j)))

178148---------------------------------- (views.parity_lemma_1) --------

179149{hole3} : Parity (S (plus j (S j)))

180−

181−\end{SaveVerbatim}

182−\useverb{prolemr}

150+\end{lstlisting}

183151

184152\noindent

185153\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:

186154

187−\begin{SaveVerbatim}{sym}

188−

155+\begin{lstlisting}

189156sym : l = r -> r = l

190157sym refl = refl

191−

192−\end{SaveVerbatim}

193−\useverb{sym}

158+\end{lstlisting}

194159

195160\noindent

196161We can complete this proof using the \texttt{trivial} tactic, which finds

@@ -201,13 +166,10 @@ We can now test the \texttt{natToBin} function from Section

201166\ref{sect:nattobin} at the prompt. 42 is 101010 in

202167binary. The binary digits are reversed:

203168

204−\begin{SaveVerbatim}{ntbtest}

205−

169+\begin{lstlisting}

206170*views> show (natToBin 42)

207171"[False, True, False, True, False, True]" : String

208−

209−\end{SaveVerbatim}

210−\useverb{ntbtest}

172+\end{lstlisting}

211173

212174

213175\subsection{Suspension of Disbelief}

@@ -222,28 +184,22 @@ something!

222184Therefore, \Idris{} provides a built-in coercion function, which allows you to use

223185a value of the incorrect types:

224186

225−\begin{SaveVerbatim}{believe}

226−

187+\begin{code}

227188believe_me : a -> b

228−

229−\end{SaveVerbatim}

230−\useverb{believe}

189+\end{code}

231190

232191\noindent

233192Obviously, this should be used with extreme caution. It is useful when prototyping, and

234193can also be appropriate when asserting properties of external code (perhaps in an

235194external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:

236195

237−\begin{SaveVerbatim}{pladodgy}

238−

196+\begin{lstlisting}

239197views.parity_lemma_2 = proof {

240198 intro;

241199 intro;

242200 exact believe_me value;

243201}

244−

245−\end{SaveVerbatim}

246−\useverb{pladodgy}

202+\end{lstlisting}

247203

248204\noindent

249205The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,

@@ -258,15 +214,12 @@ We begin by indexing binary numbers over their \texttt{Nat} equivalent. This is

258214pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this

259215case \texttt{Nat}):

260216

261−\begin{SaveVerbatim}{bindef}

262−

217+\begin{code}

263218data Binary : Nat -> Type where

264219 bEnd : Binary Z

265220 bO : Binary n -> Binary (n + n)

266221 bI : Binary n -> Binary (S (n + n))

267−

268−\end{SaveVerbatim}

269−\useverb{bindef}

222+\end{code}

270223

271224\noindent

272225\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit

@@ -278,69 +231,54 @@ the least significant bit at the front.

278231Now a function which converts a Nat to binary will state, in the type, that the

279232resulting binary number is a faithful representation of the original Nat:

280233

281−\begin{SaveVerbatim}{ntbty}

282−

234+\begin{code}

283235natToBin : (n:Nat) -> Binary n

284−

285−\end{SaveVerbatim}

286−\useverb{ntbty}

236+\end{code}

287237

288238\noindent

289239The \texttt{Parity} view makes the definition fairly simple --- halving the

290240number is effectively a right shift after all --- although we need to use a

291241provisional definition in the odd case:

292242

293−\begin{SaveVerbatim}{ntbdef}

294−

243+\begin{code}

295244natToBin : (n:Nat) -> Binary n

296245natToBin Z = bEnd

297246natToBin (S k) with (parity k)

298247 natToBin (S (j + j)) | even = bI (natToBin j)

299248 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

300−

301−\end{SaveVerbatim}

302−\useverb{ntbdef}

249+\end{code}

303250

304251\noindent

305252The problem with the odd case is the same as in the definition of \texttt{parity}, and

306253the proof proceeds in the same way:

307254

308−\begin{SaveVerbatim}{ntboddprf}

309−

255+\begin{code}

310256natToBin_lemma_1 = proof {

311257 intro;

312258 intro;

313259 rewrite sym (plusSuccRightSucc j j);

314260 trivial;

315261}

316−

317−\end{SaveVerbatim}

318−\useverb{ntboddprf}

262+\end{code}

319263

320264\noindent

321265To finish, we'll implement a main program which reads an integer from the user and

322266outputs it in binary.

323267

324−\begin{SaveVerbatim}{binmain}

325−

268+\begin{code}

326269main : IO ()

327270main = do putStr "Enter a number: "

328271 x <- getLine

329272 print (natToBin (fromInteger (cast x)))

330−

331−\end{SaveVerbatim}

332−\useverb{binmain}

273+\end{code}

333274

334275\noindent

335276For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:

336277

337−\begin{SaveVerbatim}{showbin}

338−

278+\begin{code}

339279instance Show (Binary n) where

340280 show (bO x) = show x ++ "0"

341281 show (bI x) = show x ++ "1"

342282 show bEnd = ""

343−

344−\end{SaveVerbatim}

345−\useverb{showbin}

283+\end{code}

346284

tutorial/starting.tex → tutorial/content/starting.texrenamed+15−35

@@ -16,12 +16,9 @@ all major Linux distributions.

1616

1717The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:

1818

19−\begin{SaveVerbatim}{install}

20−

19+\begin{lstlisting}[language=bash]

2120cabal update; cabal install idris

22−

23−\end{SaveVerbatim}

24−\useverb{install}

21+\end{lstlisting}

2522

2623\noindent

2724This will install the latest version released on Hackage, along with any dependencies.

@@ -33,15 +30,12 @@ To check that installation has succeeded, and to write your first \Idris{}

3330program, create a file called ``\texttt{hello.idr}'' containing the following

3431text:

3532

36−\begin{SaveVerbatim}{hello}

37−

33+\begin{code}

3834module Main

3935

4036main : IO ()

4137main = putStrLn "Hello world"

42−

43−\end{SaveVerbatim}

44−\useverb{hello}

38+\end{code}

4539

4640\noindent

4741If you are familiar with Haskell, it should be fairly clear what the program is doing

@@ -49,14 +43,11 @@ and how it works, but if not, we will explain the details later.

4943You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}

5044at the shell prompt. This will create an executable called \texttt{hello}, which you can run:

5145

52−\begin{SaveVerbatim}{hello}

53−

46+\begin{lstlisting}[language=bash]

5447$ idris hello.idr -o hello

5548$ ./hello

5649Hello world

57−

58−\end{SaveVerbatim}

59−\useverb{hello}

50+\end{lstlisting}

6051

6152\noindent

6253Note that the \texttt{\$} indicates the shell prompt! Some useful options to the

@@ -74,21 +65,16 @@ interactive environment.

7465Entering \texttt{idris} at the shell prompt starts up the interactive

7566environment. You should see something like the following:

7667

77−\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}

78−

68+\begin{lstlisting}[escapechar=^]

7969$ idris

8070 ____ __ _

8171 / _/___/ /____(_)____

82− / // __ / ___/ / ___/ Version ^version{}

72+ / // __ / ___/ / ___/ Version ^\version{}^

8373 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

8474 /___/\__,_/_/ /_/____/ Type :? for help

8575

8676Idris>

87−

88−\end{SaveVerbatim}

89−%$

90−

91−\useverb{prompt1}

77+\end{lstlisting}

9278

9379\noindent

9480This gives a \texttt{ghci}-style interface which allows evaluation of expressions,

@@ -98,8 +84,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which

9884\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then

9985the program is compiled to the executable \texttt{hello}.

10086

101−\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}

102−Idris version \version{}

87+\begin{lstlisting}[caption={Interactive environment commands}, label=cmds, escapechar=^]

88+Idris version ^\version{}^

10389--------------------

10490

10591 Command Arguments Purpose

@@ -132,16 +118,13 @@ Idris version \version{}

132118 :unset <option> Unset an option

133119 :colour :color <option> Turn REPL colours on or off; set a specific colour

134120 :q :quit Exit the Idris system

135−\end{SaveVerbatim}

136−\codefigs{cmds}{Interactive environment commands}

137−

138−

139−\begin{SaveVerbatim}[commandchars=^\{\}]{run1}

121+\end{lstlisting}

140122

123+\begin{lstlisting}[caption={Sample Interactive Run}, label=run1, escapechar=^]

141124$ idris hello.idr

142125 ____ __ _

143126 / _/___/ /____(_)____

144− / // __ / ___/ / ___/ Version ^version{}

127+ / // __ / ___/ / ___/ Version ^\version{}^

145128 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

146129 /___/\__,_/_/ /_/____/ Type :? for help

147130

@@ -153,10 +136,7 @@ main : IO ()

153136Bye bye

154137$ ./hello

155138Hello world

156−

157−\end{SaveVerbatim}

158−

159−\codefig{run1}{Sample interactive run}

139+\end{lstlisting}

160140

161141\noindent

162142Type checking a file, if successful, creates a bytecode version of the file (in

tutorial/syntax.tex → tutorial/content/syntax.texrenamed+13−31

@@ -11,24 +11,18 @@ rules and \texttt{dsl} notation.

1111We have seen \texttt{if...then...else} expressions, but these

1212are not built in --- instead, we define a function in the prelude\ldots

1313

14−\begin{SaveVerbatim}{boolelim}

15−

14+\begin{code}

1615boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;

1716boolElim True t e = t;

1817boolElim False t e = e;

19−

20−\end{SaveVerbatim}

21−\useverb{boolelim}

18+\end{code}

2219

2320\noindent

2421\ldots and extend the core syntax with a \texttt{syntax} declaration:

2522

26−\begin{SaveVerbatim}{syntaxif}

27−

23+\begin{code}

2824syntax if [test] then [t] else [e] = boolElim test t e;

29−

30−\end{SaveVerbatim}

31−\useverb{syntaxif}

25+\end{code}

3226

3327\noindent

3428The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right

@@ -56,15 +50,12 @@ constants, or bracketed expressions). Rules can use previously defined rules,

5650but may not be recursive. The following syntax extensions would therefore be

5751valid:

5852

59−\begin{SaveVerbatim}{syntaxex}

60−

53+\begin{code}

6154syntax [var] ":=" [val] = Assign var val;

6255syntax [test] "?" [t] ":" [e] = if test then t else e;

6356syntax select [x] from [t] where [w] = SelectWhere x t w;

6457syntax select [x] from [t] = Select x t;

65−

66−\end{SaveVerbatim}

67−\useverb{syntaxex}

58+\end{code}

6859

6960\noindent

7061Syntax macros can be further restricted to apply only in patterns (i.e., only on the left

@@ -73,26 +64,20 @@ of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term}

7364rules. For example, we might define an interval as follows, with a static check

7465that the lower bound is below the upper bound using \texttt{so}:

7566

76−\begin{SaveVerbatim}{interval}

77−

67+\begin{code}

7868data Interval : Type where

7969 MkInterval : (lower : Float) -> (upper : Float) ->

8070 so (lower < upper) -> Interval

81−

82−\end{SaveVerbatim}

83−\useverb{interval}

71+\end{code}

8472

8573\noindent

8674We can define a syntax which, in patterns, always matches \texttt{oh} for the proof

8775argument, and in terms requires a proof term to be provided:

8876

89−\begin{SaveVerbatim}{intervalsyn}

90−

77+\begin{code}

9178pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh

9279term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma

93−

94−\end{SaveVerbatim}

95−\useverb{intervalsyn}

80+\end{code}

9681

9782\noindent

9883In terms, the syntax \texttt{[x...y]} will generate a proof obligation

@@ -101,22 +86,19 @@ In terms, the syntax \texttt{[x...y]} will generate a proof obligation

10186Finally, syntax rules may be used to introduce alternative binding forms. For

10287exampe, a \texttt{for} loop binds a variable on each iteration:

10388

104−\begin{SaveVerbatim}{forloop}

105−

89+\begin{code}

10690syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

10791

10892main : IO ()

10993main = do for x in [1..10]:

11094 putStrLn ("Number " ++ show x)

11195 putStrLn "Done!"

112−

113−\end{SaveVerbatim}

114−\useverb{forloop}

96+\end{code}

11597

11698\noindent

11799Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents

118100a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in

119101quotation marks since it is already a reserved word.

120102

121−\input{dsl}

103+\input{./content/dsl}

122104

tutorial/theorems.tex → tutorial/content/theorems.texrenamed+53−131

@@ -6,28 +6,22 @@

66programs to be stated and proved. Equality is built in, but conceptually has

77the following definition:

9−\begin{SaveVerbatim}{}

10−

9+\begin{code}

1110data (=) : a -> b -> Type where

1211 refl : x = x

13−

14−\end{SaveVerbatim}

15−\useverb{}

12+\end{code}

1613

1714\noindent

1815Equalities can be proposed between any values of any types, but the only way to

1916construct a proof of equality is if values actually are equal. For example:

2017

21−\begin{SaveVerbatim}{eqprf}

22−

18+\begin{code}

2319fiveIsFive : 5 = 5

2420fiveIsFive = refl

2521

2622twoPlusTwo : 2 + 2 = 4

2723twoPlusTwo = refl

28−

29−\end{SaveVerbatim}

30−\useverb{eqprf}

24+\end{code}

3125

3226\subsection{The Empty Type}

3327

@@ -40,46 +34,36 @@ without using a partially defined or general recursive function (see Section

4034to prove that something is impossible, for example zero is never equal

4135to a successor:

4236

43−\begin{SaveVerbatim}{natdisjoint}

44−

37+\begin{code}

4538disjoint : (n : Nat) -> Z = S n -> _|_

4639disjoint n p = replace {P = disjointTy} p ()

4740 where

4841 disjointTy : Nat -> Type

4942 disjointTy Z = ()

5043 disjointTy (S k) = _|_

51−

52−\end{SaveVerbatim}

53−\useverb{natdisjoint}

44+\end{code}

5445

5546\noindent

5647There is no need to worry too much about how this function works --- essentially,

5748it applies the library function \texttt{replace}, which uses an equality proof to

5849transform a predicate. Here we use it to transform a value of a type which can exist,

59−the empty tuple, to a value of a type which can't, by using a proof of something

60−which can't exist.

50+the empty tuple, to a value of a type which can't, by using a proof of something which can't exist.

6151

6252Once we have an element of the empty type, we can prove anything. \texttt{FalseElim}

6353is defined in the library, to assist with proofs by contradiction.

6454

65−\begin{SaveVerbatim}{falseelim}

66−

55+\begin{code}

6756FalseElim : _|_ -> a

68−

69−\end{SaveVerbatim}

70−\useverb{falseelim}

57+\end{code}

7158

7259\subsection{Simple Theorems}

7360

7461When type checking dependent types, the type itself gets \emph{normalised}. So imagine

7562we want to prove the following theorem about the reduction behaviour of \texttt{plus}:

7663

77−\begin{SaveVerbatim}{plusred}

78−

64+\begin{code}

7965plusReduces : (n:Nat) -> plus Z n = n

80−

81−\end{SaveVerbatim}

82−\useverb{plusred}

66+\end{code}

8367

8468\noindent

8569We've written down the statement of the theorem as a type, in just the same way

@@ -93,49 +77,37 @@ correspondence~\cite{howard} explains this relationship.

9377The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n}

9478by the definition of \texttt{plus}:

9579

96−\begin{SaveVerbatim}{plusredp}

97−

80+\begin{code}

9881plusReduces n = refl

99−

100−\end{SaveVerbatim}

101−\useverb{plusredp}

82+\end{code}

10283

10384\noindent

10485It is slightly harder if we try the arguments the other way, because plus is

10586defined by recursion on its first argument. The proof also works by recursion

10687on the first argument to \texttt{plus}, namely \texttt{n}.

10788

108−\begin{SaveVerbatim}{plusRedO}

109−

89+\begin{code}

11090plusReducesZ : (n:Nat) -> n = plus n Z

11191plusReducesZ Z = refl

11292plusReducesZ (S k) = cong (plusReducesZ k)

113−

114−\end{SaveVerbatim}

115−\useverb{plusRedO}

93+\end{code}

11694

11795\noindent

11896\texttt{cong} is a function defined in the library which states that

11997equality respects function application:

12098

121−\begin{SaveVerbatim}{resps}

122−

99+\begin{code}

123100cong : {f : t -> u} -> a = b -> f a = f b

124−

125−\end{SaveVerbatim}

126−\useverb{resps}

101+\end{code}

127102

128103\noindent

129104We can do the same for the reduction behaviour of plus on successors:

130105

131−\begin{SaveVerbatim}{plusRedS}

132−

106+\begin{code}

133107plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

134108plusReducesS Z m = refl

135109plusReducesS (S k) m = cong (plusReducesS k m)

136−

137−\end{SaveVerbatim}

138−\useverb{plusRedS}

110+\end{code}

139111

140112\noindent

141113Even for trival theorems like these, the proofs are a little tricky to

@@ -152,15 +124,12 @@ the proof by \emph{induction}, so we write the cases for \texttt{Z} and

152124\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive

153125hypothesis, and insert \emph{metavariables} for the rest of the definition:

154126

155−\begin{SaveVerbatim}{prOstruct}

156−

127+\begin{code}

157128plusReducesZ' : (n:Nat) -> n = plus n Z

158129plusReducesZ' Z = ?plusredZ_Z

159130plusReducesZ' (S k) = let ih = plusReducesZ' k in

160131 ?plusredZ_S

161−

162−\end{SaveVerbatim}

163−\useverb{prOstruct}

132+\end{code}

164133

165134\noindent

166135On running \Idris{}, two global names are created, \texttt{plusredZ\_O} and

@@ -169,40 +138,31 @@ at the prompt to find out which metavariables are still to be solved (or, more

169138precisely, which functions exist but have no definitions), then the

170139\texttt{:t} command to see their types:

171140

172−\begin{SaveVerbatim}{showmetas}

173−

141+\begin{lstlisting}

174142*theorems> :m

175143Global metavariables:

176144 [plusredZ_S,plusredZ_Z]

177145

178−\end{SaveVerbatim}

179−

180−\begin{SaveVerbatim}{metatypes}

146+\end{lstlisting}

181147

148+\begin{lstlisting}

182149*theorems> :t plusredZ_Z

183150plusredZ_Z : Z = plus Z Z

184151

185152*theorems> :t plusredZ_S

186153plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z

187−

188−\end{SaveVerbatim}

189−\useverb{showmetas}

190−

191−\useverb{metatypes}

154+\end{lstlisting}

192155

193156\noindent

194157The \texttt{:p} command enters interactive proof mode, which can be used to complete

195158the missing definitions.

196159

197−\begin{SaveVerbatim}{proveO}

198−

160+\begin{lstlisting}

199161*theorems> :p plusredZ_Z

200162

201163---------------------------------- (plusredZ_Z) --------

202164{hole0} : Z = plus Z Z

203−

204−\end{SaveVerbatim}

205−\useverb{proveO}

165+\end{lstlisting}

206166

207167\noindent

208168This gives us a list of premisses

@@ -211,15 +171,12 @@ named \texttt{\{hole0\}} here).

211171At the prompt we can enter tactics to direct the construction of the proof. In this case,

212172we can normalise the goal with the \texttt{compute} tactic:

213173

214−\begin{SaveVerbatim}{compute}

215−

174+\begin{lstlisting}

216175-plusredZ_Z> compute

217176

218177---------------------------------- (plusredZ_Z) --------

219178{hole0} : Z = Z

220−

221−\end{SaveVerbatim}

222−\useverb{compute}

179+\end{lstlisting}

223180

224181\noindent

225182Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by

@@ -227,13 +184,10 @@ Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove b

227184which introduces subgoals for each of the function's explicit arguments (\texttt{refl}

228185has none):

229186

230−\begin{SaveVerbatim}{refrefl}

231−

187+\begin{lstlisting}

232188-plusredZ_Z> refine refl

233189plusredZ_Z: no more goals

234−

235−\end{SaveVerbatim}

236−\useverb{refrefl}

190+\end{lstlisting}

237191

238192\noindent

239193Here, we could also have used the \texttt{trivial} tactic, which tries to refine by

@@ -242,40 +196,31 @@ When a proof is complete, we use the \texttt{qed} tactic to add the proof to the

242196global context, and remove the metavariable from the unsolved metavariables list.

243197This also outputs a trace of the proof:

244198

245−\begin{SaveVerbatim}{prOprooftrace}

246−

199+\begin{code}

247200-plusredZ_Z> qed

248201plusredZ_Z = proof {

249202 compute;

250203 refine refl;

251204}

205+\end{code}

252206

253−\end{SaveVerbatim}

254−\useverb{prOprooftrace}

255−

256−\begin{SaveVerbatim}{showmetasO}

257−

207+\begin{lstlisting}

258208*theorems> :m

259209Global metavariables:

260210 [plusredZ_S]

261−

262−\end{SaveVerbatim}

263−\useverb{showmetasO}

211+\end{lstlisting}

264212

265213\noindent

266214The \texttt{:addproof} command, at the interactive prompt, will add the proof to

267215the source file (effectively in an appendix).

268216Let us now prove the other required lemma, \texttt{plusredZ\_S}:

269217

270−\begin{SaveVerbatim}{plusredZSprf}

271−

218+\begin{lstlisting}

272219*theorems> :p plusredZ_S

273220

274221---------------------------------- (plusredZ_S) --------

275222{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z

276−

277−\end{SaveVerbatim}

278−\useverb{plusredZSprf}

223+\end{lstlisting}

279224

280225\noindent

281226In this case, the goal is a function type, using \texttt{k} (the argument accessible by

@@ -283,37 +228,31 @@ pattern matching) and \texttt{ih} (the local variable containing the result of

283228the recursive call). We can introduce these as premisses using the \texttt{intro} tactic

284229twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:

285230

286−\begin{SaveVerbatim}{prSintros}

287−

231+\begin{lstlisting}

288232 k : Nat

289233 ih : k = plus k Z

290234---------------------------------- (plusredZ_S) --------

291235{hole2} : S k = plus (S k) Z

292−

293−\end{SaveVerbatim}

294−\useverb{prSintros}

236+\end{lstlisting}

295237

296238\noindent

297239Since plus is defined is defined by recursion on its first argument, the term

298240\texttt{plus (S k) Z} in the goal can be simplified, so we use

299241\texttt{compute}.

300242

301−\begin{SaveVerbatim}{prScompute}

243+\begin{lstlisting}

302244 k : Nat

303245 ih : k = plus k Z

304246---------------------------------- (plusredZ_S) --------

305247{hole2} : S k = S (plus k Z)

306−

307−\end{SaveVerbatim}

308−\useverb{prScompute}

248+\end{lstlisting}

309249

310250\noindent

311251We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to

312252use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can

313253achieve this with the \texttt{rewrite} tactic:

314254

315−\begin{SaveVerbatim}{}

316−

255+\begin{lstlisting}

317256-plusredZ_S> rewrite ih

318257

319258 k : Nat

@@ -322,16 +261,13 @@ achieve this with the \texttt{rewrite} tactic:

322261{hole3} : S k = S k

323262

324263-plusredZ_S>

325−

326−\end{SaveVerbatim}

327−\useverb{}

264+\end{lstlisting}

328265

329266\noindent

330267The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite

331268the goal using that proof. Here, it results in an equality which is trivially provable:

332269

333−\begin{SaveVerbatim}{prOStrace}

334−

270+\begin{lstlisting}

335271-plusredZ_S> trivial

336272plusredZ_S: no more goals

337273-plusredZ_S> qed

@@ -340,9 +276,7 @@ plusredZ_S = proof {

340276 rewrite ih;

341277 trivial;

342278}

343−

344−\end{SaveVerbatim}

345−\useverb{prOStrace}

279+\end{lstlisting}

346280

347281\noindent

348282Again, we can add this proof to the end of our source file using the \texttt{:addproof}

@@ -357,8 +291,7 @@ If we really want to trust our proofs, it is important that they are defined by

357291possible inputs and is guaranteed to terminate. Otherwise we could construct an

358292element of the empty type, from which we could prove anything:

359293

360−\begin{SaveVerbatim}{empties}

361−

294+\begin{code}

362295-- making use of 'hd' being partially defined

363296empty1 : _|_

364297empty1 = hd [] where

@@ -368,25 +301,20 @@ empty1 = hd [] where

368301-- not terminating

369302empty2 : _|_

370303empty2 = empty2

371−

372−\end{SaveVerbatim}

373−\useverb{empties}

304+\end{code}

374305

375306\noindent

376307Internally, \Idris{} checks every definition for totality, and we can check at

377308the prompt with the \texttt{:total} command. We see that neither of the above

378309definitions is total:

379310

380−\begin{SaveVerbatim}{totalcheck}

381−

311+\begin{lstlisting}

382312*theorems> :total empty1

383313possibly not total due to: empty1#hd

384314 not total as there are missing cases

385315*theorems> :total empty2

386316possibly not total due to recursive path empty2

387−

388−\end{SaveVerbatim}

389−\useverb{totalcheck}

317+\end{lstlisting}

390318

391319\noindent

392320Note the use of the word ``possibly'' --- a totality check can, of course,

@@ -395,28 +323,22 @@ is, therefore, conservative. It is also possible (and indeed advisable, in the

395323case of proofs) to mark functions as total so that it will be a compile time

396324error for the totality check to fail:

397325

398−\begin{SaveVerbatim}{emptyfail}

399−

326+\begin{lstlisting}

400327total empty2 : _|_

401328empty2 = empty2

402329

403330Type checking ./theorems.idr

404331theorems.idr:25:empty2 is possibly not total due to recursive path empty2

405−

406−\end{SaveVerbatim}

407−\useverb{emptyfail}

332+\end{lstlisting}

408333

409334\noindent

410335Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors

411336are disjoint is total:

412337

413−\begin{SaveVerbatim}{totdisjoint}

414−

338+\begin{lstlisting}

415339*theorems> :total disjoint

416340Total

417−

418−\end{SaveVerbatim}

419−\useverb{totdisjoint}

341+\end{lstlisting}

420342

421343\noindent

422344The totality check is, necessarily, conservative. To be recorded as total, a

tutorial/typesfuns.tex → tutorial/content/typesfuns.texrenamed+142−305

@@ -11,8 +11,7 @@ We can declare some constants with these types. Enter the following

1111into a file \texttt{prims.idr} and load it into the \Idris{} interactive

1212environment by typing \texttt{idris prims.idr}:

1313

14−\begin{SaveVerbatim}{constprims}

15−

14+\begin{code}

1615module prims

1716

1817x : Int

@@ -26,9 +25,7 @@ bar = 'Z'

2625

2726quux : Bool

2827quux = False

29−

30−\end{SaveVerbatim}

31−\useverb{constprims}

28+\end{code}

3229

3330\noindent

3431An \Idris{} file consists of an optional module declaration (here

@@ -50,15 +47,12 @@ functions. The prelude defines several arithmetic and comparison operators,

5047which we can use at the prompt. Evaluating things at the prompt gives an

5148answer, and the type of the answer. For example:

5249

53−\begin{SaveVerbatim}{promptprim}

54−

50+\begin{lstlisting}

5551*prims> 6*6+6

565242 : Int

5753*prims> x == 6*6+6

5854True : Bool

59−

60−\end{SaveVerbatim}

61−\useverb{promptprim}

55+\end{lstlisting}

6256

6357\noindent

6458All of the usual arithmetic and comparison operators are defined for the primitive

@@ -66,27 +60,21 @@ types. They are overloaded using type classes, as we will discuss in Section

6660\ref{sec:classes} and can be extended to work on user defined types.

6761Boolean expressions can be tested with the \texttt{if...then...else} construct:

6862

69−\begin{SaveVerbatim}{ifthenelse}

70−

63+\begin{lstlisting}

7164*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"

7265"The answer!" : String

73−

74−\end{SaveVerbatim}

75−\useverb{ifthenelse}

66+\end{lstlisting}

7667

7768\subsection{Data Types}

7869

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

8071syntax. Natural numbers and lists, for example, can be declared as follows:

8172

82−\begin{SaveVerbatim}{natlist}

83−

73+\begin{code}

8474data Nat = Z | S Nat -- Natural numbers

8575 -- (zero and successor)

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

87−

88−\end{SaveVerbatim}

89−\useverb{natlist}

77+\end{code}

9078

9179\noindent

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

@@ -97,28 +85,18 @@ or a value added to the front of another list (\texttt{x :: xs}).

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

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

9987

100−\begin{SaveVerbatim}{infixcons}

101−

88+\begin{code}

10289infixr 10 ::

103−

104−\end{SaveVerbatim}

105−\useverb{infixcons}

90+\end{code}

10691

10792\noindent

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

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

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

11196

112−\begin{SaveVerbatim}{infixsyms}

113−

97+\begin{lstlisting}

11498:+-*/=_.?|&><!@$%^~.

115−

116−\end{SaveVerbatim}

117−\useverb{infixsyms}

118−

119−\begin{SaveVerbatim}{argh}

120−$

121−\end{SaveVerbatim}

99+\end{lstlisting}

122100

123101\subsection{Functions}

124102

@@ -128,8 +106,7 @@ functions, using a single colon \texttt{:} (rather than

128106Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be

129107defined as follows, again taken from the standard library:

130108

131−\begin{SaveVerbatim}{natfns}

132−

109+\begin{code}

133110-- Unary addition

134111plus : Nat -> Nat -> Nat

135112plus Z y = y

@@ -139,9 +116,7 @@ plus (S k) y = S (plus k y)

139116mult : Nat -> Nat -> Nat

140117mult Z y = Z

141118mult (S k) y = plus y (mult k y)

142−

143−\end{SaveVerbatim}

144−\useverb{natfns}

119+\end{code}

145120

146121\noindent

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

@@ -154,29 +129,23 @@ all part of the same namespace.

154129

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

156131

157−\begin{SaveVerbatim}{fntest}

158−

132+\begin{lstlisting}

159133Idris> plus (S (S Z)) (S (S Z))

160134S (S (S (S Z))) : Nat

161135Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))

162136S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat

163−

164−\end{SaveVerbatim}

165−\useverb{fntest}

137+\end{lstlisting}

166138

167139\noindent

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

169141meaning that we can also test the functions as follows:

170142

171−\begin{SaveVerbatim}{fntest}

172−

143+\begin{lstlisting}

173144Idris> plus 2 2

174145S (S (S (S Z))) : Nat

175146Idris> mult 3 (plus 2 2)

176147S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat

177−

178−\end{SaveVerbatim}

179−\useverb{fntest}

148+\end{lstlisting}

180149

181150\noindent

182151You may wonder, by the way, why we have unary natural numbers when our

@@ -194,16 +163,13 @@ Functions can also be defined \emph{locally} using \texttt{where} clauses. For e

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

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

196165

197−\begin{SaveVerbatim}{revwhere}

198−

166+\begin{code}

199167reverse : List a -> List a

200168reverse xs = revAcc [] xs where

201169 revAcc : List a -> List a -> List a

202170 revAcc acc [] = acc

203171 revAcc acc (x :: xs) = revAcc (x :: acc) xs

204−

205−\end{SaveVerbatim}

206−\useverb{revwhere}

172+\end{code}

207173

208174\noindent

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

@@ -220,8 +186,7 @@ As well as functions, \texttt{where} blocks can include local data

220186declarations, such as the following where \texttt{MyLT} is not accessible outside

221187the definition of \texttt{foo}:

222188

223−\begin{SaveVerbatim}{wheredata}

224−

189+\begin{code}

225190foo : Int -> Int

226191foo x = case isLT of

227192 Yes => x*2

@@ -231,9 +196,7 @@ foo x = case isLT of

231196

232197 isLT : MyLT

233198 isLT = if x < 20 then Yes else No

234−

235−\end{SaveVerbatim}

236−\useverb{wheredata}

199+\end{code}

237200

238201\noindent

239202In general, functions defined in a \texttt{where} clause need a type declaration

@@ -249,8 +212,7 @@ application

249212\noindent

250213So, for example, the following definitions are legal:

251214

252−\begin{SaveVerbatim}{whereinfer}

253−

215+\begin{code}

254216even : Nat -> Bool

255217even Z = True

256218even (S k) = odd k where

@@ -262,10 +224,7 @@ test = [c (S 1), c Z, d (S Z)]

262224 where c x = 42 + x

263225 d y = c (y + 1 + z y)

264226 where z w = y + w

265−

266−\end{SaveVerbatim}

267−\useverb{whereinfer}

268−

227+\end{code}

269228

270229\subsection{Dependent Types}

271230

@@ -276,14 +235,11 @@ conventionally called vectors in the dependent type literature. In \Idris{},

276235we declare vectors as follows\footnote{Note that prior to \Idris{} 0.9.9,

277236the order of the arguments to \texttt{Vect} was reversed.}:

278237

279−\begin{SaveVerbatim}{vect}

280−

238+\begin{code}

281239data Vect : Nat -> Type -> Type where

282240 Nil : Vect Z a

283241 (::) : a -> Vect k a -> Vect (S k) a

284−

285−\end{SaveVerbatim}

286−\useverb{vect}

242+\end{code}

287243

288244\noindent

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

@@ -308,42 +264,31 @@ The type of a function over \tTC{Vect} will describe what happens to the

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

309265library, appends two \tTC{Vect}s:

310266

311−\begin{SaveVerbatim}{vapp}

312−

267+\begin{code}

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

314269(++) Nil ys = ys

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

316−

317−\end{SaveVerbatim}

318−\useverb{vapp}

271+\end{code}

319272

320273\noindent

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

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

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

324277

325−\begin{SaveVerbatim}{vapperr}

326−

278+\begin{code}

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

328280(++) Nil ys = ys

329281(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

282+\end{code}

330283

331−\end{SaveVerbatim}

332−\useverb{vapperr}

333−

334−\begin{SaveVerbatim}{vapperrmsg}

335−

284+\begin{lstlisting}

336285$ idris vbroken.idr --check

337286vbroken.idr:3:Can't unify Vect n a with Vect m a

338287

339288Specifically:

340289 Can't unify n with m

290+\end{lstlisting}

341291

342−\end{SaveVerbatim}

343−\begin{SaveVerbatim}{bleh}

344−$

345−\end{SaveVerbatim}

346−\useverb{vapperrmsg}

347292

348293\noindent

349294This error message suggests that there is a length mismatch between two vectors

@@ -357,14 +302,11 @@ of length \texttt{n}.

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

358303They are declared as follows (again, in the prelude):

359304

360−\begin{SaveVerbatim}{findecl}

361−

305+\begin{code}

362306data Fin : Nat -> Type where

363307 fZ : Fin (S k)

364308 fS : Fin k -> Fin (S k)

365−

366−\end{SaveVerbatim}

367−\useverb{findecl}

309+\end{code}

368310

369311\noindent

370312\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements;

@@ -382,14 +324,11 @@ numbers bounded by \tTC{n}.

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

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

384326

385−\begin{SaveVerbatim}{vindex}

386−

327+\begin{code}

387328index : Fin n -> Vect n a -> a

388329index fZ (x :: xs) = x

389330index (fS k) (x :: xs) = index k xs

390−

391−\end{SaveVerbatim}

392−\useverb{vindex}

331+\end{code}

393332

394333\noindent

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

@@ -407,12 +346,9 @@ since it would force \texttt{n} to be \tDC{Z}.

407346

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

409348

410−\begin{SaveVerbatim}{vindexty}

411−

349+\begin{code}

412350index : Fin n -> Vect n a -> a

413−

414−\end{SaveVerbatim}

415−\useverb{vindexty}

351+\end{code}

416352

417353\noindent

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

@@ -420,12 +356,9 @@ with \texttt{n} elements of type \texttt{a}. But there are also two names,

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

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

422358

423−\begin{SaveVerbatim}{vindeximpty}

424−

359+\begin{code}

425360index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

426−

427−\end{SaveVerbatim}

428−\useverb{vindeximpty}

361+\end{code}

429362

430363\noindent

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

@@ -437,23 +370,17 @@ free, will be automatically bound as an implicit argument. Implicit arguments

437370can still be given explicitly in applications, using \texttt{\{a=value\}} and

438371\texttt{\{n=value\}}, for example:

439372

440−\begin{SaveVerbatim}{vindexexp}

441−

373+\begin{code}

442374index {a=Int} {n=2} fZ (2 :: 3 :: Nil)

443−

444−\end{SaveVerbatim}

445−\useverb{vindexexp}

375+\end{code}

446376

447377\noindent

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

449379declared the type of \texttt{index} as:

450380

451−\begin{SaveVerbatim}{vindexn}

452−

381+\begin{code}

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

454−

455−\end{SaveVerbatim}

456−\useverb{vindexn}

383+\end{code}

457384

458385\noindent

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

@@ -468,14 +395,11 @@ before being used --- or if an implicit argument has a complex type. For example

468395we will need to state the types of the implicit arguments in the following

469396definition, which defines a predicate on vectors:

470397

471−\begin{SaveVerbatim}{elem}

472−

398+\begin{code}

473399data Elem : a -> Vect n a -> Type where

474400 here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

475401 there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

476−

477−\end{SaveVerbatim}

478−\useverb{elem}

402+\end{code}

479403

480404\noindent

481405An instance of \texttt{Elem x xs} states that \texttt{x} is an element of

@@ -483,31 +407,26 @@ An instance of \texttt{Elem x xs} states that \texttt{x} is an element of

483407such a predicate if the required element is \texttt{here}, at the head of the vector,

484408or \texttt{there}, in the tail of the vector. For example:

485409

486−\begin{SaveVerbatim}{testelem}

487−

410+\begin{code}

488411testVec : Vect 4 Int

489412testVec = 3 :: 4 :: 5 :: 6 :: Nil

490413

491414inVect : Elem 5 testVec

492415inVect = there (there here)

493−

494−\end{SaveVerbatim}

495−\useverb{testelem}

416+\end{code}

496417

497418\noindent

498419If the same implicit arguments are being used a lot, it can make a definition

499420difficult to read. To avoid this problem, a \texttt{using} block gives the types and

500421ordering of any implicit arguments which can appear within the block:

501422

502−\begin{SaveVerbatim}{elemusing}

503−

423+\begin{code}

504424using (x:a, y:a, xs:Vect n a)

505425 data Elem : a -> Vect n a -> Type where

506426 here : Elem x (x :: xs)

507427 there : Elem x xs -> Elem x (y :: xs)

428+\end{code}

508429

509−\end{SaveVerbatim}

510−\useverb{elemusing}

511430

512431\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}

513432

@@ -517,8 +436,7 @@ reduction behaviour to affect type checking. However, this

517436restriction can be relaxed by using a \texttt{mutual} block, which allows

518437data types and functions to be defined simultaneously:

519438

520−\begin{SaveVerbatim}{mutual}

521−

439+\begin{code}

522440mutual

523441 even : Nat -> Bool

524442 even Z = True

@@ -527,9 +445,8 @@ mutual

527445 odd : Nat -> Bool

528446 odd Z = False

529447 odd (S k) = even k

448+\end{code}

530449

531−\end{SaveVerbatim}

532−\useverb{mutual}

533450

534451\noindent

535452In a \texttt{mutual} block, first all of the type declarations are added,

@@ -544,12 +461,10 @@ that is, a language where expressions do not have side-effects --- is that I/O

544461is inherently side-effecting. Therefore in \Idris{}, such interactions are

545462encapsulated in the type \texttt{IO}:

546463

547−\begin{SaveVerbatim}{ioty}

548−

464+\begin{code}

549465data IO a -- IO operation returning a value of type a

466+\end{code}

550467

551−\end{SaveVerbatim}

552−\useverb{ioty}

553468

554469\noindent

555470We'll leave the definition of \texttt{IO} abstract, but effectively it describes what

@@ -558,41 +473,34 @@ resulting operations are executed externally,

558473by the run-time system. We've already seen one IO

559474program:

560475

561−\begin{SaveVerbatim}{main}

562−

476+\begin{code}

563477main : IO ()

564478main = putStrLn "Hello world"

479+\end{code}

565480

566−\end{SaveVerbatim}

567−\useverb{main}

568481

569482\noindent

570483The type of \texttt{putStrLn} explains that it takes a string, and returns an

571484element of the unit type () via an I/O action. There is a variant \texttt{putStr} which

572485outputs a string without a newline:

573486

574−\begin{SaveVerbatim}{putstr}

575−

487+\begin{code}

576488putStrLn : String -> IO ()

577489putStr : String -> IO ()

578−

579−\end{SaveVerbatim}

490+\end{code}

580491

581492We can also read strings from user input:

582493

583−\begin{SaveVerbatim}{getline}

584−

494+\begin{code}

585495getLine : IO String

496+\end{code}

586497

587−\end{SaveVerbatim}

588−\useverb{getline}

589498

590499\noindent

591500A number of other I/O operations are defined in the prelude, for example for reading and

592501writing files, including:

593502

594−\begin{SaveVerbatim}{fileops}

595−

503+\begin{code}

596504data File -- abstract

597505data Mode = Read | Write | ReadWrite

598506

@@ -604,9 +512,8 @@ fwrite : File -> String -> IO ()

604512feof : File -> IO Bool

605513

606514readFile : String -> IO String

515+\end{code}

607516

608−\end{SaveVerbatim}

609−\useverb{fileops}

610517

611518\subsection{``\texttt{do}'' notation}

612519

@@ -617,15 +524,13 @@ computation into the input of the next. \texttt{IO} is an abstract type, however

617524can't access the result of a computation directly. Instead, we sequence

618525operations with \texttt{do} notation:

619526

620−\begin{SaveVerbatim}{greet}

621−

527+\begin{code}

622528greet : IO ()

623529greet = do putStr "What is your name? "

624530 name <- getLine

625531 putStrLn ("Hello " ++ name)

532+\end{code}

626533

627−\end{SaveVerbatim}

628−\useverb{greet}

629534

630535\noindent

631536The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type

@@ -637,12 +542,10 @@ statement in the do block must begin in the same column.

637542The \texttt{return} operation allows us to inject a value directly into an IO

638543operation:

639544

640−\begin{SaveVerbatim}{return}

641−

545+\begin{code}

642546return : a -> IO a

547+\end{code}

643548

644−\end{SaveVerbatim}

645−\useverb{return}

646549

647550\noindent

648551As we will see later, \texttt{do} notation is more general than this, and can be

@@ -659,16 +562,14 @@ part of \texttt{prelude.idr}.

659562

660563We have already seen the \texttt{List} and \texttt{Vect} data types:

661564

662−\begin{SaveVerbatim}{listvec}

663−

565+\begin{code}

664566data List a = Nil | (::) a (List a)

665567

666568data Vect : Nat -> Type -> Type where

667569 Nil : Vect Z a

668570 (::) : a -> Vect k a -> Vect (S k) a

571+\end{code}

669572

670−\end{SaveVerbatim}

671−\useverb{listvec}

672573

673574\noindent

674575Note that the constructor names are the same for each --- constructor names (in

@@ -687,8 +588,7 @@ The library also defines a number of functions for manipulating these types.

687588\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}

688589and applies a function to every element of the list or vector.

689590

690−\begin{SaveVerbatim}{map}

691−

591+\begin{code}

692592map : (a -> b) -> List a -> List b

693593map f [] = []

694594map f (x :: xs) = f x :: map f xs

@@ -696,34 +596,29 @@ map f (x :: xs) = f x :: map f xs

696596map : (a -> b) -> Vect n a -> Vect n b

697597map f [] = []

698598map f (x :: xs) = f x :: map f xs

599+\end{code}

699600

700−\end{SaveVerbatim}

701−\useverb{map}

702601

703602\noindent

704603For example, to double every element in a vector of integers:

705604

706−\begin{SaveVerbatim}{dvect}

707−

605+\begin{code}

708606intVec : Vect 5 Int

709607intVec = [1, 2, 3, 4, 5]

710608

711609double : Int -> Int

712610double x = x * 2

611+\end{code}

713612

714−\end{SaveVerbatim}

715−\useverb{dvect}

716613

717614\noindent

718615You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:

719616

720−\begin{SaveVerbatim}{rundvect}

721−

617+\begin{lstlisting}

722618*usefultypes> show (map double intVec)

723619"[2, 4, 6, 8, 10]" : String

620+\end{lstlisting}

724621

725−\end{SaveVerbatim}

726−\useverb{rundvect}

727622

728623\noindent

729624For more details of the functions available on \texttt{List} and \texttt{Vect},

@@ -737,13 +632,11 @@ need, please feel free to add it and submit a patch!

737632There are actually neater ways to write the above expression. One way would be

738633to use an anonymous function:

739634

740−\begin{SaveVerbatim}{lam1}

741−

635+\begin{lstlisting}

742636*usefultypes> show (map (\x => x * 2) intVec)

743637"[2, 4, 6, 8, 10]" : String

638+\end{lstlisting}

744639

745−\end{SaveVerbatim}

746−\useverb{lam1}

747640

748641\noindent

749642The notation \texttt{$\backslash$x => val} constructs an anonymous function

@@ -754,13 +647,11 @@ types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,

754647e.g. \texttt{$\backslash$ (x, y) => x + y}.

755648We could also use an operator section:

756649

757−\begin{SaveVerbatim}{sec1}

758−

650+\begin{code}

759651*usefultypes> show (map (* 2) intVec)

760652"[2, 4, 6, 8, 10]" : String

653+\end{code}

761654

762−\end{SaveVerbatim}

763−\useverb{sec1}

764655

765656\noindent

766657\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to

@@ -772,38 +663,32 @@ Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.

772663\texttt{Maybe} describes an optional value. Either there is a value of the given type,

773664or there isn't:

774665

775−\begin{SaveVerbatim}{maybe}

776−

666+\begin{code}

777667data Maybe a = Just a | Nothing

668+\end{code}

778669

779−\end{SaveVerbatim}

780−\useverb{maybe}

781670

782671\noindent

783672\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,

784673looking something up in a \texttt{List} (rather than a vector) may result in an out of

785674bounds error:

786675

787−\begin{SaveVerbatim}{lookuplist}

788−

676+\begin{code}

789677list_lookup : Nat -> List a -> Maybe a

790678list_lookup _ Nil = Nothing

791679list_lookup Z (x :: xs) = Just x

792680list_lookup (S k) (x :: xs) = list_lookup k xs

681+\end{code}

793682

794−\end{SaveVerbatim}

795−\useverb{lookuplist}

796683

797684\noindent

798685The \texttt{maybe} function is used to process values of type \texttt{Maybe},

799686either by applying a function to the value, if there is one, or by providing a default value:

800687

801−\begin{SaveVerbatim}{maybefn}

802−

688+\begin{code}

803689maybe : Maybe a -> |(default:b) -> (a -> b) -> b

690+\end{code}

804691

805−\end{SaveVerbatim}

806−\useverb{maybefn}

807692

808693\noindent

809694The vertical bar $\mid$ before the default value is a laziness annotation. Normally

@@ -817,41 +702,35 @@ needed.

817702

818703Values can be paired with the following built-in data type:

819704

820−\begin{SaveVerbatim}{mkpair}

821−

705+\begin{code}

822706data Pair a b = MkPair a b

707+\end{code}

823708

824−\end{SaveVerbatim}

825−\useverb{mkpair}

826709

827710\noindent

828711As syntactic sugar, we can write \texttt{(a, b)} which, according to context,

829712means either \texttt{Pair a b} or \texttt{MkPair a b}.

830713Tuples can contain an arbitrary number of values, represented as nested pairs:

831714

832−\begin{SaveVerbatim}{tuple}

833−

715+\begin{code}

834716fred : (String, Int)

835717fred = ("Fred", 42)

836718

837719jim : (String, Int, String)

838720jim = ("Jim", 25, "Cambridge")

721+\end{code}

839722

840−\end{SaveVerbatim}

841−\useverb{tuple}

842723

843724\subsubsection*{Dependent Pairs}

844725

845726Dependent pairs allow the type of the second element of a pair to depend on

846727the value of the first element:

847728

848−\begin{SaveVerbatim}{sigma}

849−

729+\begin{code}

850730data Exists : (A : Type) -> (P : A -> Type) -> Type where

851731 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P

732+\end{code}

852733

853−\end{SaveVerbatim}

854−\useverb{sigma}

855734

856735\noindent

857736Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of

@@ -859,13 +738,11 @@ A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}

859738constructs a value of this type. For example, we can pair a number with a

860739\texttt{Vect} of a particular length.

861740

862−\begin{SaveVerbatim}{dvec}

863−

741+\begin{code}

864742vec : (n : Nat ** Vect n Int)

865743vec = (2 ** [3, 4])

744+\end{code}

866745

867−\end{SaveVerbatim}

868−\useverb{dvec}

869746

870747\noindent

871748The type checker could of course infer the value of the first element from the

@@ -873,25 +750,21 @@ length of the vector. We can write an underscore \texttt{\_} in place of values

873750expect the type checker to fill in, so the above definition could also be

874751written as:

875752

876−\begin{SaveVerbatim}{dvec1}

877−

753+\begin{code}

878754vec : (n : Nat ** Vect n Int)

879755vec = (_ ** [3, 4])

756+\end{code}

880757

881−\end{SaveVerbatim}

882−\useverb{dvec1}

883758

884759\noindent

885760We might also prefer to omit the type of the first element of the pair, since,

886761again, it can be inferred:

887762

888−\begin{SaveVerbatim}{dvec2}

889−

763+\begin{code}

890764vec : (n ** Vect n Int)

891765vec = (_ ** [3, 4])

766+\end{code}

892767

893−\end{SaveVerbatim}

894−\useverb{dvec2}

895768

896769\noindent

897770One use for dependent pairs is to return values of dependent types where the

@@ -899,22 +772,18 @@ index is not necessarily known in advance. For example, if we filter elements

899772out of a \texttt{Vect} according to some predicate, we will not know in advance what the

900773length of the resulting vector will be:

901774

902−\begin{SaveVerbatim}{vfilter}

903−

775+\begin{code}

904776filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

777+\end{code}

905778

906−\end{SaveVerbatim}

907−\useverb{vfilter}

908779

909780\noindent

910781If the \texttt{Vect} is empty, the result is easy:

911782

912−\begin{SaveVerbatim}{vfilternil}

913−

783+\begin{code}

914784filter p Nil = (_ ** [])

785+\end{code}

915786

916−\end{SaveVerbatim}

917−\useverb{vfilternil}

918787

919788\noindent

920789In the \texttt{::} case, we need to inspect the result of a recursive call to

@@ -922,13 +791,10 @@ In the \texttt{::} case, we need to inspect the result of a recursive call to

922791extract the length and the vector from the result. To do this, we use \texttt{with}

923792notation, which allows pattern matching on intermediate values:

924793

925−\begin{SaveVerbatim}{vfiltercons}

926−

794+\begin{code}

927795filter p (x :: xs) with (filter p xs)

928796 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

929−

930−\end{SaveVerbatim}

931−\useverb{vfiltercons}

797+\end{code}

932798

933799\noindent

934800We will see more on \texttt{with} notation later.

@@ -938,13 +804,11 @@ We will see more on \texttt{with} notation later.

938804The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the

939805value is true:

940806

941−\begin{SaveVerbatim}{sotype}

942−

807+\begin{code}

943808data so : Bool -> Type where

944809 oh : so True

945−

946−\end{SaveVerbatim}

947−\useverb{sotype}

810+\end{code}

811+

948812

949813\noindent

950814This is most useful for providing a static guarantee that a dynamic check has been made.

@@ -952,16 +816,14 @@ For example, we might provide a safe interface to a function which draws a pixel

952816on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that

953817the point \texttt{(x,y)} is within the bounds of a 640x480 window:

954818

955−\begin{SaveVerbatim}{soexample}

956−

819+\begin{code}

957820inBounds : Int -> Int -> Bool

958821inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480

959822

960823drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()

961824drawPoint x y p = unsafeDrawPoint x y

962−

963−\end{SaveVerbatim}

964−\useverb{soexample}

825+\end{code}

826+

965827

966828\subsection{More Expressions}

967829

@@ -969,29 +831,25 @@ drawPoint x y p = unsafeDrawPoint x y

969831

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

971833

972−\begin{SaveVerbatim}{letb}

973−

834+\begin{code}

974835mirror : List a -> List a

975836mirror xs = let xs' = rev xs in

976837 xs ++ xs'

977−

978−\end{SaveVerbatim}

979−\useverb{letb}

838+\end{code}

839+

980840

981841\noindent

982842We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract

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

984844

985−\begin{SaveVerbatim}{letp}

986−

845+\begin{code}

987846data Person = MkPerson String Int

988847

989848showPerson : Person -> String

990849showPerson p = let MkPerson name age = p in

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

992−

993−\end{SaveVerbatim}

994−\useverb{letp}

851+\end{code}

852+

995853

996854\subsubsection*{List comprehensions}

997855

@@ -1000,12 +858,10 @@ showPerson p = let MkPerson name age = p in

1000858\Idris{} provides \emph{comprehension} notation as a convenient shorthand for

1001859building lists. The general form is:

1002860

1003−\begin{SaveVerbatim}{listcomp}

1004−

861+\begin{lstlisting}

1005862[ expression | qualifiers ]

1006−

1007−\end{SaveVerbatim}

1008−\useverb{listcomp}

863+\end{lstlisting}

864+

1009865

1010866\noindent

1011867This generates the list of values produced by evaluating the

@@ -1013,14 +869,12 @@ This generates the list of values produced by evaluating the

1013869\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as

1014870follows:

1015871

1016−\begin{SaveVerbatim}{triples}

1017−

872+\begin{code}

1018873pythag : Int -> List (Int, Int, Int)

1019874pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],

1020875 x*x + y*y == z*z ]

1021−

1022−\end{SaveVerbatim}

1023−\useverb{triples}

876+\end{code}

877+

1024878

1025879\noindent

1026880The \texttt{[a..b]} notation is another shorthand which builds a list of

@@ -1035,14 +889,12 @@ Another way of inspecting intermediate values of \emph{simple} types

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

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

1037891

1038−\begin{SaveVerbatim}{split}

1039−

892+\begin{code}

1040893splitAt : Char -> String -> (String, String)

1041894splitAt c x = case break (== c) x of

1042895 (x, y) => (x, strTail y)

1043−

1044−\end{SaveVerbatim}

1045−\useverb{split}

896+\end{code}

897+

1046898

1047899\noindent

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

@@ -1055,29 +907,25 @@ looks up an index in a list, returning \texttt{Nothing} if the index is out

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

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

1057909

1058−\begin{SaveVerbatim}{listlookup}

1059−

910+\begin{code}

1060911lookup_default : Nat -> List a -> a -> a

1061912lookup_default i xs def = case list_lookup i xs of

1062913 Nothing => def

1063914 Just x => x

1064−

1065−\end{SaveVerbatim}

1066−\useverb{listlookup}

915+\end{code}

916+

1067917

1068918\noindent

1069919If the index is in bounds, we get the value at that index, otherwise we get

1070920a default value:

1071921

1072−\begin{SaveVerbatim}{deftest}

1073−

922+\begin{lstlisting}

1074923*usefultypes> lookup_default 2 [3,4,5,6] (-1)

10759245 : Int

1076925*usefultypes> lookup_default 4 [3,4,5,6] (-1)

1077926-1 : Int

1078−

1079−\end{SaveVerbatim}

1080−\useverb{deftest}

927+\end{lstlisting}

928+

1081929

1082930\noindent

1083931\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis

@@ -1099,17 +947,15 @@ determined \emph{without} type checking the \texttt{case}-expression itself.

1099947automatically generating field access and update functions. For example, we

1100948can represent a person's name and age in a record:

1101949

1102−\begin{SaveVerbatim}{recsimpl}

1103−

950+\begin{code}

1104951record Person : Type where

1105952 MkPerson : (name : String) ->

1106953 (age : Int) -> Person

1107954

1108955fred : Person

1109956fred = MkPerson "Fred" 30

1110−

1111−\end{SaveVerbatim}

1112−\useverb{recsimpl}

957+\end{code}

958+

1113959

1114960\noindent

1115961Record declarations are like \texttt{data} declarations, except that they are

@@ -1117,31 +963,25 @@ introduced by the \texttt{record} keyword, and can only have one constructor.

1117963The names of the binders in the constructor type (\texttt{name} and \texttt{age})

1118964here are the field names, which we can use to access the field values:

1119965

1120−\begin{SaveVerbatim}{recaccess}

1121−

966+\begin{lstlisting}

1122967*record> name fred

1123968"Fred" : String

1124969*record> age fred

112597030 : Int

1126971*record> :t name

1127972name : Person -> String

1128−

1129−\end{SaveVerbatim}

1130−\useverb{recaccess}

973+\end{lstlisting}

1131974

1132975\noindent

1133976We can also use the field names to update a record (or, more precisely, produce a

1134977new record with the given fields updates).

1135978

1136−\begin{SaveVerbatim}{recupdate}

1137−

979+\begin{lstlisting}

1138980*record> record { name = "Jim" } fred

1139981MkPerson "Jim" 30 : Person

1140982*record> record { name = "Jim", age = 20 } fred

1141983MkPerson "Jim" 20 : Person

1142−

1143−\end{SaveVerbatim}

1144−\useverb{recupdate}

984+\end{lstlisting}

1145985

1146986\noindent

1147987The syntax \texttt{record \{ field = val, ... \}} generates a function which updates

@@ -1152,29 +992,26 @@ Updates are allowed to change the type of a field,

1152992provided that the result is well-typed, and the result does not affect the type of

1153993the record as a whole. For example:

1154994

1155−\begin{SaveVerbatim}{deprec}

1156−

995+\begin{code}

1157996record Class : Type where

1158997 ClassInfo : (students : Vect n Person) ->

1159998 (className : String) ->

1160999 Class

1161−

1162−\end{SaveVerbatim}

1163−\useverb{deprec}

1000+\end{code}

11641001

11651002\noindent

11661003It is safe to update the \texttt{students} field to a vector of a different length

11671004because it will not affect the type of the record:

11681005

1169−\begin{SaveVerbatim}{addstu}

1170−

1006+\begin{code}

11711007addStudent : Person -> Class -> Class

11721008addStudent p c = record { students = p :: students c } c

1009+\end{code}

11731010

1011+\begin{lstlisting}

11741012*record> addStudent fred (ClassInfo [] "CS")

11751013ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"

11761014 : Class

1015+\end{lstlisting}

11771016

1178−\end{SaveVerbatim}

1179−\useverb{addstu}

11801017

tutorial/views.tex → tutorial/content/views.texrenamed+10−25

@@ -7,14 +7,11 @@ by the value of others. For example, if we were to write down the implicit

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

88determined by whether the vector was empty or not:

10−\begin{SaveVerbatim}{appdep}

11−

10+\begin{code}

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

1312(++) {n=Z} [] ys = ys

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

15−

16−\end{SaveVerbatim}

17−\useverb{appdep}

14+\end{code}

1815

1916\noindent

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

@@ -32,15 +29,12 @@ we know about the forms of other values. In its simplest form, the \texttt{with}

3229adds another argument to the function being defined, e.g. we have already seen

3330a vector filter function, defined as follows:

3431

35−\begin{SaveVerbatim}{vfilterdef}

36−

32+\begin{code}

3733filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

3834filter p [] = ( _ ** [] )

3935filter p (x :: xs) with (filter p xs)

4036 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

41−

42−\end{SaveVerbatim}

43−\useverb{vfilterdef}

37+\end{code}

4438

4539\noindent

4640Here, the \texttt{with} clause allows us to deconstruct the result of

@@ -54,26 +48,20 @@ testing another. For example, a \texttt{Nat} is either even or odd. If it's even

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

5549plus one:

5650

57−\begin{SaveVerbatim}{parity}

58−

51+\begin{code}

5952data Parity : Nat -> Type where

6053 even : Parity (n + n)

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

62−

63−\end{SaveVerbatim}

64−\useverb{parity}

55+\end{code}

6556

6657\noindent

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

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

6960it is even or odd and constructs the predicate accordingly.

7061

71−\begin{SaveVerbatim}{parityty}

72−

62+\begin{code}

7363parity : (n:Nat) -> Parity n

74−

75−\end{SaveVerbatim}

76−\useverb{parityty}

64+\end{code}

7765

7866\label{sect:nattobin}

7967

@@ -82,16 +70,13 @@ We'll come back to the definition of \texttt{parity} shortly. We can use it

8270to write a function which converts a natural number to a list of binary digits

8371(least significant first) as follows, using the \texttt{with} rule:

8472

85−\begin{SaveVerbatim}{natToBin}

86−

73+\begin{code}

8774natToBin : Nat -> List Bool

8875natToBin Z = Nil

8976natToBin k with (parity k)

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

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

92−

93−\end{SaveVerbatim}

94−\useverb{natToBin}

79+\end{code}

9580

9681\noindent

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

tutorial/macros.ltx → tutorial/fpmacros.styrenamed+41−21

@@ -1,11 +1,25 @@

1−%\usepackage{amstex}

2−\usepackage{amssymb}

3−\usepackage{latexsym}

4−\usepackage{eepic}

5−

1+%% ------------------------------------------- [ Functional Programming Macros ]

2+%% A Package to provide support for functional programming.

3+%%

4+\NeedsTeXFormat{LaTeX2e}[1994/06/01]

5+\ProvidesPackage{fpmacros}[2013/12/17 fpmacros]

6+%% ------------------------------------------------------- [ Required Packages ]

7+\RequirePackage{ifthen}

8+\RequirePackage{amssymb}

9+\RequirePackage{latexsym}

10+\RequirePackage{eepic}

11+\RequirePackage{fancyvrb}

12+%% ----------------------------------------------------- [ Option Delcarations ]

13+\newboolean{useverb}

14+\setboolean{useverb}{true}

15+

16+\DeclareOption{noverb}{%

17+ \setboolean{useverb}{false}

18+}

619

7−%%%%%%%%% INFERENCE RULES

20+\ProcessOptions\relax

821

22+%% --------------------------------------------------------- [ Inference Rules ]

923\newlength{\rulevgap}

1024\setlength{\rulevgap}{0.05in}

1125\newlength{\ruleheight}

@@ -78,8 +92,7 @@

7892\setlength{\unitlength}{0.0005in}

7993\begin{picture}(69,180)(0,12)

8094\blacken\path(12,192)(12,12)(57,102)

81− (12,192)(12,192)

82−\path(12,192)(12,12)(57,102)

95+ (12,192)(12,192)\path(12,192)(12,12)(57,102)

8396 (12,192)(12,192)

8497\end{picture}

8598}

@@ -305,18 +318,20 @@

305318

306319\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}

307320

308−\newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}

309−\newcommand{\useverb}[1]{\BUseVerbatim{#1}}

310−\newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

311−\newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

321+\ifthenelse{\boolean{useverb}}{%

322+ \newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}

323+ \newcommand{\useverb}[1]{\BUseVerbatim{#1}}

324+ \newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

325+ \newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

326+ \newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

327+ \newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}

328+ \newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

329+ \newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

330+ \newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

331+}{}

312332

313333\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}

314334\caption{#3}\label{#2}\end{figure}}

315−\newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

316−\newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}

317−\newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

318−\newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

319−\newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

320335\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}

321336\caption{#3}\label{#2}\end{figure*}}

322337

@@ -324,10 +339,13 @@

324339\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

325340\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

326341\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}

327−\newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}

328342\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}

329343\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

330344

345+\ifthenelse{\boolean{useverb}}{%

346+ \newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}

347+}{}

348+

331349\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}

332350\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}

333351

@@ -676,8 +694,9 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

676694\newcommand{\falsecase}{\Cases{\False}}

677695

678696% Code

679−\newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}

680−

697+\ifthenelse{\boolean{useverb}}{%

698+ \newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}

699+}{}

681700% Quicksort

682701

683702\newcommand{\QSView}{\TC{QuickSort}}

@@ -1063,4 +1082,5 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

10631082\newcommand{\direct}[1]{\texttt{\%#1}}

10641083

10651084\newcommand{\Feature}[1]{\textbf{Remark:}}

1066−%\newcommand{\Remark}[1]{\textbf{Remark:}}

1085+

1086+\endinput

tutorial/idris-tutorial.pdfdeleted

Binary file not shown.

tutorial/idris-tutorial.tex+36−21

@@ -1,39 +1,54 @@

1−\documentclass{article}

1+\documentclass[british, final]{article}

3+\usepackage[l2tabu,orthodox]{nag}

4+\usepackage{fixltx2e}

5+\usepackage{babel}

6+\usepackage[iso]{isodate}

7+\usepackage[utf8]{inputenc}

8+\usepackage[T1]{fontenc}

9+\usepackage[protrusion=true, expansion=true]{microtype}

10+\usepackage[strict=true]{csquotes}

11+\usepackage{xspace}

12+

13+\usepackage{mathpazo}

14+\usepackage[scaled=0.95]{helvet}

15+\usepackage{courier}

216

317\usepackage{fullpage}

4−\usepackage{palatino}

5−\usepackage{url}

6−\usepackage{fancyvrb}

718\usepackage{hyperref}

19+\usepackage[missing=0.9.10]{gitinfo}

20+

21+\usepackage{fpmacros}

22+\usepackage[numbers]{idrislang}

823

924\input{conf.ltx}

10−\input{macros.ltx}

1125\input{library.ltx}

1226

13−\newcommand{\Idris}{\textsc{Idris}}

14−\newcommand{\version}{0.9.10}

27+\newcommand{\version}{\gitVtagn}

1528

1629\title{Programming in \Idris{}: a tutorial}

17−\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}

30+\author{The \Idris{} Community}

31+\date{\origdate\today}

1832

1933\begin{document}

2034

2135\maketitle

2236

2337\tableofcontents

24−

25−\input{intro}

26−\input{starting}

27−\input{typesfuns}

28−\input{classes}

29−\input{modules}

30−\input{interp}

31−\input{views}

32−\input{theorems}

33−\input{provisional}

34−\input{syntax}

35−\input{miscellany}

36−\input{conclusions}

38+\newpage

39+

40+\input{./content/intro}

41+\input{./content/starting}

42+\input{./content/typesfuns}

43+\input{./content/classes}

44+\input{./content/modules}

45+\input{./content/interp}

46+\input{./content/views}

47+\input{./content/theorems}

48+\input{./content/provisional}

49+\input{./content/syntax}

50+\input{./content/miscellany}

51+\input{./content/conclusions}

3752

3853\bibliographystyle{abbrv}

3954\bibliography{literature.bib}

tutorial/idrislang.stynew file+188

@@ -0,0 +1,188 @@

1+%% --------------------------------------------------- [ Idris Styling Package ]

2+%%

3+%% A set of LaTeX macros and styling for working with Idris in LaTeX

4+%%

5+%% + Provides a listings bindings:

6+%% + idris :: default ascii

7+%% + literateidris :: convert ascii maths to math symbols.

8+%% + Defines a `numbers' and `default' listings style.

9+%% + Defines a `code' environment for typesetting idris.

10+%% + \begin{code}[...] ... \end{code}

11+%% + Defines commands typesetting the name Idris.

12+%% + \Idris{}

13+%% + \idris{}

14+%%

15+%% Options:

16+%% - literate :: turn on literate idris for code environments.

17+%% - numbers :: turn on numbers for code environments.

18+%%

19+%% ----------------------------------------------------------- [ Begin Package ]

20+\ProvidesPackage{idrislang}

21+

22+\RequirePackage{ifthen}

23+\RequirePackage{listings}

24+\RequirePackage{xspace}

25+%% ----------------------------------------------------------------- [ Options ]

26+\newboolean{literate}

27+\setboolean{literate}{false}

28+\newboolean{numbers}

29+\setboolean{numbers}{false}

30+

31+\DeclareOption{literate}{%

32+ \setboolean{literate}{true}

33+}

34+

35+\DeclareOption{numbers}{%

36+ \setboolean{numbers}{true}

37+}

38+

39+\ProcessOptions\relax

40+

41+%% ---------------------------------------------------------------- [ Commands ]

42+\newcommand{\Idris}{\textsc{Idris}\xspace}

43+\newcommand{\idris}{\textsc{Idris}\xspace}

44+

45+%% --------------------------------------------------- [ Define Idris Listings ]

46+\lstdefinelanguage{idris}{%

47+ sensitive,%

48+%% ----------------------------------------------------------- [ Default Style ]

49+ basicstyle=\ttfamily,

50+ flexiblecolumns=false,

51+ commentstyle=\footnotesize\sffamily,

52+%% ---------------------------------------------------------------- [ Keywords ]

53+%% From Idris Parser and idris-mode and vimscript

54+ keywords={%

55+ abstract, attack, case, compute, do, dsl, else, exact, focus, if,

56+ import, in, infix, infixl, infixr, instance, intros, module,

57+ mutual, namespace, of, let, parameters, partial, pattern, prefix,

58+ private, public, refine, rewrite, solve, syntax, term, then,

59+ total, trivial, try, using, where, with

60+},

61+%% ------------------------------------------------------- [ Prelude Functions ]

62+%% Generated using

63+%% find lib/ -name "*.idr" | xargs grep -e "^[a-zA-Z0-9]* :" | awk -F : '{printf $2", "}'

64+ morekeywords={%

65+ class, data, instance, record, dsl, postulate, default, assert_total,

66+ lambda, variable, index_first, index_next

67+ % trace, unsafePerformPrimIO, FInt, FChar, FByte, FShort, FLong,

68+ % FBits8, FBits16, FBits32, FBits64, FBits8x16, FBits16x8,

69+ % FBits32x4, FBits64x2, interpFTy, ForeignTy, mkForeignPrim,

70+ % mkLazyForeignPrim, liftPrimIO, fork, unsafePerformIO, listens,

71+ % censor, Writer, liftReaderT, asks, Reader, modify, gets, State,

72+ % RWS, nGTSm, decideNatLTE, lte, vectInjective1, vectInjective2,

73+ % run, myID, send, msgWaiting, recv, recvWithSender, create,

74+ % sendToThread, checkMsgs, getMsg, viewB8x16, viewB16x8, viewB32x4,

75+ % viewB64x2, pow, exp, log, pi, sin, cos, tan, asin, acos, atan,

76+ % atan2, sinh, cosh, tanh, sqrt, floor, ceiling, count, countFrom,

77+ % curry, uncurry, uniformB8x16, uniformB16x8, uniformB32x4,

78+ % uniformB64x2, putStr, putStrLn, print, getLine, putChar, getChar,

79+ % fopen, openFile, closeFile, fread, fwrite, feof, ferror, nullPtr,

80+ % nullStr, validFile, while, readFile, userSuppliedName, seq, try,

81+ % mkPair, getUName, unApply, mkApp, binderTy, divCeil, nextPow2,

82+ % nextBytes, machineTy, bitsUsed, natToBits, getPad, pad8, pad16,

83+ % pad32, pad64, shiftLeft, shiftRightLogical, shiftRightArithmetic,

84+ % and, or, xor, plus, minus, times, sdiv, udiv, srem, urem, lt, lte,

85+ % eq, gte, gt, complement, zeroExtend, intToBits, bitsToInt, bitAt,

86+ % getBit, setBit, unsetBit, bitsToStr, findElem, replaceElem,

87+ % replaceByElem, mapElem, anyNilAbsurd, anyElim, any, negAnyAll,

88+ % notAllHere, notAllThere, all, length, index, weaken, take, toList,

89+ % fromList, replicate, foldl, foldr, map, pad, zeroBoundIsEmpty,

90+ % empty, insert, delete, contains, fromList, toList, applyKleisli,

91+ % applyMor, applyEndo, absZ, negZ, negNat, minusNatZ, plusZ, subZ,

92+ % multZ, fromInt, natPlusZPlus, natMultZMult, doubleNegElim,

93+ % posInjective, negSInjective, posNotNeg, plusZeroLeftNeutralZ,

94+ % plusZeroRightNeutralZ, plusCommutativeZ, modBin, modComp, div,

95+ % rem, intToMod, modToStr, branch4, branch5, branch6, branch7,

96+ % merge1, merge2, merge3, treeLookup, treeInsert, delType,

97+ % treeDelete, treeToList, empty, lookup, insert, delete, fromList,

98+ % toList, getWitness, getProof, FalseElim, replace, sym, trans,

99+ % lazy, par, malloc, Not, id, the, const, fst, snd, flip, cong,

100+ % boolElim, not, intToBool, boolOp, div, mod, strHead, strTail,

101+ % strCons, strIndex, reverse, null, getArgs, getEnv, setEnv,

102+ % unsetEnv, getEnvironment, exit, usleep, sequence, toHexDigit,

103+ % b8ToString, b16ToString, b32ToString, b64ToString, tail, head,

104+ % last, init, index, deleteAt, replaceAt, take, drop, fromList,

105+ % replicate, zipWith, zip, unzip, concat, elemBy, elem, lookupBy,

106+ % lookup, hasAnyBy, hasAny, find, findIndex, elemIndexBy, elemIndex,

107+ % nubBy, nub, isPrefixOfBy, isPrefixOf, isSuffixOfBy, isSuffixOf,

108+ % catMaybes, diag, range, isLeft, isRight, choose, either, lefts,

109+ % rights, partitionEithers, fromEither, maybeToEither, strM, unpack,

110+ % pack, span, break, split, ltrim, trim, words, lines, foldr1,

111+ % unwords, length, realPart, imagPart, mkPolar, cis, magnitude,

112+ % phase, conjugate, isNothing, isJust, maybe, fromMaybe, toMaybe,

113+ % justInjective, lowerMaybe, raiseToMaybe, isNil, isCons, head,

114+ % tail, last, init, take, drop, takeWhile, dropWhile, list, length,

115+ % repeat, replicate, zipWith, zipWith3, zip, zip3, unzip, unzip3,

116+ % mapMaybe, toList, reverse, intersperse, intercalate, elemBy, elem,

117+ % lookupBy, lookup, hasAnyBy, hasAny, find, findIndex, findIndices,

118+ % elemIndexBy, elemIndex, elemIndicesBy, elemIndices, filter, nubBy,

119+ % nub, span, break, split, partition, isPrefixOfBy, isPrefixOf,

120+ % isSuffixOfBy, isSuffixOf, sorted, mergeBy, merge, sort,

121+ % maybeToList, listToMaybe, catMaybes, appendNilRightNeutral,

122+ % appendAssociative, lengthAppend, mapPreservesLength,

123+ % mapDistributesOverAppend, mapFusion, hasAnyByNilFalse,

124+ % hasAnyNilFalse, fromIntegerNat, toIntegerNat, hyper, log2, gcd,

125+ % liftA, liftA2, liftA3, guard, when, finToNat, finToInt, weaken,

126+ % strengthen, last, natToFin, integerToFin, fromInteger, flatten,

127+ % return, isUpper, isLower, isAlpha, isDigit, isAlphaNum, isSpace,

128+ % isNL, toUpper, toLower, isHexDigit, isValidHeap, merge, insert,

129+ % findMinimum, deleteMinimum, toList, fromList, sort, main, foldl,

130+ % concat, concatMap, and, or, any, all, sum, product, Vars,

131+ % getAction, setInfo, getInfo, lift, output, queryVars, postVars,

132+ % cookieVars, queryVar, getOutput, getHeaders, flushHeaders, flush,

133+ % getVars, getContent, getCgiEnv, runCGI, mult

134+ },

135+%% ---------------------------------------------------------------- [ Comments ]

136+ morecomment=[l]--,%

137+ morecomment=[n]{\{-}{-\}}

138+}[keywords,comments,strings]%

139+

140+%% ---------------------------------------- [ Define Idris with Literate Stuff ]

141+\lstdefinelanguage{literateidris}[]{idris}{

142+ literate= {+}{{$+$}}1

143+ {/}{{$/$}}1

144+ {*}{{$*$}}1

145+ {=}{{$=$}}1

146+ {>}{{$>$}}1

147+ {<}{{$<$}}1

148+ {\\}{{$\lambda$}}1

149+ {\\\\}{{\char`\\\char`\\}}1

150+ {->}{{$\rightarrow$}}2

151+ {>=}{{$\geq$}}2

152+ {<-}{{$\leftarrow$}}2

153+ {<=}{{$\leq$}}2

154+ {=>}{{$\Rightarrow$}}2

155+ {==}{{$\equiv$}}2

156+ {\ .}{{$\circ$}}2

157+ {\ .\ }{{$\circ$}}2

158+ {>>}{{>>}}2

159+ {>>=}{{>>=}}2

160+ {|}{{$\mid$}}1,

161+}

162+%% -------------------------------------------------- [ Default Listings Style ]

163+

164+\lstdefinestyle{default}{%

165+ xleftmargin=\parindent,

166+ tabsize=2

167+}

168+\lstdefinestyle{numbers}{%

169+ numbers=left,

170+ numbersep=10pt,

171+ numberstyle=\footnotesize\sffamily,

172+ frame=leftline

173+}

174+

175+%% ------------------------------------------------------ [ A Code Environment ]

176+%% Replicate the existence of literate haskell code environments,

177+%% option to make pretty with numbers.

178+\lstnewenvironment{code}[1][]

179+ {\ifthenelse{\boolean{literate}}{%

180+ \lstset{language=literateidris}}{%

181+ \lstset{language=idris}}

182+ \ifthenelse{\boolean{numbers}}{%

183+ \lstset{style=numbers, #1}}{%

184+ \lstset{style=default, #1}}

185+ }

186+ {}

187+\endinput

188+%% --------------------------------------------------------------------- [ EOF ]