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

git.iko.soy/Idris-dev

Refresh the tutorial

commit2c001c9bf18f69e281601404d0084a9292dc2980 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 31 Mar 2017, 18:45 (10 years ago) parent5fc838d

29 files changed+406−308

compare with master

unifiedsplit

docs/tutorial/index.rst+4−2

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

44The Idris Tutorial

55##################

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

7+This is the Idris Tutorial.

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.

811

912.. note::

1013 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

2730 interp

2831 views

2932 theorems

30− provisional

3133 interactive

3234 syntax

3335 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").

253253

254254::

255255

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

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

257257 Just 42 : Maybe Int

258− *ifaces> m_add (Just 20) Nothing

258+ *Interfaces> m_add (Just 20) Nothing

259259 Nothing : Maybe Int

260260

261261Pattern Matching Bind

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

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

567567

568568

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+

569612Determining Parameters

570613======================

571614

docs/tutorial/introduction.rst+5

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

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

5656dependent types for writing and verifying systems software.

5757

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+

5863Example Code

5964============

6065

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:

6767

6868 head xs {p = ?headProof}

6969

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−

8070Implicit conversions

8171====================

8272

docs/tutorial/modules.rst+19−60

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

1616

1717 module Btree

1818

19+ public export

1920 data BTree a = Leaf

2021 | Node (BTree a) a (BTree a)

2122

23+ export

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

2325 insert x Leaf = Node Leaf x Leaf

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

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

2628

29+ export

2730 toList : BTree a -> List a

2831 toList Leaf = []

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

3033

34+ export

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

3236 toTree [] = Leaf

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

3438

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

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

3541

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

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

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

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

4753 print (Btree.toList t)

4854

49−

50−

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

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

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

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

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

57+full:

5458

5559+ ``Btree.BTree``

5660+ ``Btree.Leaf``

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

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

116120 synonym for.

117121

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.

118126

119127Meaning for Data Types

120128----------------------

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

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

137145 definitions are exported

138146

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−

170147``%access`` Directive

171148----------------------

172149

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

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

174151directive, for example:

175152

176153.. code-block:: idris

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

179156

180157 %access export

181158

159+ public export

182160 data BTree a = Leaf

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

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

184162

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

186164 insert x Leaf = Node Leaf x Leaf

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

237215 test x = x ++ x

238216

239217This (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

241219disambiguated by their types:

242220

243221::

244222

245− *foo> test 3

223+ *Foo> test 3

246224 6 : Int

247− *foo> test "foo"

225+ *Foo> test "foo"

248226 "foofoo" : String

249227

250228Parameterised blocks

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

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

302280

303281

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``::

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

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

148148

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+

149169More information

150170================

151171

docs/tutorial/starting.rst+2−1

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

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

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

1212

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.

1415

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

1617

docs/tutorial/theorems.rst+141−2

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

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

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

124124

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+

125264.. _sect-totality:

126265

127266Totality Checking

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

151290

152291::

153292

154− *theorems> :total empty1

293+ *Theorems> :total empty1

155294 possibly not total due to: empty1#hd

156295 not total as there are missing cases

157− *theorems> :total empty2

296+ *Theorems> :total empty2

158297 possibly not total due to recursive path empty2

159298

160299Note 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:

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

251251 where z w = y + w

252252

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.

253300

254301Dependent Types

255302===============

256303

304+.. _sect-fctypes:

305+

257306First Class Types

258307-----------------

259308

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

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

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

263−computes a type:

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

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

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

264312

265313.. code-block:: idris

266314

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

350398

351399::

352400

353− $ idris vbroken.idr --check

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

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

356− Type mismatch between

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

358− and

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

401+ $ idris VBroken.idr --check

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

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

404+ Vect (S k + m) a

360405

361− Specifically:

362− Type mismatch between

363− plus k k

364− and

365− plus k m

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+

412+ Specifically:

413+ Type mismatch between

414+ plus k k

415+ and

416+ plus k m

366417

367418

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

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

656707

657708.. code-block:: idris

658709

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

660− ifThenElse True t e = t;

661− ifThenElse False t e = e;

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

711+ ifThenElse True t e = t

712+ ifThenElse False t e = e

662713

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

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

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

681732

682733.. code-block:: idris

683734

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

685− ifThenElse True t e = t;

686− ifThenElse False t e = e;

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

736+ ifThenElse True t e = t

737+ ifThenElse False t e = e

687738

688739Codata Types

689740============

690741

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

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

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

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

696−which is defined as follows.

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

743+arguments as potentially infinite. For

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

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

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

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

697748

698749.. code-block:: idris

699750

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

778829=================

779830

780831Idris 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

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

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

784836

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

836888

837889::

838890

839− *usefultypes> show (map double intVec)

891+ *UsefulTypes> show (map double intVec)

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

841893

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

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

850902

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

852904

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

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!

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

856906

857907Aside: Anonymous functions and operator sections

858908~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

862912

863913::

864914

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

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

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

867917

868918The 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:

874924

875925::

876926

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

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

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

879929

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

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

938988

939989::

940990

941− *usefultypes> fst jim

991+ *UsefulTypes> fst jim

942992 "Jim" : String

943− *usefultypes> snd jim

993+ *UsefulTypes> snd jim

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

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

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

946996 True : Bool

947997

948998Dependent Pairs

949999---------------

9501000

9511001Dependent 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

953−as “sigma types”:

1002+on the value of the first element.

9541003

9551004.. code-block:: idris

9561005

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

10211070

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

10231072

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

10241074

10251075Records

10261076-------

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

10521102

10531103::

10541104

1055− *record> firstName fred

1105+ *Record> firstName fred

10561106 "Fred" : String

1057− *record> age fred

1107+ *Record> age fred

10581108 30 : Int

1059− *record> :t firstName

1109+ *Record> :t firstName

10601110 firstName : Person -> String

10611111

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

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

10651115

10661116.. code-block:: bash

10671117

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

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

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

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

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

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

10721122

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

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

10981148

10991149::

11001150

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

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

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

11031153

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

11041160

11051161Nested record update

11061162~~~~~~~~~~~~~~~~~~~~

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

11231179

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

11251181

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

11261183

11271184Dependent Records

11281185-----------------

11291186

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

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

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

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

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

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

11341191

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

11401197 snd : b

11411198

11421199

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

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

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

1146−For example:

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

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

1202+the record with the size. For example:

11471203

11481204

11491205.. code-block:: idris

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

12581314

12591315::

12601316

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

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

12621318 5 : Integer

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

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

12641320 -1 : Integer

12651321

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

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

12781334Totality

12791335========

12801336

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

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

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

1338+A total function is a function that either:

13091339

1310− main : IO ()

1311− main = do

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.

1340++ Terminates for all possible inputs, or

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

13271342

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

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

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

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

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+If a function is total, we can consider its type a precise description of what

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

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

1346+it's total:

13431347

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

1345− 1 : Integer

1346− unsafe> the Integer $ unsafeHead []

1347− unsafeHead [] : Integer

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

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

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

13481351

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

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

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

1352−for all possible inputs.

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

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

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

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

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

9090of these patterns.

9191

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

9393complete the definition of ``parity``.

9494

9595With and proofs

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

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

11module Main

3−import btree

3+import BTree

55main : IO ()

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

7− print (btree.toList t)

7+ printLn (btree.toList t)

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

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

11module btree

3+public export

34data BTree a = Leaf

45 | Node (BTree a) a (BTree a)

7+export

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

79insert x Leaf = Node Leaf x Leaf

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

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

1012

13+export

1114toList : BTree a -> List a

1215toList Leaf = []

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

1417

18+export

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

1620toTree [] = Leaf

1721toTree (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)

3333 Expr G c

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

3535

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

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

3737 interp env (Var i) = lookup i env

3838 interp env (Val x) = x

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

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

6767main : IO ()

6868main = do putStr "Enter a number: "

6969 x <- getLine

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

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

7171

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

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

1−module letbind

1+module LetBind

33mirror : List a -> List a

44mirror 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

33x : Int

44x = 42

samples/tutorial/Record.idrnew file+21

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

1+import Data.Vect

3+record Person where

4+ constructor MkPerson

5+ firstName, middleName, lastName : String

6+ age : Int

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)

3535plusReducesS Z m = Refl

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

3737

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

23intVec : Vect 5 Int

34intVec = [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

44 Even : Parity (n + n)

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

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

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+

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

814parity Z = Even {n=Z}

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

1016parity (S (S k)) with (parity k)

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

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

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

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

1319

1420natToBin : Nat -> List Bool

1521natToBin Z = Nil

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

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

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

1925

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

33even : Nat -> Bool

44even 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−