2c001c9 · Idris-dev · git.iko.soy

docs/tutorial/index.rst+4−2

compare with master

unifiedsplit

@@ -4,7 +4,10 @@

4The Idris Tutorial

5##################

6

7+This is the Idris Tutorial.

7−This is the Idris Tutorial. It will teach you about programming in the Idris Language.

8+It provides a brief introduction to programming in the Idris Language.

9+It covers the core language features, and assumes some familiarity with an

10+existing functional programming language such as Haskell or OCaml.

8

11

9.. note::

12.. note::

10 The documentation for Idris has been published under the Creative

13 The documentation for Idris has been published under the Creative

@@ -27,7 +30,6 @@ This is the Idris Tutorial. It will teach you about programming in the Idris Lan

27 interp

30 interp

28 views

31 views

29 theorems

32 theorems

30− provisional

31 interactive

33 interactive

32 syntax

34 syntax

33 miscellany

35 miscellany

docs/tutorial/interfaces.rst+45−2

@@ -253,9 +253,9 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").

253

254::

255

256− *ifaces> m_add (Just 20) (Just 22)

256+ *Interfaces> m_add (Just 20) (Just 22)

257 Just 42 : Maybe Int

258− *ifaces> m_add (Just 20) Nothing

258+ *Interfaces> m_add (Just 20) Nothing

259 Nothing : Maybe Int

260

261Pattern Matching Bind

@@ -566,6 +566,49 @@ implementation ``myord`` as follows, at the Idris prompt:

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

567

568

569+Sometimes, we also need access to a named parent implementation. For example,

570+the prelude defines the following ``Semigroup`` interface:

571+

572+.. code-block:: idris

573+

574+ interface Semigroup ty where

575+ (<+>) : ty -> ty -> ty

576+

577+Then it defines ``Monoid``, which extends ``Semigroup`` with a "neutral"

578+value:

579+

580+.. code-block:: idris

581+

582+ interface Semigroup ty => Monoid ty where

583+ neutral : ty

584+

585+We can define two different implementations of ``Semigroup`` and

586+``Monoid`` for ``Nat``, one based on addition and one on multiplication:

587+

588+.. code-block:: idris

589+

590+ [PlusNatSemi] Semigroup Nat where

591+ (<+>) x y = x + y

592+

593+ [MultNatSemi] Semigroup Nat where

594+ (<+>) x y = x * y

595+

596+The neutral value for addition is ``0``, but the neutral value for multiplication

597+is ``1``. It's important, therefore, that when we define implementations

598+of ``Monoid`` they extend the correct ``Semigroup`` implementation. We can

599+do this with a ``using`` clause in the implementation as follows:

600+

601+.. code-block:: idris

602+

603+ [PlusNatMonoid] Monoid Nat using PlusNatSemi where

604+ neutral = 0

605+

606+ [MultNatMonoid] Monoid Nat using MultNatSemi where

607+ neutral = 1

608+

609+The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should

610+extend ``PlusNatSemi`` specifically.

611+

569Determining Parameters

612Determining Parameters

570======================

613======================

571

614

docs/tutorial/introduction.rst+5

@@ -55,6 +55,11 @@ assumed, although most concepts will at least be explained

55briefly. The reader is also assumed to have some interest in using

56dependent types for writing and verifying systems software.

57

58+For a more in-depth introduction to Idris, which proceeds at a much slower

59+pace, covering interactive program development, with many more examples, see

60+`Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_

61+by Edwin Brady, available from `Manning <https://www.manning.com>`_.

62+

58Example Code

63Example Code

59============

64============

60

65

docs/tutorial/miscellany.rst−10

@@ -67,16 +67,6 @@ In the case that a proof is not found, it can be provided explicitly as normal:

67

68 head xs {p = ?headProof}

69

70−More generally, we can fill in implicit arguments with a default value

71−by annotating them with ``default``. The definition above is equivalent

72−to:

73−

74−.. code-block:: idris

75−

76− head : (xs : List a) ->

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

78− head (x :: xs) = x

79−

80Implicit conversions

70Implicit conversions

81====================

71====================

82

72

docs/tutorial/modules.rst+19−60

@@ -16,22 +16,28 @@ module which defines a binary tree type ``BTree`` (in a file

16

17 module Btree

18

19+ public export

19 data BTree a = Leaf

20 data BTree a = Leaf

20 | Node (BTree a) a (BTree a)

21 | Node (BTree a) a (BTree a)

21

22

23+ export

22 insert : Ord a => a -> BTree a -> BTree a

24 insert : Ord a => a -> BTree a -> BTree a

23 insert x Leaf = Node Leaf x Leaf

25 insert x Leaf = Node Leaf x Leaf

24 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

26 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

25 else (Node l v (insert x r))

27 else (Node l v (insert x r))

26

28

29+ export

27 toList : BTree a -> List a

30 toList : BTree a -> List a

28 toList Leaf = []

31 toList Leaf = []

29 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

32 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

30

33

34+ export

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

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

32 toTree [] = Leaf

36 toTree [] = Leaf

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

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

34

38

39+The modifiers ``export`` and ``public export`` say which names are visible

40+from other modules. These are explained further below.

35

41

36Then, this gives a main program (in a file

42Then, this gives a main program (in a file

37``bmain.idr``) which uses the ``Btree`` module to sort a list:

43``bmain.idr``) which uses the ``Btree`` module to sort a list:

@@ -46,11 +52,9 @@ Then, this gives a main program (in a file

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

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

47 print (Btree.toList t)

53 print (Btree.toList t)

48

54

49−

50−

51−The same names can be defined in multiple modules. This is possible

55+The same names can be defined in multiple modules: names are *qualified* with

52−because in practice names are *qualified* with the name of the module.

53−The names defined in the ``Btree`` module are, in full:

56+the name of the module. The names defined in the ``Btree`` module are, in

57+full:

54

58

55+ ``Btree.BTree``

59+ ``Btree.BTree``

56+ ``Btree.Leaf``

60+ ``Btree.Leaf``

@@ -115,6 +119,10 @@ Meaning for Functions

115 the module. Otherwise, Idris won't know what the synonym is a

119 the module. Otherwise, Idris won't know what the synonym is a

116 synonym for.

120 synonym for.

117

121

122+Since ``public export`` means that a function's definition is exported,

123+this effectively makes the function definition part of the module's API.

124+Therefore, it's generally a good idea to avoid using ``public export`` for

125+functions unless you really mean to export the full definition.

118

126

119Meaning for Data Types

127Meaning for Data Types

120----------------------

128----------------------

@@ -136,41 +144,10 @@ For interfaces, the meanings are:

136- ``public export`` the interface name, method names and default

144- ``public export`` the interface name, method names and default

137 definitions are exported

145 definitions are exported

138

146

139−

140−

141−``BTree`` Revisited

142−+++++++++++++++++++

143−

144−For our ``BTree`` module, it makes sense for the tree data type and the

145−functions to be exported as ``export``, as we see below:

146−

147−.. code-block:: idris

148−

149− module BTree

150−

151− export data BTree a = Leaf

152− | Node (BTree a) a (BTree a)

153−

154− export

155− insert : Ord a => a -> BTree a -> BTree a

156− insert x Leaf = Node Leaf x Leaf

157− insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

158− else (Node l v (insert x r))

159−

160− export

161− toList : BTree a -> List a

162− toList Leaf = []

163− toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

164−

165− export

166− toTree : Ord a => List a -> BTree a

167− toTree [] = Leaf

168− toTree (x :: xs) = insert x (toTree xs)

169−

170``%access`` Directive

147``%access`` Directive

171----------------------

148----------------------

172

149

173−Finally, the default export mode can be changed with the ``%access``

150+The default export mode can be changed with the ``%access``

174directive, for example:

151directive, for example:

175

152

176.. code-block:: idris

153.. code-block:: idris

@@ -179,8 +156,9 @@ directive, for example:

179

156

180 %access export

157 %access export

181

158

159+ public export

182 data BTree a = Leaf

160 data BTree a = Leaf

183− | Node (BTree a) a (BTree a)

161+ | Node (BTree a) a (BTree a)

184

162

185 insert : Ord a => a -> BTree a -> BTree a

163 insert : Ord a => a -> BTree a -> BTree a

186 insert x Leaf = Node Leaf x Leaf

164 insert x Leaf = Node Leaf x Leaf

@@ -237,14 +215,14 @@ wish to overload names within the same module:

237 test x = x ++ x

215 test x = x ++ x

238

216

239This (admittedly contrived) module defines two functions with fully

217This (admittedly contrived) module defines two functions with fully

240−qualified names ``foo.x.test`` and ``foo.y.test``, which can be

218+qualified names ``Foo.x.test`` and ``Foo.y.test``, which can be

241disambiguated by their types:

219disambiguated by their types:

242

220

243::

221::

244

222

245− *foo> test 3

223+ *Foo> test 3

246 6 : Int

224 6 : Int

247− *foo> test "foo"

225+ *Foo> test "foo"

248 "foofoo" : String

226 "foofoo" : String

249

227

250Parameterised blocks

228Parameterised blocks

@@ -301,22 +279,3 @@ which can be inferred by the type checker:

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

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

302

280

303

281

304−Modules Dependencies Using Atom

305−===============================

306−

307−If you are using the Atom editor and have a dependency on another package,

308−corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,

309−you need to let Atom know that it should be loaded. The easiest way to

310−accomplish that is with a .ipkg file. The general contents of an ipkg file

311−will be described in the next section of the tutorial, but for now here is

312−a simple recipe for this trivial case.

313−

314−- Create a folder myProject.

315−

316−- Add a file myProject.ipkg containing just a couple of lines:

317−

318−``package myProject``

319−

320−``pkgs = pruviloj, lightyear``

321−

322−- In Atom, use the File menu to Open Folder myProject.

docs/tutorial/packages.rst+20

@@ -146,6 +146,26 @@ The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

146Note how both tests have reported success by printing ``Test Passed``

147as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

148

149+Package Dependencies Using Atom

150+===============================

151+

152+If you are using the Atom editor and have a dependency on another package,

153+corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,

154+you need to let Atom know that it should be loaded. The easiest way to

155+accomplish that is with a .ipkg file. The general contents of an ipkg file

156+will be described in the next section of the tutorial, but for now here is

157+a simple recipe for this trivial case.

158+

159+- Create a folder myProject.

160+

161+- Add a file myProject.ipkg containing just a couple of lines:

162+

163+``package myProject``

164+

165+``pkgs = pruviloj, lightyear``

166+

167+- In Atom, use the File menu to Open Folder myProject.

168+

149More information

169More information

150================

170================

151

171

docs/tutorial/starting.rst+2−1

@@ -10,7 +10,8 @@ Prerequisites

10Before installing Idris, you will need to make sure you have all

11of the necessary libraries and tools. You will need:

12

13−- A fairly recent Haskell platform. Version ``2013.2.0.0`` should be sufficiently recent, though it is better to be completely up to date.

13+- A fairly recent version of `GHC <https://www.haskell.org/ghc/>`_. The

14+ earliest version we currently test with is 7.6.3.

14

15

15- The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.

16- The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.

16

17

docs/tutorial/theorems.rst+141−2

@@ -122,6 +122,145 @@ Idris provides interactive editing capabilities, which can help with

122building proofs. For more details on building proofs interactively in

123an editor, see :ref:`proofs-index`.

124

125+.. _sect-parity:

126+

127+Theorems in Practice

128+====================

129+

130+The need to prove theorems can arise naturally in practice. For example,

131+previously (:ref:`sec-views`) we implemented ``natToBin`` using a function

132+``parity``:

133+

134+.. code-block:: idris

135+

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

137+

138+However, we didn't provide a definition for ``parity``. We might expect it

139+to look something like the following:

140+

141+.. code-block:: idris

142+

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

144+ parity Z = Even {n=Z}

145+ parity (S Z) = Odd {n=Z}

146+ parity (S (S k)) with (parity k)

147+ parity (S (S (j + j))) | Even = Even {n=S j}

148+ parity (S (S (S (j + j)))) | Odd = Odd {n=S j}

149+

150+Unfortunately, this fails with a type error:

151+

152+::

153+

154+ When checking right hand side of with block in views.parity with expected type

155+ Parity (S (S (j + j)))

156+

157+ Type mismatch between

158+ Parity (S j + S j) (Type of Even)

159+ and

160+ Parity (S (S (plus j j))) (Expected type)

161+

162+The problem is that normalising ``S j + S j``, in the type of ``Even``

163+doesn't result in what we need for the type of the right hand side of

164+``Parity``. We know that ``S (S (plus j j))`` is going to be equal to

165+``S j + S j``, but we need to explain it to Idris with a proof. We can

166+begin by adding some *holes* (see :ref:`sect-holes`) to the definition:

167+

168+.. code-block:: idris

169+

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

171+ parity Z = Even {n=Z}

172+ parity (S Z) = Odd {n=Z}

173+ parity (S (S k)) with (parity k)

174+ parity (S (S (j + j))) | Even = let result = Even {n=S j} in

175+ ?helpEven

176+ parity (S (S (S (j + j)))) | Odd = let result = Odd {n=S j} in

177+ ?helpOdd

178+

179+Checking the type of ``helpEven`` shows us what we need to prove for the

180+``Even`` case:

181+

182+::

183+

184+ j : Nat

185+ result : Parity (S (plus j (S j)))

186+ --------------------------------------

187+ helpEven : Parity (S (S (plus j j)))

188+

189+We can therefore write a helper function to *rewrite* the type to the form

190+we need:

191+

192+.. code-block:: idris

193+

194+ helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))

195+ helpEven j p = rewrite plusSuccRightSucc j j in p

196+

197+The ``rewrite ... in`` syntax allows you to change the required type of an

198+expression by rewriting it according to an equality proof. Here, we have

199+used ``plusSuccRightSucc``, which has the following type:

200+

201+.. code-block:: idris

202+

203+ plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right

204+

205+We can see the effect of ``rewrite`` by replacing the right hand side of

206+``helpEven`` with a hole, and working step by step. Beginning with the following:

207+

208+.. code-block:: idris

209+

210+ helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))

211+ helpEven j p = ?helpEven_rhs

212+

213+We can look at the type of ``helpEven_rhs``:

214+

215+.. code-block:: idris

216+

217+ j : Nat

218+ p : Parity (S (plus j (S j)))

219+ --------------------------------------

220+ helpEven_rhs : Parity (S (S (plus j j)))

221+

222+Then we can ``rewrite`` by applying ``plusSuccRightSucc j j``, which gives

223+an equation ``S (j + j) = j + S j``, thus replacing ``S (j + j)`` (or,

224+in this case, ``S (plus j j)`` since ``S (j + j)`` reduces to that) in the

225+type with ``j + S j``:

226+

227+.. code-block:: idris

228+

229+ helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))

230+ helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs

231+

232+Checking the type of ``helpEven_rhs`` now shows what has happened, including

233+the type of the equation we just used (as the type of ``_rewrite_rule``):

234+

235+.. code-block:: idris

236+

237+ j : Nat

238+ p : Parity (S (plus j (S j)))

239+ _rewrite_rule : S (plus j j) = plus j (S j)

240+ --------------------------------------

241+ helpEven_rhs : Parity (S (plus j (S j)))

242+

243+Using ``rewrite`` and another helper for the ``Odd`` case, we can complete

244+``parity`` as follows:

245+

246+.. code-block:: idris

247+

248+ helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))

249+ helpEven j p = rewrite plusSuccRightSucc j j in p

250+

251+ helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))

252+ helpOdd j p = rewrite plusSuccRightSucc j j in p

253+

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

255+ parity Z = Even {n=Z}

256+ parity (S Z) = Odd {n=Z}

257+ parity (S (S k)) with (parity k)

258+ parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})

259+ parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})

260+

261+Full details of ``rewrite`` are beyond the scope of this introductory tutorial,

262+but it is covered in the theorem proving tutorial (see :ref:`proofs-index`).

263+

125.. _sect-totality:

264.. _sect-totality:

126

265

127Totality Checking

266Totality Checking

@@ -151,10 +290,10 @@ definitions is total:

151

290

152::

291::

153

292

154− *theorems> :total empty1

293+ *Theorems> :total empty1

155 possibly not total due to: empty1#hd

294 possibly not total due to: empty1#hd

156 not total as there are missing cases

295 not total as there are missing cases

157− *theorems> :total empty2

296+ *Theorems> :total empty2

158 possibly not total due to recursive path empty2

297 possibly not total due to recursive path empty2

159

298

160Note the use of the word “possibly” — a totality check can, of course,

299Note the use of the word “possibly” — a totality check can, of course,

docs/tutorial/typesfuns.rst+128−122

@@ -250,17 +250,65 @@ So, for example, the following definitions are legal:

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

251 where z w = y + w

252

253+.. _sect-holes:

254+

255+Holes

256+-----

257+

258+Idris programs can contain *holes* which stand for incomplete parts of

259+programs. For example, we could leave a hole for the greeting in our

260+"Hello world" program:

261+

262+.. code-block:: idris

263+

264+ main : IO ()

265+ main = putStrLn ?greeting

266+

267+The syntax ``?greeting`` introduces a hole, which stands for a part of

268+a program which is not yet written. This is a valid Idris program, and you

269+can check the type of ``greeting``:

270+

271+::

272+

273+ *Hello> :t greeting

274+ --------------------------------------

275+ greeting : String

276+

277+Checking the type of a hole also shows the types of any variables in scope.

278+For example, given an incomplete definition of ``even``:

279+

280+.. code-block:: idris

281+

282+ even : Nat -> Bool

283+ even Z = True

284+ even (S k) = ?even_rhs

285+

286+We can check the type of ``even_rhs`` and see the expected return type,

287+and the type of the variable ``k``:

288+

289+::

290+

291+ *Even> :t even_rhs

292+ k : Nat

293+ --------------------------------------

294+ even_rhs : Bool

295+

296+Holes are useful because they help us write functions *incrementally*.

297+Rather than writing an entire function in one go, we can leave some parts

298+unwritten and use Idris to tell us what is necessary to complete the

299+definition.

253

300

254Dependent Types

301Dependent Types

255===============

302===============

256

303

304+.. _sect-fctypes:

305+

257First Class Types

306First Class Types

258-----------------

307-----------------

259

308

260−In Idris, types are a first class language construct, meaning that they

309+In Idris, types are first class, meaning that they can be computed and

261−can be computed and manipulated (and passed to functions) just like any

310+manipulated (and passed to functions) just like any other language construct.

262−other language construct. For example, we could write a function which

311+For example, we could write a function which computes a type:

263−computes a type:

264

312

265.. code-block:: idris

313.. code-block:: idris

266

314

@@ -350,19 +398,22 @@ following:

350

398

351::

399::

352

400

353− $ idris vbroken.idr --check

401+ $ idris VBroken.idr --check

402+ VBroken.idr:9:23-25:

354− vbroken.idr:9:23:When elaborating right hand side of Vect.++:

403+ When checking right hand side of Vect.++ with expected type

355− When elaborating an application of constructor Vect.:::

404+ Vect (S k + m) a

356− Type mismatch between

357− Vect (k + k) a (Type of xs ++ xs)

358− and

359− Vect (plus k m) a (Expected type)

360

405

406+ When checking an application of constructor Vect.:::

407+ Type mismatch between

408+ Vect (k + k) a (Type of xs ++ xs)

409+ and

410+ Vect (plus k m) a (Expected type)

411+

361− Specifically:

412+ Specifically:

362− Type mismatch between

413+ Type mismatch between

363− plus k k

414+ plus k k

364− and

415+ and

365− plus k m

416+ plus k m

366

417

367

418

368This error message suggests that there is a length mismatch between

419This error message suggests that there is a length mismatch between

@@ -656,9 +707,9 @@ not always the best approach. Consider the following function:

656

707

657.. code-block:: idris

708.. code-block:: idris

658

709

659− ifThenElse : Bool -> a -> a -> a;

710+ ifThenElse : Bool -> a -> a -> a

660− ifThenElse True t e = t;

711+ ifThenElse True t e = t

661− ifThenElse False t e = e;

712+ ifThenElse False t e = e

662

713

663This function uses one of the ``t`` or ``e`` arguments, but not both

714This function uses one of the ``t`` or ``e`` arguments, but not both

664(in fact, this is used to implement the ``if...then...else`` construct

715(in fact, this is used to implement the ``if...then...else`` construct

@@ -681,19 +732,19 @@ without any explicit use of ``Force`` or ``Delay``:

681

732

682.. code-block:: idris

733.. code-block:: idris

683

734

684− ifThenElse : Bool -> Lazy a -> Lazy a -> a;

735+ ifThenElse : Bool -> Lazy a -> Lazy a -> a

685− ifThenElse True t e = t;

736+ ifThenElse True t e = t

686− ifThenElse False t e = e;

737+ ifThenElse False t e = e

687

738

688Codata Types

739Codata Types

689============

740============

690

741

691−Codata types are like regular data types, except that they allow for us to

692−define infinite data structures. More precisely, for a type ``T``, each of its

742+Codata types allow us to define infinite data structures by marking recursive

743+arguments as potentially infinite. For

693−constructor arguments of type ``T`` are transformed into a coinductive parameter

744+a codata type ``T``, each of its constructor arguments of type ``T`` are transformed

694−``Inf T``. This makes each of the ``T`` arguments lazy, and allows infinite data

745+into an argument of type ``Inf T``. This makes each of the ``T`` arguments

695−structures of type ``T`` to be built. One example of a codata type is Stream,

746+lazy, and allows infinite data structures of type ``T`` to be built. One

696−which is defined as follows.

747+example of a codata type is Stream, which is defined as follows.

697

748

698.. code-block:: idris

749.. code-block:: idris

699

750

@@ -778,7 +829,8 @@ Useful Data Types

778=================

829=================

779

830

780Idris includes a number of useful data types and library functions

831Idris includes a number of useful data types and library functions

781−(see the ``libs/`` directory in the distribution). This chapter

832+(see the ``libs/`` directory in the distribution, and the

833+`documentation <https://www.idris-lang.org/documentation/>`_). This section

782describes a few of these. The functions described here are imported

834describes a few of these. The functions described here are imported

783automatically by every Idris program, as part of ``Prelude.idr``.

835automatically by every Idris program, as part of ``Prelude.idr``.

784

836

@@ -836,7 +888,7 @@ the vector:

836

888

837::

889::

838

890

839− *usefultypes> show (map double intVec)

891+ *UsefulTypes> show (map double intVec)

840 "[2, 4, 6, 8, 10]" : String

892 "[2, 4, 6, 8, 10]" : String

841

893

842For more details of the functions available on ``List`` and

894For more details of the functions available on ``List`` and

@@ -850,9 +902,7 @@ For more details of the functions available on ``List`` and

850

902

851- ``libs/base/Data/VectType.idr``

903- ``libs/base/Data/VectType.idr``

852

904

853−Functions include filtering, appending, reversing, and so on. Also

905+Functions include filtering, appending, reversing, and so on.

854−remember that Idris is still in development, so if you don’t see

855−the function you need, please feel free to add it and submit a patch!

856

906

857Aside: Anonymous functions and operator sections

907Aside: Anonymous functions and operator sections

858~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

908~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -862,7 +912,7 @@ would be to use an anonymous function:

862

912

863::

913::

864

914

865− *usefultypes> show (map (\x => x * 2) intVec)

915+ *UsefulTypes> show (map (\x => x * 2) intVec)

866 "[2, 4, 6, 8, 10]" : String

916 "[2, 4, 6, 8, 10]" : String

867

917

868The notation ``\x => val`` constructs an anonymous function which takes

918The notation ``\x => val`` constructs an anonymous function which takes

@@ -874,7 +924,7 @@ e.g. ``\(x, y) => x + y``. We could also use an operator section:

874

924

875::

925::

876

926

877− *usefultypes> show (map (* 2) intVec)

927+ *UsefulTypes> show (map (* 2) intVec)

878 "[2, 4, 6, 8, 10]" : String

928 "[2, 4, 6, 8, 10]" : String

879

929

880``(*2)`` is shorthand for a function which multiplies a number

930``(*2)`` is shorthand for a function which multiplies a number

@@ -938,19 +988,18 @@ contain an arbitrary number of values, represented as nested pairs:

938

988

939::

989::

940

990

941− *usefultypes> fst jim

991+ *UsefulTypes> fst jim

942 "Jim" : String

992 "Jim" : String

943− *usefultypes> snd jim

993+ *UsefulTypes> snd jim

944 (25, "Cambridge") : (Int, String)

994 (25, "Cambridge") : (Int, String)

945− *usefultypes> jim == ("Jim", (25, "Cambridge"))

995+ *UsefulTypes> jim == ("Jim", (25, "Cambridge"))

946 True : Bool

996 True : Bool

947

997

948Dependent Pairs

998Dependent Pairs

949---------------

999---------------

950

1000

951Dependent pairs allow the type of the second element of a pair to depend

1001Dependent pairs allow the type of the second element of a pair to depend

952−on the value of the first element. Traditionally, these are referred to

1002+on the value of the first element.

953−as “sigma types”:

954

1003

955.. code-block:: idris

1004.. code-block:: idris

956

1005

@@ -1021,6 +1070,7 @@ intermediate values:

1021

1070

1022We will see more on ``with`` notation later.

1071We will see more on ``with`` notation later.

1023

1072

1073+Dependent pairs are sometimes referred to as “sigma types”.

1024

1074

1025Records

1075Records

1026-------

1076-------

@@ -1052,11 +1102,11 @@ can be used to access the field values:

1052

1102

1053::

1103::

1054

1104

1055− *record> firstName fred

1105+ *Record> firstName fred

1056 "Fred" : String

1106 "Fred" : String

1057− *record> age fred

1107+ *Record> age fred

1058 30 : Int

1108 30 : Int

1059− *record> :t firstName

1109+ *Record> :t firstName

1060 firstName : Person -> String

1110 firstName : Person -> String

1061

1111

1062We can also use the field names to update a record (or, more

1112We can also use the field names to update a record (or, more

@@ -1065,9 +1115,9 @@ updated):

1065

1115

1066.. code-block:: bash

1116.. code-block:: bash

1067

1117

1068− *record> record { firstName = "Jim" } fred

1118+ *Record> record { firstName = "Jim" } fred

1069 MkPerson "Jim" "Joe" "Bloggs" 30 : Person

1119 MkPerson "Jim" "Joe" "Bloggs" 30 : Person

1070− *record> record { firstName = "Jim", age $= (+ 1) } fred

1120+ *Record> record { firstName = "Jim", age $= (+ 1) } fred

1071 MkPerson "Jim" "Joe" "Bloggs" 31 : Person

1121 MkPerson "Jim" "Joe" "Bloggs" 31 : Person

1072

1122

1073The syntax ``record { field = val, ... }`` generates a function which

1123The syntax ``record { field = val, ... }`` generates a function which

@@ -1098,9 +1148,15 @@ length because it will not affect the type of the record:

1098

1148

1099::

1149::

1100

1150

1101− *record> addStudent fred (ClassInfo [] "CS")

1151+ *Record> addStudent fred (ClassInfo [] "CS")

1102 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class

1152 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class

1103

1153

1154+We could also use ``$=`` to define ``addStudent`` more concisely:

1155+

1156+.. code-block:: idris

1157+

1158+ addStudent' : Person -> Class -> Class

1159+ addStudent' p c = record { students $= (p ::) } c

1104

1160

1105Nested record update

1161Nested record update

1106~~~~~~~~~~~~~~~~~~~~

1162~~~~~~~~~~~~~~~~~~~~

@@ -1123,12 +1179,13 @@ can also be accessed with the following syntax:

1123

1179

1124 record { a->b->c } x

1180 record { a->b->c } x

1125

1181

1182+The ``$=`` notation is also valid for nested record updates.

1126

1183

1127Dependent Records

1184Dependent Records

1128-----------------

1185-----------------

1129

1186

1130−Records can also be dependent on values. Records *parameters*, which

1187+Records can also be dependent on values. Records have *parameters*, which

1131−are not subject to field updates. The parameters appear as arguments

1188+cannot be updated like the other fields. The parameters appear as arguments

1132to the resulting type, and are written following the record type

1189to the resulting type, and are written following the record type

1133name. For example, a pair type could be defined as follows:

1190name. For example, a pair type could be defined as follows:

1134

1191

@@ -1140,10 +1197,9 @@ name. For example, a pair type could be defined as follows:

1140 snd : b

1197 snd : b

1141

1198

1142

1199

1143−Using the class record from the original introduction to records. The

1200+Using the ``class`` record from earlier, the size of the class can be

1144−size of the class can be restricted using a ``Vect`` and the size

1201+restricted using a ``Vect`` and the size included in the type by parameterising

1145−promoted to the type level by parameterising the record with the size.

1146−For example:

1202+the record with the size. For example:

1147

1203

1148

1204

1149.. code-block:: idris

1205.. code-block:: idris

@@ -1258,9 +1314,9 @@ we get a default value:

1258

1314

1259::

1315::

1260

1316

1261− *usefultypes> lookup_default 2 [3,4,5,6] (-1)

1317+ *UsefulTypes> lookup_default 2 [3,4,5,6] (-1)

1262 5 : Integer

1318 5 : Integer

1263− *usefultypes> lookup_default 4 [3,4,5,6] (-1)

1319+ *UsefulTypes> lookup_default 4 [3,4,5,6] (-1)

1264 -1 : Integer

1320 -1 : Integer

1265

1321

1266**Restrictions:** The ``case`` construct is intended for simple

1322**Restrictions:** The ``case`` construct is intended for simple

@@ -1278,75 +1334,25 @@ matching ``let`` and lambda bindings. It will *only* work if:

1278Totality

1334Totality

1279========

1335========

1280

1336

1337+Idris distinguishes between *total* and *partial* functions.

1281−A *total* function is a function that terminates for all possible

1338+A total function is a function that either:

1282−inputs, or one that is guaranteed to produce some output before making

1283−a recursive call. For example, Idris' ``head`` function is total for

1284−all lists:

1285−

1286−::

1287−

1288− Idris> :t Prelude.List.head

1289− head : (l : List a) -> {auto ok : NonEmpty l} -> a

1290−

1291−The ``{auto ok : NonEmpty l}`` tells us that Idris won't compile if we

1292−try to call ``head`` on an empty list. The implementation is as follows:

1293−

1294−.. code-block:: idris

1295−

1296− ||| Get the first element of a non-empty list

1297− ||| @ ok proof that the list is non-empty

1298− head : (l : List a) -> {auto ok : NonEmpty l} -> a

1299− head [] {ok=IsNonEmpty} impossible

1300− head (x::xs) {ok=p} = x

1301−

1302−(Note that this implementation is in contrast to Haskell's ``head``,

1303−which is *not* total and will fail at runtime rather than compile time.)

1304−The following Idris code will compile:

1305−

1306−.. code-block:: idris

1307−

1308− module Main

1309

1339

1310− main : IO ()

1340++ Terminates for all possible inputs, or

1311− main = do

1341++ Produces a non-empty, finite, prefix of a possibly infinite result

1312− let x : Integer = head [1,2,3]

1313− print x

1314−

1315−And will print ``1``. However, the same code with ``head []`` won't compile:

1316−

1317−::

1318−

1319− test.idr:5:26:When checking right hand side of main with expected type

1320− IO ()

1321−

1322− When checking argument ok to function Prelude.List.head:

1323− Can't find a value of type

1324− NonEmpty []

1325−

1326−We can't bind and print ``x`` because ``head []`` doesn't type check.

1327

1342

1328−However, we might imagine a function, ``unsafeHead``, that is identical to

1343+If a function is total, we can consider its type a precise description of what

1329−Idris' ``head`` function except that it is *not* total: it will error out

1344+that function will do. For example, if we have a function with a return

1330−at runtime if called on an empty list. (This is similar to the behavior of

1345+type of ``String`` we know something different, depending on whether or not

1331−Haskell's ``head`` function.) ``unsafeHead`` might look like this:

1346+it's total:

1332−

1333−.. code-block:: idris

1334−

1335− -- Unsafe head example!

1336− unsafeHead : List a -> a

1337− unsafeHead (x::xs) = x

1338−

1339−And although it typechecks and compiles, it will not reduce (that is, evaluation

1340−of the function will cause it to change):

1341−

1342−::

1343

1347

1344− unsafe> the Integer $ unsafeHead [1, 2, 3]

1348++ If it's total, it will return a value of type ``String`` in finite time

1345− 1 : Integer

1349++ If it's partial, then as long as it doesn't crash or enter an infinite loop,

1346− unsafe> the Integer $ unsafeHead []

1350+ it will return a ``String``.

1347− unsafeHead [] : Integer

1348

1351

1349−Functions that are not total are known as *partial functions*. As

1352+Idris makes this distinction so that it knows which functions are safe to

1350−mentioned in the note about ``mutual`` blocks, non-total definitions

1353+evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,

1351−aren't reduced when type checking because they are not well-defined

1354+if it tries to evaluate a function during type checking which doesn't

1352−for all possible inputs.

1355+terminate, then type checking won't terminate!

1356+Therefore, only total functions will be evaluated during type checking.

1357+Partial functions can still be used in types, but will not be evaluated

1358+further.

docs/tutorial/views.rst+1−1

@@ -89,7 +89,7 @@ a function in the patterns (``+``) and repeated occurrences of

89``j``—this is allowed because another argument has determined the form

90of these patterns.

91

92−We will return to this function in Section :ref:`sect-provisional` to

92+We will return to this function in the next section :ref:`sect-parity` to

93complete the definition of ``parity``.

94

95With and proofs

samples/tutorial/bmain.idr → samples/tutorial/BMain.idrrenamed+2−2

@@ -1,8 +1,8 @@

1module Main

2

3−import btree

3+import BTree

4

5main : IO ()

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

7− print (btree.toList t)

7+ printLn (btree.toList t)

8

samples/tutorial/btree.idr → samples/tutorial/BTree.idrrenamed+4

@@ -1,17 +1,21 @@

1module btree

2

3+public export

3data BTree a = Leaf

4data BTree a = Leaf

4 | Node (BTree a) a (BTree a)

5 | Node (BTree a) a (BTree a)

5

6

7+export

6insert : Ord a => a -> BTree a -> BTree a

8insert : Ord a => a -> BTree a -> BTree a

7insert x Leaf = Node Leaf x Leaf

9insert x Leaf = Node Leaf x Leaf

8insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

10insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

9 else (Node l v (insert x r))

11 else (Node l v (insert x r))

10

12

13+export

11toList : BTree a -> List a

14toList : BTree a -> List a

12toList Leaf = []

15toList Leaf = []

13toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

16toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

14

17

18+export

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

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

16toTree [] = Leaf

20toTree [] = Leaf

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

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

samples/tutorial/btreemod.idr → samples/tutorial/BTreeMod.idrrenamed

The content is the same.

samples/tutorial/foo.idr → samples/tutorial/Foo.idrrenamed

The content is the same.

samples/tutorial/hello.idr → samples/tutorial/Hello.idrrenamed

The content is the same.

samples/tutorial/idiom.idr → samples/tutorial/Idiom.idrrenamed

The content is the same.

samples/tutorial/classes.idr → samples/tutorial/Interfaces.idrrenamed

The content is the same.

samples/tutorial/interp.idr → samples/tutorial/Interp.idrrenamed+2−2

@@ -33,7 +33,7 @@ using (G : Vect n Ty)

33 Expr G c

34 If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a

35

36− interp : Env G -> %static (e : Expr G t) -> interpTy t

36+ interp : Env G -> (e : Expr G t) -> interpTy t

37 interp env (Var i) = lookup i env

38 interp env (Val x) = x

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

@@ -67,5 +67,5 @@ testFac = interp [] fact 4

67main : IO ()

68main = do putStr "Enter a number: "

69 x <- getLine

70− print (interp [] fact (cast x))

70+ printLn (interp [] fact (cast x))

71

samples/tutorial/letbind.idr → samples/tutorial/LetBind.idrrenamed+1−1

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

1−module letbind

1+module LetBind

2

3mirror : List a -> List a

4mirror xs = let xs' = reverse xs in

samples/tutorial/prims.idr → samples/tutorial/Prims.idrrenamed+1−1

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

1−module prims

1+module Prims

2

3x : Int

4x = 42

samples/tutorial/Record.idrnew file+21

@@ -0,0 +1,21 @@

1+import Data.Vect

2+

3+record Person where

4+ constructor MkPerson

5+ firstName, middleName, lastName : String

6+ age : Int

7+

8+fred : Person

9+fred = MkPerson "Fred" "Joe" "Bloggs" 30

10+

11+record Class where

12+ constructor ClassInfo

13+ students : Vect n Person

14+ className : String

15+

16+addStudent : Person -> Class -> Class

17+addStudent p c = record { students = p :: students c } c

18+

19+addStudent' : Person -> Class -> Class

20+addStudent' p c = record { students $= (p ::) } c

21+

samples/tutorial/theorems.idr → samples/tutorial/Theorems.idrrenamed−20

@@ -35,23 +35,3 @@ plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

35plusReducesS Z m = Refl

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

37

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

39−plusReducesZ' Z = ?plusredZ_Z

40−plusReducesZ' (S k) = let ih = plusReducesZ' k in

41− ?plusredZ_S

42−

43−

44−---------- Proofs ----------

45−

46−plusredZ_S = proof {

47− intro;

48− intro;

49− rewrite ih;

50− trivial;

51−}

52−

53−plusredZ_Z = proof {

54− compute;

55− trivial;

56−}

57−

samples/tutorial/universe.idr → samples/tutorial/Universe.idrrenamed

The content is the same.

samples/tutorial/usefultypes.idr → samples/tutorial/UsefulTypes.idrrenamed+1

@@ -1,3 +1,4 @@

1+import Data.Vect

1

2

2intVec : Vect 5 Int

3intVec : Vect 5 Int

3intVec = [1, 2, 3, 4, 5]

4intVec = [1, 2, 3, 4, 5]

samples/tutorial/vbroken.idr → samples/tutorial/VBroken.idrrenamed

The content is the same.

samples/tutorial/views.idr → samples/tutorial/Views.idrrenamed+8−20

@@ -4,12 +4,18 @@ data Parity : Nat -> Type where

4 Even : Parity (n + n)

5 Odd : Parity (S (n + n))

6

7+helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))

8+helpEven j p = rewrite plusSuccRightSucc j j in p

9+

10+helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))

11+helpOdd j p = rewrite plusSuccRightSucc j j in p

12+

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

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

8parity Z = Even {n=Z}

14parity Z = Even {n=Z}

9parity (S Z) = Odd {n=Z}

15parity (S Z) = Odd {n=Z}

10parity (S (S k)) with (parity k)

16parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | Even ?= Even {n=S j}

17+ parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})

12− parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

18+ parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})

13

19

14natToBin : Nat -> List Bool

20natToBin : Nat -> List Bool

15natToBin Z = Nil

21natToBin Z = Nil

@@ -17,21 +23,3 @@ natToBin k with (parity k)

17 natToBin (j + j) | Even = False :: natToBin j

23 natToBin (j + j) | Even = False :: natToBin j

18 natToBin (S (j + j)) | Odd = True :: natToBin j

24 natToBin (S (j + j)) | Odd = True :: natToBin j

19

25

20−

21−---------- Proofs ----------

22−

23−views.parity_lemma_2 = proof {

24− intro;

25− intro;

26− rewrite sym (plusSuccRightSucc j j);

27− trivial;

28−}

29−

30−views.parity_lemma_1 = proof {

31− intro;

32− intro;

33− rewrite sym (plusSuccRightSucc j j);

34− trivial;

35−}

36−

37−

samples/tutorial/viewsbroken.idr → samples/tutorial/ViewsBroken.idrrenamed

The content is the same.

samples/tutorial/wheres.idr → samples/tutorial/Wheres.idrrenamed+1−1

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

1−module wheres

1+module Wheres

2

3even : Nat -> Bool

4even Z = True

samples/tutorial/binary.idrdeleted−61

@@ -1,61 +0,0 @@

1−module Main

2−

3−data Binary : Nat -> Type where

4− bEnd : Binary Z

5− bO : Binary n -> Binary (n + n)

6− bI : Binary n -> Binary (S (n + n))

7−

8−implementation Show (Binary n) where

9− show (bO x) = show x ++ "0"

10− show (bI x) = show x ++ "1"

11− show bEnd = ""

12−

13−data Parity : Nat -> Type where

14− Even : Parity (n + n)

15− Odd : Parity (S (n + n))

16−

17−parity : (n:Nat) -> Parity n

18−parity Z = Even {n=Z}

19−parity (S Z) = Odd {n=Z}

20−parity (S (S k)) with (parity k)

21− parity (S (S (j + j))) | Even ?= Even {n=S j}

22− parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

23−

24−natToBin : (n:Nat) -> Binary n

25−natToBin Z = bEnd

26−natToBin (S k) with (parity k)

27− natToBin (S (j + j)) | Even = bI (natToBin j)

28− natToBin (S (S (j + j))) | Odd ?= bO (natToBin (S j))

29−

30−intToNat : Int -> Nat

31−intToNat 0 = Z

32−intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

33−

34−main : IO ()

35−main = do putStr "Enter a number: "

36− x <- getLine

37− print (natToBin (fromInteger (cast x)))

38−

39−---------- Proofs ----------

40−

41−Main.natToBin_lemma_1 = proof

42− intros

43− rewrite plusSuccRightSucc j j

44− rewrite sym (plusSuccRightSucc j j)

45− trivial

46−

47−

48−parity_lemma_1 = proof

49− intros

50− rewrite sym (plusSuccRightSucc j j)

51− trivial

52−

53−

54−parity_lemma_2 = proof {

55− intro;

56− intro;

57− rewrite sym (plusSuccRightSucc j j);

58− trivial;

59−}

60−

61−