87039fb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Heading normalisation, and reST usage fixes.

+ Fixed minor reST inconsistencies. + Normalised syntax used for headers to become inline with the [convention used for Python](http://sphinx.readthedocs.org/en/latest/rest.html#sections)

commit87039fb0a7376392ea86248d756fbc1e83068fbc authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateMon 30 Mar 2015, 21:59 (12 years ago) parent5c8c1d3

34 files changed+277−268

compare with master

unifiedsplit

docs/effects/conclusions.rst+2−2 docs/effects/depeff.rst+6−6 docs/effects/hangman.rst+10−10 docs/effects/impleff.rst+9−10 docs/effects/introduction.rst+2−2 docs/effects/simpleeff.rst+13−13 docs/effects/state.rst+8−8 docs/effects/summary.rst+9−9 docs/faq/faq.rst+12−12 docs/guides/type-providers-ffi.rst+12−11 docs/index.rst+2−1 docs/proofs/inductive.rst+6−5 docs/proofs/interactive.rst+4−5 docs/proofs/patterns.rst+7−6 docs/proofs/pluscomm.rst+7−6 docs/reference/documenting.rst+4−4 docs/reference/erasure.rst+21−20 docs/reference/ffi.rst+8−7 docs/reference/uniqueness-types.rst+5−4 docs/tutorial/classes.rst+12−12 docs/tutorial/conclusions.rst+2−2 docs/tutorial/index.rst+3−3 docs/tutorial/interactive.rst+10−10 docs/tutorial/interp.rst+7−7 docs/tutorial/introduction.rst+4−4 docs/tutorial/miscellany.rst+17−17 docs/tutorial/modules.rst+5−5 docs/tutorial/packages.rst+4−4 docs/tutorial/provisional.rst+5−5 docs/tutorial/starting.rst+5−5 docs/tutorial/syntax.rst+11−8 docs/tutorial/theorems.rst+12−12 docs/tutorial/typesfuns.rst+29−29 docs/tutorial/views.rst+4−4

docs/effects/conclusions.rst+2−2

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

11.. _sect-further:

3−===============

3+***************

44Further Reading

5−===============

5+***************

77This tutorial has given an introduction to writing and reasoning about

88side-effecting programs in Idris, using the ``Effects`` library.

docs/effects/depeff.rst+6−6

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

11.. _sect-depeff:

3−=================

3+*****************

44Dependent Effects

5−=================

5+*****************

77In the programs we have seen so far, the available effects have remained

88constant. Sometimes, however, an operation can *change* the available

@@ -16,7 +16,7 @@ we will see how this can be used to implement a type-safe and

1616resource-safe protocol for file management.

1717

1818Dependent States

19−----------------

19+================

2020

2121Suppose we have a function which reads input from the console, converts

2222it to an integer, and adds it to a list which is stored in a ``STATE``.

@@ -59,7 +59,7 @@ It has the following type:

5959 putM : y -> { [STATE x] ==> [STATE y] } Eff ()

6060

6161Result-dependent Effects

62−------------------------

62+========================

6363

6464Often, whether a state is updated could depend on the success or

6565otherwise of an operation. In our ``readInt`` example, we might wish to

@@ -134,7 +134,7 @@ check (i.e. whether reading a value succeeded) has indeed been done.

134134 being inspected in the type of each branch.

135135

136136File Management

137−---------------

137+===============

138138

139139A practical use for dependent effects is in specifying resource usage

140140protocols and verifying that they are executed correctly. For example,

@@ -242,7 +242,7 @@ reading, but the effect list contains a ``FILE_IO`` effect carrying a

242242file open for writing.

243243

244244Pattern-matching bind

245−---------------------

245+=====================

246246

247247It might seem that having to test each potentially failing operation

248248with a ``case`` clause could lead to ugly code, with lots of

docs/effects/hangman.rst+10−10

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

11.. _sect-hangman:

3−=======================================

3+***************************************

44Example: A “Mystery Word” Guessing Game

5−=======================================

5+***************************************

77In this section, we will use the techniques and specific effects

88discussed in the tutorial so far to implement a larger example, a simple

@@ -29,7 +29,7 @@ using the newly defined effect (and any others required to implement the

2929interface).

3030

3131Step 1: Game State

32−------------------

32+==================

3333

3434First, we categorise the game states as running games (where there are a

3535number of guesses available, and a number of letters still to guess), or

@@ -53,7 +53,7 @@ this data:

5353 data Mystery : GState -> Type

5454

5555Step 2: Game Rules

56−------------------

56+==================

5757

5858We describe the game rules as a dependent effect, where each action has

5959a *precondition* (i.e. what the game state must be before carrying out

@@ -131,7 +131,7 @@ then allow us to play the game.

131131 MYSTERY h = MkEff (Mystery h) MysteryRules

132132

133133Step 3: Implement Rules

134−-----------------------

134+=======================

135135

136136To *implement* the rules, we begin by giving a concrete definition of

137137game state:

@@ -211,7 +211,7 @@ such a way that the number of missing letters or number of guesses does

211211not follow the rules.

212212

213213Step 4: Implement Interface

214−---------------------------

214+===========================

215215

216216Having described the rules, and implemented state transitions which

217217follow those rules as an effect handler, we can now write an interface

@@ -225,7 +225,7 @@ for the game which uses the ``MYSTERY`` effect:

225225The type indicates that the game must start in a running state, with

226226some guesses available, and eventually reach a not-running state (i.e.

227227won or lost). The only way to achieve this is by correctly following the

228−stated rules.

228+stated rules.

229229

230230Note that the type of ``game`` makes no assumption that there are

231231letters to be guessed in the given word (i.e. it is ``w`` rather than

@@ -267,7 +267,7 @@ generator, then pick a random ``Fin`` to index into a list of

267267 limited form of type inference, but very useful in practice.

268268

269269A possible complete implementation of ``game`` is

270−presented below:

270+presented below:

271271

272272.. code-block:: idris

273273

@@ -298,7 +298,7 @@ presented below:

298298 (S k) => game

299299

300300Discussion

301−----------

301+==========

302302

303303Writing the rules separately as an effect, then an implementation

304304which uses that effect, ensures that the implementation must follow

@@ -330,4 +330,4 @@ These are, of course, simple errors, but were caught by the type

330330checker before any testing of the game.

331331

332332.. [1]

333− Readers may recognise this game by the name “Hangman.”

333+ Readers may recognise this game by the name “Hangman”.

docs/effects/impleff.rst+9−10

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

11.. _sect-impleff:

3−====================

3+********************

44Creating New Effects

5−====================

5+********************

77We have now seen several side-effecting operations provided by the

88``Effects`` library, and examples of their use in Section

@@ -14,7 +14,7 @@ selection of the available effects are implemented, and show how new

1414effectful operations may be provided.

1515

1616State

17−-----

17+=====

1818

1919Effects are described by *algebraic data types*, where the

2020constructors describe the operations provided when the effect is

@@ -154,7 +154,7 @@ Such details are not important for using the library, or even writing

154154new effects, however.

155155

156156Summary

157−~~~~~~~

157+-------

158158

159159The following listing summarises what is required to define the

160160``STATE`` effect:

@@ -183,7 +183,7 @@ The following listing summarises what is required to define the

183183

184184

185185Console I/O

186−-----------

186+===========

187187

188188Then listing below gives the definition of the ``STDIO``

189189effect, including handlers for ``IO`` and ``IOExcept``. We omit the

@@ -219,7 +219,7 @@ directly.

219219 STDIO = MkEff () StdIO

220220

221221Exceptions

222−----------

222+==========

223223

224224The listing below gives the definition of the ``Exception``

225225effect, including two of its handlers for ``Maybe`` and ``List``. The

@@ -244,7 +244,7 @@ error.

244244

245245

246246Non-determinism

247−---------------

247+===============

248248

249249The following listing gives the definition of the ``Select``

250250effect for writing non-deterministic programs, including a handler for

@@ -277,10 +277,10 @@ accumulate all successful results, and in the ``Maybe`` handler we try

277277the first value in the last, and try later values only if that fails.

278278

279279File Management

280−---------------

280+===============

281281

282282Result-dependent effects are no different from non-dependent effects

283−in the way they are implemented. The listing below

283+in the way they are implemented. The listing below

284284illustrates this for the ``FILE_IO`` effect. The syntax for state

285285transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is

286286computed from the result of the operation ``res``, follows that for

@@ -320,4 +320,3 @@ continuation ``k`` are different depending on whether the result is

320320``True`` (opening succeeded) or ``False`` (opening failed). This uses

321321``validFile``, defined in the ``Prelude``, to test whether a file

322322handler refers to an open file or not.

323−

docs/effects/introduction.rst+2−2

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

1−============

1+************

22Introduction

3−============

3+************

55Pure functional languages with dependent types such as `Idris

66<http://idris-lang.org/>`_ support reasoning about programs directly

docs/effects/simpleeff.rst+13−13

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

11.. _sect-simpleff:

3−==============

3+**************

44Simple Effects

5−==============

5+**************

77So far we have seen how to write programs with locally mutable state

88using the ``STATE`` effect. To recap, we have the definitions below

@@ -41,7 +41,7 @@ All of the effects in the library, including those described in this

4141section, are summarised in Appendix :ref:`sect-appendix`.

4242

4343Console I/O

44−-----------

44+===========

4545

4646Console I/O is supported with the ``STDIO``

4747effect, which allows reading and writing characters and strings to and

@@ -67,7 +67,7 @@ can perform (or at the very least simulate) console I/O:

6767 instance Handler StdIO (IOExcept a)

6868

6969Examples

70−~~~~~~~~

70+--------

7171

7272A program which reads the user’s name, then says hello, can be written

7373as follows:

@@ -117,7 +117,7 @@ read and write from the console. To run this, ``main`` does not need

117117to be changed.

118118

119119Aside: Resource Types

120−~~~~~~~~~~~~~~~~~~~~~

120+---------------------

121121

122122To find out the resource type of an effect, if necessary (for example

123123if we want to initialise a resource explicitiy with ``runInit`` rather

@@ -132,7 +132,7 @@ than using a default value with ``run``) we can run the

132132 Int : Type

133133

134134Exceptions

135−----------

135+==========

136136

137137The ``EXCEPTION``

138138effect is declared in module ``Effect.Exception``. This allows programs

@@ -155,7 +155,7 @@ generally:

155155 instance Show a => Handler (Exception a) IO

156156

157157Example

158−~~~~~~~

158+-------

159159

160160Suppose we have a ``String`` which is expected to represent an integer

161161in the range ``0`` to ``n``. We can write a function ``parseNumber``

@@ -232,7 +232,7 @@ the boundedness proof:

232232 else raise NotANumber

233233

234234Random Numbers

235−--------------

235+==============

236236

237237Random number generation is also implemented by the library, in module

238238``Effect.Random``:

@@ -263,7 +263,7 @@ produce a random number:

263263 (essentially a number with an upper bound given in its type).

264264

265265Example

266−~~~~~~~

266+-------

267267

268268We can use the ``RND`` effect to implement a simple guessing game. The

269269``guess`` function, given a target number, will repeatedly ask the

@@ -317,7 +317,7 @@ do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.

317317

318318

319319Non-determinism

320−---------------

320+===============

321321

322322The listing below gives the definition of the non-determinism

323323effect, which allows a program to choose a value non-deterministically

@@ -337,7 +337,7 @@ succeeds:

337337 instance Handler Selection List

338338

339339Example

340−~~~~~~~

340+-------

341341

342342The ``SELECT`` effect can be used to solve constraint problems, such

343343as finding Pythagorean triples. The idea is to use ``select`` to give

@@ -373,7 +373,7 @@ context). We can try this as follows:

373373 print $ the (List _) $ run (triple 100)

374374

375375``vadd`` revisited

376−------------------

376+==================

377377

378378We now return to the ``vadd`` program from the introduction. Recall the

379379definition:

@@ -453,7 +453,7 @@ with gracefully.

453453 else raise "Not a number"

454454

455455Example: An Expression Calculator

456−---------------------------------

456+=================================

457457

458458To show how these effects can fit together, let us consider an

459459evaluator for a simple expression language, with addition and integer

docs/effects/state.rst+8−8

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

11.. _sect-state:

3−=====

3+*****

44State

5−=====

5+*****

77Many programs, even pure programs, can benefit from locally mutable

88state. For example, consider a program which tags binary tree nodes

@@ -34,7 +34,7 @@ specific value ``i``, has the following type:

3434 treeTag : (i : Int) -> BTree a -> BTree (Int, a)

3535

3636First attempt

37−-------------

37+=============

3838

3939Naïvely, we can implement ``treeTag`` by implementing a helper

4040function which propagates a counter, returning the result of the count

@@ -75,7 +75,7 @@ is local mutable state (the counter) which we have had to make

7575explicit.

7676

7777Introducing ``Effects``

78−-----------------------

78+=======================

7979

8080Idris provides a library, ``Effects`` [3]_, which captures this

8181pattern and many others involving effectful computation [1]_. An

@@ -217,7 +217,7 @@ shown in Listing [introprog].

217217 main = print (treeTag 1 testTree)

218218

219219Effects and Resources

220−---------------------

220+=====================

221221

222222Each effect is associated with a *resource*, which is initialised

223223before an effectful program can be run. For example, in the case of

@@ -261,7 +261,7 @@ implemented ``treeTag`` by initialising the state as follows:

261261 treeTag i x = runPureInit [i] (treeTagAux x)

262262

263263Labelled Effects

264−----------------

264+================

265265

266266What if we have more than one state, especially more than one state of

267267the same type? How would ``get`` and ``put`` know which state they

@@ -358,7 +358,7 @@ effect. Note that labels are polymorphic in the label type ``lbl``.

358358Hence, a label can be anything—a string, an integer, a type, etc.

359359

360360``!``-notation

361−--------------

361+==============

362362

363363In many cases, using ``do``-notation can make programs unnecessarily

364364verbose, particularly in cases where the value bound is used once,

@@ -412,7 +412,7 @@ is lifted to:

412412 f g'

413413

414414Syntactic Sugar and ``Eff``

415−---------------------------

415+===========================

416416

417417By now, you may be wondering about the syntax we are using for

418418``Eff``, because it doesn’t look like a normal type! (If not, you may

docs/effects/summary.rst+9−9

@@ -1,14 +1,14 @@

11.. _sect-appendix:

3−===============

3+***************

44Effects Summary

5−===============

5+***************

77This appendix gives interfaces for the core effects provided by the

88library.

1010EXCEPTION

11−---------

11+=========

1212

1313.. code-block:: idris

1414

@@ -29,7 +29,7 @@ EXCEPTION

2929 instance Show a => Handler (Exception a) IO

3030

3131FILE\_IO

32−--------

32+========

3333

3434.. code-block:: idris

3535

@@ -58,7 +58,7 @@ FILE\_IO

5858 instance Handler FileIO IO

5959

6060RND

61−---

61+===

6262

6363.. code-block:: idris

6464

@@ -77,7 +77,7 @@ RND

7777 instance Handler Random m

7878

7979SELECT

80−------

80+======

8181

8282.. code-block:: idris

8383

@@ -93,7 +93,7 @@ SELECT

9393 instance Handler Selection List

9494

9595STATE

96−-----

96+=====

9797

9898.. code-block:: idris

9999

@@ -111,7 +111,7 @@ STATE

111111 instance Handler State m

112112

113113STDIO

114−-----

114+=====

115115

116116.. code-block:: idris

117117

@@ -133,7 +133,7 @@ STDIO

133133 instance Handler StdIO (IOExcept a)

134134

135135SYSTEM

136−------

136+======

137137

138138.. code-block:: idris

139139

docs/faq/faq.rst+12−12

@@ -1,9 +1,9 @@

1−==========================

1+**************************

22Frequently Asked Questions

3−==========================

3+**************************

55What are the differences between Agda and Idris?

6−------------------------------------------------

6+================================================

88The main difference is that Idris has been designed from the start to support

99verified systems programming through easy interoperability with C and high

@@ -14,7 +14,7 @@ do notation. Idris also supports tactic based theorem proving, and has a

1414lightweight Hugs/GHCI style interface.

1515

1616Is Idris production ready?

17−--------------------------

17+==========================

1818

1919Idris is primarily a research tool for exploring the possibilities of software

2020development with dependent types, meaning that the primary goal is not (yet) to

@@ -29,7 +29,7 @@ limited to) extra library support, polishing the run-time system (and ensuring

2929it is robust), providing and maintaining a JVM back end, etc.

3030

3131Why does Idris use eager evaluation rather than lazy?

32−-----------------------------------------------------

32+=====================================================

3333

3434Idris uses eager evaluation for more predictable performance, in particular

3535because one of the longer term goals is to be able to write efficient and

@@ -57,7 +57,7 @@ concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an

5757``Int``.

5858

5959How can I make lazy control structures?

60−---------------------------------------

60+=======================================

6161

6262You can make control structures using the special Lazy type. For example,

6363``if...then...else`` is defined as follows in the library:

@@ -74,7 +74,7 @@ The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will

7474only be evaluated if they are used, that is, they are evaluated lazily.

7575

7676Evaluation at the REPL doesn't behave as I expect. What's going on?

77−-------------------------------------------------------------------

77+===================================================================

7878

7979Being a fully dependently typed language, Idris has two phases where it

8080evaluates things, compile-time and run-time. At compile-time it will only

@@ -100,14 +100,14 @@ the difference between:

100100 \n => \m => plus n (S m) : Nat -> Nat -> Nat

101101

102102When will Idris be self-hosting?

103−--------------------------------

103+================================

104104

105105It’s not a priority, though not a bad idea in the long run. It would be a

106106worthwhile effort in the short term to implement libraries to support

107107self-hosting, such as a good parsing library.

108108

109109Does Idris have Universe Polymorphism? What is the type of ``Type``?

110−--------------------------------------------------------------------

110+====================================================================

111111

112112Rather than Universe polymorphism, Idris has a cumulative hierarchy of

113113universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.

@@ -115,7 +115,7 @@ Cumulativity means that if ``x : Type n`` then also ``x : Type m``,

115115provided that ``n <= m``.

116116

117117Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?

118−------------------------------------------------------------------------------------

118+===================================================================================

119119

120120Historically the C language and many other languages have used the

121121names ``Float`` and ``Double`` to represent floating point numbers of

@@ -132,14 +132,14 @@ That is, the names ``Float`` and ``Double`` are used to describe

132132single and double precision numbers.

133133

134134What does the name ‘Idris’ mean?

135−--------------------------------

135+================================

136136

137137British people of a certain age may be familiar with this

138138`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If

139139that doesn’t help, maybe you can invent a suitable acronym :-) .

140140

141141Where can I find more answers?

142−------------------------------

142+==============================

143143

144144There is an `Unofficial FAQ

145145<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on

docs/guides/type-providers-ffi.rst+12−11

@@ -1,5 +1,6 @@

1+***********************

12Type Providers in Idris

2−=======================

3+***********************

45`Type providers in Idris

56<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

@@ -9,7 +10,7 @@ foreign functions, because these will often be used with type

910providers.

1011

1112The use case

12−------------

13+============

1314

1415First, let's talk about *why* we might want type providers. There are

1516a number of reasons to use them and there are other examples available

@@ -23,7 +24,7 @@ relied upon. We don't just want to hard-code these types into our

2324program... so we'll use a type provider to find them at compile time!

2425

2526A simple example

26−----------------

27+================

2728

2829First, let's go over a basic usage of type providers, because foreign

2930functions can be confusing but it's important to remember that

@@ -94,7 +95,7 @@ themselves!

9495Don't worry, there's a better way.

9596

9697Foreign Functions

97−-----------------

98+=================

9899

99100It's actually pretty easy to write a C function that figures out the

100101size of ``size_t``:

@@ -114,8 +115,8 @@ So now we can get the size of ``size_t`` as long as we're in C code.

114115We'd like to be able to use this from Idris. Can we do this? It turns

115116out we can.

116117

117−mkForeign

118−~~~~~~~~~

118+``mkForeign``

119+-------------

119120

120121With mkForeign, we can turn a C function into an IO action. It works

121122like this:

@@ -138,7 +139,7 @@ compiler "Treat the return value of this C function like it's a C int,

138139and when you pass it back into Idris, convert it to an Idris int."

139140

140141Caveats of mkForeign

141−^^^^^^^^^^^^^^^^^^^^

142+--------------------

142143

143144First and foremost: ``mkForeign`` is not actually a function. It is

144145treated specially by the compiler, and there are certain rules you

@@ -185,7 +186,7 @@ applied. This is okay:

185186 lengths = mapM strlen listOfStrings

186187

187188Running foreign functions

188−~~~~~~~~~~~~~~~~~~~~~~~~~

189+-------------------------

189190

190191This is all well and good for writing code that will typecheck. To

191192actually run the code, we'll need to do just a bit more work. Exactly

@@ -193,7 +194,7 @@ what we need to do depends on whether we want to interpret or compile

193194our code.

194195

195196In the interpreter

196−^^^^^^^^^^^^^^^^^^

197+------------------

197198

198199If we want to call our foreign functions from interpreted code (such

199200as the REPL or a type provider), we need to dynamically link a library

@@ -213,7 +214,7 @@ functions from an installed library rather than something you wrote

213214yourself, the "./" is not necessary.

214215

215216In an executable

216−^^^^^^^^^^^^^^^^

217+----------------

217218

218219If we want to run our code from an executable, we can statically link

219220instead. We'll use the ``%include`` and ``%link`` directives:

@@ -229,7 +230,7 @@ directives search in the current directory by default. (That is, the

229230directory from which we run idris.)

230231

231232Putting it all together

232−-----------------------

233+=======================

233234

234235So, at the beginning of this article I said we'd use type providers to

235236port ``struct stat`` to Idris. The relevant part is just translating

docs/index.rst+2−1

@@ -15,6 +15,7 @@ Documentation for the Idris Language

1515

1616 More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

1717

18+

1819* :ref:`tutorial-index`

1920* :ref:`eff-tutorial-index`

2021* :ref:`faq-index`

@@ -47,7 +48,7 @@ The Idris Tutorial

4748 tutorial/miscellany

4849 tutorial/conclusions

4950

50−.. _effects:

51+.. _faq:

5152

5253##########################

5354Frequently Asked Questions

docs/proofs/inductive.rst+6−5

@@ -1,5 +1,6 @@

1+****************

12Inductive Proofs

2−================

3+****************

45Before embarking on proving ``plus_commutes`` in Idris itself, let us

56consider the overall structure of a proof of some property of natural

@@ -25,7 +26,7 @@ case). Recalling ``plus``:

2526

2627This is total because it covers all possible inputs (the first argument

2728can only be ``Z`` or ``S k`` for some ``k``, and the second argument

28−``m`` covers all possible ``Nat``\ s) and in the recursive call, ``k``

29+``m`` covers all possible ``Nat``) and in the recursive call, ``k``

2930is structurally smaller than ``S k`` so the first argument will always

3031reach the base case ``Z`` in any sequence of recursive calls.

3132

@@ -50,7 +51,7 @@ function capturing all such inductive definitions:

5051.. code-block:: idris

5152

5253 nat_induction : (P : Nat -> Type) -> -- Property to show

53− (P Z) -> -- Base case

54+ (P Z) -> -- Base case

5455 ((k : Nat) -> P k -> P (S k)) -> -- Inductive step

5556 (x : Nat) -> -- Show for all x

5657 P x

@@ -63,12 +64,12 @@ version of ``plus``:

6364.. code-block:: idris

6465

6566 plus_ind : Nat -> Nat -> Nat

66− plus_ind n m

67+ plus_ind n m

6768 = nat_induction (\x => Nat)

6869 m -- Base case, plus_ind Z m

6970 (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m

7071 -- where k_rec = plus_ind k m

71− n

72+ n

7273

7374To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and

7475``m``, we can also use induction. Either we can fix ``m`` and perform

docs/proofs/interactive.rst+4−5

@@ -1,13 +1,14 @@

1+***************************

12Interactive Theorem Proving

2−===========================

3+***************************

45Idris also supports interactive theorem proving via tactics. This

5−is generally not recommended to be used directly, but rather used as a

6+is generally not recommended to be used directly, but rather used as a

67mechanism for building proof automation which is beyond the scope of this

78tutorial. In this section, we briefly discus tactics.

910One way to write proofs interactively is to write the general *structure* of

10−the proof, and use the interactive mode to complete the details.

11+the proof, and use the interactive mode to complete the details.

1112Consider the following definition, proved in :ref:`sect-theorems`:

1213

1314.. code-block:: idris

@@ -162,5 +163,3 @@ which is trivially provable:

162163

163164Again, we can add this proof to the end of our source file using the

164165``:addproof`` command at the interactive prompt.

165−

166−

docs/proofs/patterns.rst+7−6

@@ -1,5 +1,6 @@

1+***********************

12Pattern Matching Proofs

2−=======================

3+***********************

45In this section, we will provide a proof of ``plus_commutes`` directly,

56by writing a pattern matching definition. We will use interactive

@@ -26,7 +27,7 @@ mapping to Emacs commands.

2627

2728

2829Creating a Definition

29−---------------------

30+=====================

3031

3132To begin, create a file ``pluscomm.idr`` containing the following type

3233declaration:

@@ -87,7 +88,7 @@ It is a good idea to give these slightly more meaningful names:

8788 plus_commutes (S k) m = ?plus_commutes_S

8889

8990Base Case

90−---------

91+=========

9192

9293We can create a separate lemma for the base case interactively, by

9394pressing ``\l`` with the cursor over ``plus_commutes_Z``. This

@@ -263,7 +264,7 @@ proof, giving:

263264The base case is now complete.

264265

265266Inductive Step

266−--------------

267+==============

267268

268269Our main theorem, ``plus_commutes`` should currently be in the following

269270state:

@@ -333,9 +334,9 @@ defined by matching on its first argument. The complete definition is:

333334 plus_commutes_S k Z = Refl

334335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

335336

336−All metavariables have now been solved,

337+All metavariables have now been solved,

337338

338−The ``total`` annotation means that we require the final function to

339+The ``total`` annotation means that we require the final function to

339340pass the totality checker; i.e. it will terminate on all possible

340341well-typed inputs. This is important for proofs, since it provides a

341342guarantee that the proof is valid in *all* cases, not just those for

docs/proofs/pluscomm.rst+7−6

@@ -1,5 +1,6 @@

1+********************************************

12Running example: Addition of Natural Numbers

2−============================================

3+********************************************

45Throughout this tutorial, we will be working with the following

56function, defined in the Idris prelude, which defines addition on

@@ -44,7 +45,7 @@ We can use these properties in an Idris program, but in order to do so

4445we must *prove* them.

4546

4647Equality Proofs

47−---------------

48+===============

4849

4950Idris has a built-in propositional equality type, conceptually defined

5051as follows:

@@ -93,7 +94,7 @@ error:

9394 4 = 5 (Expected type)

9495

9596Type checking equality proofs

96−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

97+-----------------------------

9798

9899An important step in type checking Idris programs is *unification*,

99100which attempts to resolve implicit arguments such as the implicit

@@ -123,7 +124,7 @@ following equalities directly:

123124 plus_reduces_Sk k m = Refl

124125

125126Heterogeneous Equality

126−----------------------

127+======================

127128

128129Equality in Idris is *heterogeneous*, meaning that we can even propose

129130equalities between values in different types:

@@ -164,7 +165,7 @@ there is only one value which will type check:

164165 vect_eq_length xs _ Refl = Refl

165166

166167Properties of ``plus``

167−----------------------

168+======================

168169

169170Using the ``(=)`` type, we can now state the properties of ``plus``

170171given above as Idris type declarations:

@@ -185,4 +186,4 @@ the function.) We will also discuss how to use such equality proofs, and

185186see where the need for them arises in practice.

186187

187188.. [1]

188− This is known as the Curry-Howard correspondence

189+ This is known as the Curry-Howard correspondence.

docs/reference/documenting.rst+4−4

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

11.. _sect-documenting:

3−======================

3+**********************

44Documenting Idris Code

5−======================

5+**********************

77Idris documentation comes in two major forms: comments, which exist

88for a reader’s edification and are ignored by the compiler, and inline

@@ -12,7 +12,7 @@ reference. To consult the documentation for a declaration ``f``, write

1212(``C-c C-d`` in Emacs, in Vim).

1313

1414Comments

15−--------

15+========

1616

1717Use comments to explain why code is written the way that it

1818is. Idris’s comment syntax is the same as that of Haskell: lines

@@ -22,7 +22,7 @@ lines. These can be used to comment out lines of code or provide

2222simple documentation for the readers of Idris code.

2323

2424Inline Documentation

25−--------------------

25+====================

2626

2727Idris also supports a comprehensive and rich inline syntax for Idris

2828code to be generated. This syntax also allows for named parameters and

docs/reference/erasure.rst+21−20

@@ -1,5 +1,6 @@

1+*************************

12Erasure By Usage Analysis

2−=========================

3+*************************

45This work stems from this `feature proposal

56<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__

@@ -8,7 +9,7 @@ is out of date — and sometimes even in direct contradiction with the

89eventual implementation.

910

1011Motivation

11−----------

12+==========

1213

1314Traditional dependently typed languages (Agda, Coq) are good at

1415erasing *proofs* (either via irrelevance or an extra universe).

@@ -52,7 +53,7 @@ The following two sections describe two cases where doing so improves

5253the runtime performance asymptotically.

5354

5455Binary numbers

55−~~~~~~~~~~~~~~

56+--------------

5657

5758- O(n) instead of O(log n)

5859

@@ -106,7 +107,7 @@ should get rid of them and get runtime code similar to what a idris

106107programmer would write.

107108

108109U-views of lists

109−~~~~~~~~~~~~~~~~

110+----------------

110111

111112- O(n^2) instead of O(n)

112113

@@ -141,7 +142,7 @@ linear time — so we need to erase the index ``xs`` if we want to

141142achieve this goal.

142143

143144Changes to Idris

144−----------------

145+================

145146

146147Usage analysis is run at every compilation and its outputs are used

147148for various purposes. This is actually invisible to the user but it's

@@ -185,7 +186,7 @@ Postulates are no longer required to be collapsible. They are now

185186required to be *unused* instead.

186187

187188Changes to the language

188−-----------------------

189+=======================

189190

190191You can use dots to mark fields that are not intended to be used at

191192runtime.

@@ -221,7 +222,7 @@ You can also put dots in types of functions to get more guarantees.

221222and free implicits are automatically dotted here, too.

222223

223224What it means

224−-------------

225+=============

225226

226227Dot annotations serve two purposes:

227228

@@ -235,7 +236,7 @@ are there mainly to help the programmer (and the compiler) refrain

235236from using the values they want to erase.

236237

237238How to use it

238−-------------

239+=============

239240

240241Ideally, few or no extra annotations are needed -- in practice, it

241242turns out that having free implicits automatically dotted is enough to

@@ -250,7 +251,7 @@ compiles to a reasonable binary. Generally, it's sufficient to follow

250251erasure warnings (which may be sometimes unhelpful at the moment).

251252

252253Benchmarks

253−----------

254+==========

254255

255256- source: https://github.com/ziman/idris-benchmarks

256257- results: http://ziman.functor.sk/erasure-bm/

@@ -258,7 +259,7 @@ Benchmarks

258259It can be clearly seen that asymptotics are improved by erasure.

259260

260261Shortcomings

261−------------

262+============

262263

263264You can't get warnings in libraries because usage analysis starts from

264265``Main.main``. This will be solved by the planned ``%default_usage``

@@ -300,7 +301,7 @@ only if it is unused in every implementation of the method that occurs

300301in the program.

301302

302303Planned features

303−----------------

304+================

304305

305306- Fixes to the above shortcomings in general.

306307

@@ -316,10 +317,10 @@ Planned features

316317 in compiled programs.

317318

318319Troubleshooting

319−---------------

320+===============

320321

321322My program is slower

322−~~~~~~~~~~~~~~~~~~~~

323+--------------------

323324

324325The patch introducing erasure by usage analysis also disabled some

325326optimisations that were in place before; these are subsumed by the new

@@ -336,14 +337,14 @@ getting compiled into the binary.

336337The solution is to change the code so that there are no warnings.

337338

338339Usage warnings are unhelpful

339−~~~~~~~~~~~~~~~~~~~~~~~~~~~~

340+----------------------------

340341

341342This is a known issue and we are working on it. For now, see the section

342343`How to read and resolve erasure

343344warnings <#how-to-read-and-resolve-erasure-warnings>`__.

344345

345346There should be no warnings in this function

346−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

347+--------------------------------------------

347348

348349A possible cause is non-totality of the function (more precisely,

349350non-coverage). If a function is non-covering, the program needs to

@@ -361,7 +362,7 @@ https://gist.github.com/ziman/10458331). You can either rephrase the

361362function or wait until this is fixed, hopefully soon. Fixed.

362363

363364The compiler refuses to recognise this thing as erased

364−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

365+------------------------------------------------------

365366

366367You can force anything to be erased by wrapping it in the ``Erased``

367368monad. While this program triggers usage warnings,

@@ -379,10 +380,10 @@ the following program does not:

379380 f g x = g (Erase x) -- OK

380381

381382How to read and resolve erasure warnings

382−----------------------------------------

383+========================================

383384

384385Example 1

385−~~~~~~~~~

386+---------

386387

387388Consider the following program:

388389

@@ -439,7 +440,7 @@ or fixing ``vlen`` to not use the index:

439440Which solution is appropriate depends on the usecase.

440441

441442Example 2

442−~~~~~~~~~

443+---------

443444

444445Consider the following program manipulating value-indexed binary

445446numbers.

@@ -494,7 +495,7 @@ with every constructor of ``Bin`` and make it a bound implicit:

494495 I : {n : Nat} -> bin n -> Bin (1 + n + n)

495496

496497References

497−----------

498+==========

498499

499500.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

500501 families need not store their indices

docs/reference/ffi.rst+8−7

@@ -1,5 +1,6 @@

1+******************************

12New Foreign Function Interface

2−==============================

3+******************************

45.. sectionauthor:: Edwin Brady

@@ -19,7 +20,7 @@ are some things you will need to be aware of, which this page

1920describes.

2021

2122The ``IO'`` monad, and ``main``

22−-------------------------------

23+===============================

2324

2425The ``IO`` monad exists as before, but is now specific to the C

2526backend (or, more precisely, any backend whose foreign function calls

@@ -61,7 +62,7 @@ function's name, but potentially something more complicated such as an

6162external library file or even a URL).

6263

6364FFI descriptors

64−---------------

65+===============

6566

6667An FFI descriptor is a record containing a predicate which holds when

6768a type can be marshalled, and the type of the target of a foreign

@@ -98,7 +99,7 @@ For C, this is:

9899 String -- the name of the C function

99100

100101Foreign calls

101−-------------

102+=============

102103

103104To call a foreign function, the ``foreign`` function is used. For

104105example:

@@ -134,7 +135,7 @@ example a shorthand for calling external JavaScript functions:

134135 jscall fname ty = foreign FFI_JS fname ty

135136

136137FFI implementation

137−~~~~~~~~~~~~~~~~~~

138+------------------

138139

139140In order to write bindings to external libraries, the details of how

140141``foreign`` works are unnecessary --- you simply need to know that

@@ -172,7 +173,7 @@ builds the following implicit proof as the ``fty`` argument to

172173 FFun C_Str (FFun C_Str (FRet C_Ptr))

173174

174175Compiling foreign calls

175−-----------------------

176+=======================

176177

177178(This section assumes some knowledge of the Idris internals.)

178179

@@ -232,7 +233,7 @@ to marshal the arguments and return value appropriately.

232233 the function ``toFType``, to see how this works in practice.

233234

234235JavaScript FFI descriptor

235−~~~~~~~~~~~~~~~~~~~~~~~~~

236+=========================

236237

237238The JavaScript FFI descriptor is a little more complex, because the

238239JavaScript FFI supports marshalling functions. It is defined as

docs/reference/uniqueness-types.rst+5−4

@@ -1,5 +1,6 @@

1+****************

12Uniqueness Types

2−================

3+****************

45Uniqueness Types are an experimental feature available from Idris

560.9.15. A value with a unique type is guaranteed to have *at most one*

@@ -25,7 +26,7 @@ include:

2526 allocate

2627

2728Using Uniqueness

28−~~~~~~~~~~~~~~~~

29+================

2930

3031If ``x : T`` and ``T : UniqueType``, then there is at most one reference

3132to ``x`` at any time during run-time execution. For example, we can

@@ -129,7 +130,7 @@ such a function may be passed a ``UniqueType``, any value of type

129130once on the right hand side.

130131

131132Borrowed Types

132−~~~~~~~~~~~~~~

133+--------------

133134

134135It quickly becomes obvious when working with uniqueness types that

135136having only one reference at a time can be painful. For example, what

@@ -227,7 +228,7 @@ therefore write ``showU`` as follows:

227228 showU' (x :: xs) = show x ++ ", " ++ showU' xs

228229

229230Problems/Disadvantages/Still to do...

230−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

231+-------------------------------------

231232

232233This is a work in progress, there is lots to do. The most obvious

233234problem is the loss of abstraction. On the one hand, we have more

docs/tutorial/classes.rst+12−12

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

11.. _sect-classes:

3−============

3+************

44Type Classes

5−============

5+************

77We often want to define functions which work across several different

88data types. For example, we would like arithmetic operators to work on

@@ -65,7 +65,7 @@ going to use it to convert each element to a ``String``:

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

6666

6767Default Definitions

68−-------------------

68+===================

6969

7070The library defines an ``Eq`` class which provides an interface for

7171comparing values for equality or inequality, with instances for all of

@@ -110,7 +110,7 @@ definition is missing, and there is a default definition for it, then

110110the default is used instead.

111111

112112Extending Classes

113−-----------------

113+=================

114114

115115Classes can also be extended. A logical next step from an equality

116116relation ``Eq`` is to define an ordering relation ``Ord``. We can

@@ -155,7 +155,7 @@ separated list, for example:

155155 sortAndShow xs = show (sort xs)

156156

157157Functors and Applicatives

158−-------------------------

158+=========================

159159

160160So far, we have seen single parameter type classes, where the parameter

161161is of type ``Type``. In general, there can be any number (greater than

@@ -195,7 +195,7 @@ abstracts the notion of function application:

195195 (<*>) : f (a -> b) -> f a -> f b

196196

197197Monads and ``do``-notation

198−--------------------------

198+==========================

199199

200200The ``Monad`` class allows us to encapsulate binding and computation,

201201and is the basis of ``do``-notation introduced in Section

@@ -248,7 +248,7 @@ are available, or return ``Nothing`` if they are not. Managing the

248248 Nothing : Maybe Int

249249

250250``!``-notation

251−~~~~~~~~~~~~~~

251+--------------

252252

253253In many cases, using ``do``-notation can make programs unnecessarily

254254verbose, particularly in cases such as ``m_add`` above where the value

@@ -292,7 +292,7 @@ is lifted to:

292292 f g'

293293

294294Monad comprehensions

295−~~~~~~~~~~~~~~~~~~~~

295+--------------------

296296

297297The list comprehension notation we saw in Section

298298:ref:`sect-more-expr` is more general, and applies to anything which

@@ -336,7 +336,7 @@ would be:

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

337337

338338Idiom brackets

339−--------------

339+==============

340340

341341While ``do`` notation gives an alternative meaning to sequencing,

342342idioms give an alternative meaning to *application*. The notation and

@@ -386,7 +386,7 @@ application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>

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

387387

388388An error-handling interpreter

389−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

389+-----------------------------

390390

391391Idiom notation is commonly useful when defining evaluators. McBride

392392and Paterson describe such an evaluator [1]_, for a language similar

@@ -455,7 +455,7 @@ to handle errors:

455455 MkEval envFn => envFn env

456456

457457Named Instances

458−---------------

458+===============

459459

460460It can be desirable to have multiple instances of a type class, for

461461example to provide alternative methods for sorting or printing values.

@@ -492,7 +492,7 @@ instance ``myord`` as follows, at the Idris prompt:

492492

493493

494494Determining Parameters

495−----------------------

495+======================

496496

497497When a class has more than one parameter, it can help resolution if

498498the parameters used to resolve the type class are restricted. For

docs/tutorial/conclusions.rst+2−2

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

11.. _sect-concs:

3−===============

3+***************

44Further Reading

5−===============

5+***************

77Further information about Idris programming, and programming with

88dependent types in general, can be obtained from various sources:

docs/tutorial/index.rst+3−3

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

11.. _tutorial-index:

3−####################

4− The Idris Tutorial

5−####################

3+##################

4+The Idris Tutorial

5+##################

77The is the Idris Tutorial. It will teach you about programming in the Idris Language.

docs/tutorial/interactive.rst+10−10

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

11.. _sect-interactive:

3−===================

3+*******************

44Interactive Editing

5−===================

5+*******************

77By now, we have seen several examples of how Idris’ dependent type

88system can give extra confidence in a function’s correctness by giving

@@ -25,7 +25,7 @@ available.

2525

2626

2727Editing at the REPL

28−-------------------

28+===================

2929

3030The REPL provides a number of commands, which we will describe

3131shortly, which generate new program fragments based on the currently

@@ -59,10 +59,10 @@ A text editor can take advantage of this, along with the editing

5959commands, in order to provide interactive editing support.

6060

6161Editing Commands

62−----------------

62+================

6363

6464:addclause

65−~~~~~~~~~~

65+----------

6666

6767The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a

6868template definition for the function named ``f`` declared on line

@@ -91,7 +91,7 @@ This declares that any names generated for types in the ``Vect`` family

9191should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.

9292

9393:casesplit

94−~~~~~~~~~~

94+----------

9595

9696The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the

9797pattern variable ``x`` on line ``n`` into the various pattern forms it

@@ -125,7 +125,7 @@ That is, the pattern variable ``ys`` has been split into one case

125125ys`` would lead to a unification error.

126126

127127:addmissing

128−~~~~~~~~~~~

128+-----------

129129

130130The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

131131clauses which are required to make the function ``f`` on line ``n``

@@ -148,7 +148,7 @@ generates the required clauses, and eliminates the clauses which would

148148lead to unification errors.

149149

150150:proofsearch

151−~~~~~~~~~~~~

151+------------

152152

153153The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to

154154find a value for the metavariable ``f`` on line ``n`` by proof search,

@@ -186,7 +186,7 @@ must have type ``c`` and the only way to get this is to apply ``f`` to

186186recursively.

187187

188188:makewith

189−~~~~~~~~~

189+---------

190190

191191The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a

192192``with`` to a pattern clause. For example, recall ``parity``. If line

@@ -219,7 +219,7 @@ dependent pattern matching by showing a programmer exactly what the

219219valid patterns are.

220220

221221Interactive Editing in Vim

222−--------------------------

222+==========================

223223

224224The editor mode for Vim provides syntax highlighting, indentation and

225225interactive editing support using the commands described above.

docs/tutorial/interp.rst+7−7

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

11.. _sect-interp:

3−===================================

3+***********************************

44Example: The Well-Typed Interpreter

5−===================================

5+***********************************

77In this section, we’ll use the features we’ve seen so far to write a

88larger example, an interpreter for a simple functional programming

@@ -12,7 +12,7 @@ system to ensure that any programs which can be represented are

1212well-typed.

1313

1414Representing Languages

15−----------------------

15+======================

1616

1717First, let us define the types in the language. We have integers,

1818booleans, and functions, represented by ``Ty``:

@@ -140,7 +140,7 @@ that only the branch which is taken need be evaluated:

140140 Expr G a

141141

142142Writing the Interpreter

143−-----------------------

143+=======================

144144

145145When we evaluate an ``Expr``, we’ll need to know the values in scope,

146146as well as their types. ``Env`` is an environment, indexed over the

@@ -225,7 +225,7 @@ its operands directly, and for ``If``, we apply the Idris

225225 else interp env e

226226

227227Testing

228−-------

228+=======

229229

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

231231``\x. \y. y + x`` is written as follows:

@@ -248,7 +248,7 @@ can be written as:

248248 (Var Stop)))

249249

250250Running

251−-------

251+=======

252252

253253To finish, we write a ``main`` program which interprets the factorial

254254function on user input:

@@ -271,7 +271,7 @@ program at the Idris interactive environment is:

271271

272272

273273Aside: ``cast``

274−~~~~~~~~~~~~~~~

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

275275

276276The prelude defines a type class ``Cast`` which allows conversion

277277between types:

docs/tutorial/introduction.rst+4−4

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

11.. _sect-intro:

3−============

3+************

44Introduction

5−============

5+************

77In conventional programming languages, there is a clear distinction

88between *types* and *values*. For example, in `Haskell

@@ -44,7 +44,7 @@ a lightweight foreign function interface which allows easy interaction

4444with external ``C`` libraries.

4545

4646Intended Audience

47−-----------------

47+=================

4848

4949This tutorial is intended as a brief introduction to the language, and

5050is aimed at readers already familiar with a functional language such

@@ -55,7 +55,7 @@ briefly. The reader is also assumed to have some interest in using

5555dependent types for writing and verifying systems software.

5656

5757Example Code

58−------------

58+============

5959

6060This tutorial includes some example code, which has been tested with

6161Idris version . The files are available in the Idris

docs/tutorial/miscellany.rst+17−17

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

11.. _sect-misc:

3−==========

3+**********

44Miscellany

5−==========

5+**********

77In this section we discuss a variety of additional features:

@@ -15,7 +15,7 @@ In this section we discuss a variety of additional features:

1515+ the universe hierarchy.

1616

1717Auto implicit arguments

18−-----------------------

18+=======================

1919

2020We have already seen implicit arguments, which allows arguments to be

2121omitted when they can be inferred by the type checker, e.g.

@@ -70,7 +70,7 @@ to:

7070 head (x :: xs) = x

7171

7272Implicit conversions

73−--------------------

73+====================

7474

7575Idris supports the creation of *implicit conversions*, which allow

7676automatic conversion of values from one type to another when required to

@@ -99,7 +99,7 @@ specific language, or to hide details of a proof. Such examples are

9999beyond the scope of this tutorial.

100100

101101Literate programming

102−--------------------

102+====================

103103

104104Like Haskell, Idris supports *literate* programming. If a file has

105105an extension of ``.lidr`` then it is assumed to be a literate file. In

@@ -120,7 +120,7 @@ program line (beginning with ``>``) and a comment line (beginning with

120120any other character).

121121

122122Foreign function calls

123−----------------------

123+======================

124124

125125For practical programming, it is often necessary to be able to use

126126external libraries, particularly for interfacing with the operating

@@ -191,7 +191,7 @@ function is implemented as follows, as a call to an external function

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

192192

193193Include and linker directives

194−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

194+-----------------------------

195195

196196Foreign function calls are translated directly to calls to C functions,

197197with appropriate conversion between the Idris representation of a

@@ -215,7 +215,7 @@ through the following directives:

215215 object ``x.so``.

216216

217217Testing foreign function calls

218−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

218+------------------------------

219219

220220Normally, the Idris interpreter (used for typechecking and at the REPL)

221221will not perform IO actions. Additionally, as it neither generates C

@@ -232,7 +232,7 @@ command or the ``%dynamic`` directive. For example:

232232 0.9995736030415051 : Float

233233

234234Type Providers

235−--------------

235+==============

236236

237237Idris type providers, inspired by F#’s type providers, are a means of

238238making our types be “about” something in the world outside of Idris. For

@@ -301,7 +301,7 @@ provider implementations, including a statically-checked SQLite binding,

301301are available in an external collection [1]_.

302302

303303C Target

304−--------

304+========

305305

306306The default target of Idris is C. Compiling via :

307307

@@ -341,14 +341,14 @@ is shown below :

341341 putStrLn $ show $ factorial 3

342342

343343JavaScript Target

344−-----------------

344+=================

345345

346346Idris is capable of producing *JavaScript* code that can be run in a

347347browser as well as in the *NodeJS* environment or alike. One can use the

348348FFI to communicate with the *JavaScript* ecosystem.

349349

350350Code Generation

351−~~~~~~~~~~~~~~~

351+---------------

352352

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

354354that is tailored for running in the browser issue the following command:

@@ -375,7 +375,7 @@ automatically add a newline to the end of each string. This behaviour

375375does not show up in the *NodeJS* code generator.

376376

377377Using the FFI

378−~~~~~~~~~~~~~

378+-------------

379379

380380To write a useful application we need to communicate with the outside

381381world. Maybe we want to manipulate the DOM or send an Ajax request. For

@@ -441,7 +441,7 @@ program:

441441The program outputs ``3``, just like we expected.

442442

443443Including external *JavaScript* files

444−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

444+-------------------------------------

445445

446446Whenever one is working with *JavaScript* one might want to include

447447external libraries or just some functions that she or he wants to call

@@ -470,7 +470,7 @@ And for use in the browser:

470470The given files will be added to the top of the generated code.

471471

472472Including *NodeJS* modules

473−~~~~~~~~~~~~~~~~~~~~~~~~~~

473+--------------------------

474474

475475The *NodeJS* code generator can also include modules with the ``%lib``

476476directive.

@@ -486,7 +486,7 @@ This directive compiles into the following *JavaScript*

486486 var fs = require("fs");

487487

488488Shrinking down generated *JavaScript*

489−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

489+-------------------------------------

490490

491491Idris can produce very big chunks of *JavaScript* code. However, the

492492generated code can be minified using the ``closure-compiler`` from

@@ -497,7 +497,7 @@ and it’s highly recommended to use it when shipping a *JavaScript*

497497application written in Idris.

498498

499499Cumulativity

500−------------

500+============

501501

502502Since values can appear in types and *vice versa*, it is natural that

503503types themselves have types. For example:

docs/tutorial/modules.rst+5−5

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

11.. _sect-namespaces:

3−=======================

3+**********************

44Modules and Namespaces

5−=======================

5+**********************

77An Idris program consists of a collection of modules. Each module

88includes an optional ``module`` declaration giving the name of the

@@ -72,7 +72,7 @@ main module, with the ``main`` function, must be called

7272``Main``—although its filename need not be ``Main.idr``.

7373

7474Export Modifiers

75−----------------

75+================

7676

7777By default, all names defined in a module are exported for use by other

7878modules. However, it is good practice only to export a minimal interface

@@ -146,7 +146,7 @@ abstract names in module ``C``, but will not re-export anything from

146146module ``B``.

147147

148148Explicit Namespaces

149−-------------------

149+===================

150150

151151Defining a module also defines a namespace implicitly. However,

152152namespaces can also be given *explicitly*. This is most useful if you

@@ -176,7 +176,7 @@ disambiguated by their types:

176176 "foofoo" : String

177177

178178Parameterised blocks

179−--------------------

179+====================

180180

181181Groups of functions can be parameterised over a number of arguments

182182using a ``parameters`` declaration, for example:

docs/tutorial/packages.rst+4−4

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

11.. _sect-packages:

3−========

3+********

44Packages

5−========

5+********

77Idris includes a simple system for building packages from a

88package description file. These files can be used with the Idris

@@ -10,7 +10,7 @@ compiler to manage the development process of your Idris

1010programmes and packages.

1111

1212Package Descriptions

13−--------------------

13+====================

1414

1515A package description includes the following:

1616

@@ -58,7 +58,7 @@ external ``C`` libraries, the following options are available:

5858 object files to be installed, perhaps generated by the ``Makefile``.

5959

6060Using Package files

61−-------------------

61+===================

6262

6363Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:

6464

docs/tutorial/provisional.rst+5−5

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

11.. _sect-provisional:

3−=======================

3+***********************

44Provisional Definitions

5−=======================

5+***********************

77Sometimes when programming with dependent types, the type required by

88the type checker and the type of the program we have written will be

@@ -54,7 +54,7 @@ reduction. These values are obviously equal — how can we rewrite the

5454program to fix this problem?

5555

5656Provisional definitions

57−-----------------------

57+=======================

5858

5959*Provisional definitions* help with this problem by allowing us to defer

6060the proof details until a later point. There are two main reasons why

@@ -159,7 +159,7 @@ reversed:

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

160160

161161Suspension of Disbelief

162−-----------------------

162+=======================

163163

164164Idris requires that proofs be complete before compiling programs

165165(although evaluation at the prompt is possible without proof details).

@@ -192,7 +192,7 @@ The ``exact`` tactic allows us to provide an exact value for the proof.

192192In this case, we assert that the value we gave was correct.

193193

194194Example: Binary numbers

195−-----------------------

195+=======================

196196

197197Previously, we implemented conversion to binary numbers using the

198198``Parity`` view. Here, we show how to use the same view to implement a

docs/tutorial/starting.rst+5−5

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

11.. _sect-starting:

3−===============

3+***************

44Getting Started

5−===============

5+***************

77Prerequisites

8−-------------

8+=============

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

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

@@ -18,7 +18,7 @@ of the necessary libraries and tools. You will need:

1818 from MacPorts/Homebrew and all major Linux distributions.

1919

2020Downloading and Installing

21−--------------------------

21+==========================

2222

2323The easiest way to install Idris, if you have all of the

2424prerequisites, is to type:

@@ -69,7 +69,7 @@ instead. Some useful options to the Idris command are:

6969- ``--help`` display usage summary and command line options

7070

7171The Interactive Environment

72−---------------------------

72+===========================

7373

7474Entering ``idris`` at the shell prompt starts up the interactive

7575environment. You should see something like the following:

docs/tutorial/syntax.rst+11−8

@@ -1,14 +1,17 @@

1+.. _sect-syntax:

3+*****************

14Syntax Extensions

2−=================

5+*****************

4−supports the implementation of *Embedded Domain Specific Languages*

5−(EDSLs) in several ways [1]_. One way, as we have already seen, is

6−through extending ``do`` notation. Another important way is to allow

7−extension of the core syntax. In this section we describe two ways of

8−extending the syntax: ``syntax`` rules and ``dsl`` notation.

7+Idris supports the implementation of *Embedded Domain Specific

8+Languages* (EDSLs) in several ways [1]_. One way, as we have already

9+seen, is through extending ``do`` notation. Another important way is

10+to allow extension of the core syntax. In this section we describe two

11+ways of extending the syntax: ``syntax`` rules and ``dsl`` notation.

912

1013``syntax`` rules

11−----------------

14+================

1215

1316We have seen ``if...then...else`` expressions, but these are not built

1417in. Instead, we can define a function in the prelude as follows (we

@@ -101,7 +104,7 @@ a bound variable, substituted on the right hand side. We have also put

101104``in`` in quotation marks since it is already a reserved word.

102105

103106``dsl`` notation

104−----------------

107+================

105108

106109The well-typed interpreter in Section :ref:`sect-interp` is a simple

107110example of a common programming pattern with dependent types. Namely:

docs/tutorial/theorems.rst+12−12

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

11.. _sect-theorems:

3−===============

3+***************

44Theorem Proving

5−===============

5+***************

77Equality

8−--------

8+========

1010Idris allows propositional equalities to be declared, allowing theorems about

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

@@ -31,7 +31,7 @@ For example:

3131.. _sect-empty:

3232

3333The Empty Type

34−--------------

34+==============

3535

3636There is an empty type, :math:`\bot`, which has no constructors. It is

3737therefore impossible to construct an element of the empty type, at least

@@ -64,7 +64,7 @@ contradiction.

6464 void : Void -> a

6565

6666Simple Theorems

67−---------------

67+===============

6868

6969When type checking dependent types, the type itself gets *normalised*.

7070So imagine we want to prove the following theorem about the reduction

@@ -116,16 +116,16 @@ We can do the same for the reduction behaviour of plus on successors:

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

117117construct in one go. When things get even slightly more complicated, it

118118becomes too much to think about to construct proofs in this ‘batch

119−mode’.

119+mode’.

120120

121121Idris provides interactive editing capabilities, which can help with

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

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

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

124124

125125.. _sect-totality:

126126

127127Totality Checking

128−-----------------

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

129129

130130If we really want to trust our proofs, it is important that they are

131131defined by *total* functions — that is, a function which is defined for

@@ -195,7 +195,7 @@ total, a function ``f`` must:

195195- Not call any non-total functions

196196

197197Directives and Compiler Flags for Totality

198−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

198+------------------------------------------

199199

200200By default, Idris allows all well-typed definitions, whether total or not.

201201However, it is desirable for functions to be total as far as possible, as this

@@ -216,7 +216,7 @@ Finally, the compiler flag ``--warnpartial`` causes to print a warning

216216for any undeclared partial function.

217217

218218Totality checking issues

219−~~~~~~~~~~~~~~~~~~~~~~~~

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

220220

221221Please note that the totality checker is not perfect! Firstly, it is

222222necessarily conservative due to the undecidability of the halting

@@ -226,14 +226,14 @@ into it so far, so there may still be cases where it believes a function

226226is total which is not. Do not rely on it for your proofs yet!

227227

228228Hints for totality

229−~~~~~~~~~~~~~~~~~~

229+------------------

230230

231231In cases where you believe a program is total, but Idris does not agree, it is

232232possible to give hints to the checker to give more detail for a termination

233233argument. The checker works by ensuring that all chains of recursive calls

234234eventually lead to one of the arguments decreasing towards a base case, but

235235sometimes this is hard to spot. For example, the following definition cannot be

236−checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``

236+checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``

237237will always be smaller than ``(x :: xs)``:

238238

239239.. code-block:: idris

docs/tutorial/typesfuns.rst+29−29

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

11.. _sect-typefuns:

3−===================

3+*******************

44Types and Functions

5−===================

5+*******************

77Primitive Types

8−---------------

8+===============

1010Idris defines several primitive types: ``Int``, ``Integer`` and

1111``Float`` for numeric operations, ``Char`` and ``String`` for text

@@ -71,7 +71,7 @@ work on user defined types. Boolean expressions can be tested with the

7171 "The answer!" : String

7272

7373Data Types

74−----------

74+==========

7575

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

7777similar syntax. Natural numbers and lists, for example, can be

@@ -105,7 +105,7 @@ symbols:

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

106106

107107Functions

108−---------

108+=========

109109

110110Functions are implemented by pattern matching, again using a similar

111111syntax to Haskell. The main difference is that Idris requires type

@@ -175,7 +175,7 @@ numbers. This means it can optimise the representation, and functions

175175such as ``plus`` and ``mult``.

176176

177177``where`` clauses

178−~~~~~~~~~~~~~~~~~

178+-----------------

179179

180180Functions can also be defined *locally* using ``where`` clauses. For

181181example, to define a function which reverses a list, we can use an

@@ -241,10 +241,10 @@ So, for example, the following definitions are legal:

241241 where z w = y + w

242242

243243Dependent Types

244−---------------

244+===============

245245

246246Vectors

247−~~~~~~~

247+-------

248248

249249A standard example of a dependent type is the type of “lists with

250250length”, conventionally called vectors in the dependent type

@@ -322,7 +322,7 @@ two vectors — we needed a vector of length ``k + m``, but provided a

322322vector of length ``k + k``.

323323

324324The Finite Sets

325−~~~~~~~~~~~~~~~

325+---------------

326326

327327Finite sets, as the name suggests, are sets with a finite number of

328328elements. They are available as part of the Idris library, by

@@ -337,12 +337,12 @@ importing ``Data.Fin``, or can be declared as follows:

337337From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.

338338So this is not a set in the sense of a collection that is a container of objects,

339339rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.

340−Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where

340+Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where

341341``n`` is the argument used to instantiate the ``Fin`` type.

342342For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.

343343

344344Let us look at the constructors in greater detail.

345−

345+

346346``FZ`` is the zeroth element of a finite set with ``S k`` elements;

347347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``

348348elements. ``Fin`` is indexed by a ``Nat``, which represents the number

@@ -377,7 +377,7 @@ attempting to look up an element in an empty vector would give a

377377compile time type error, since it would force ``n`` to be ``Z``.

378378

379379Implicit Arguments

380−~~~~~~~~~~~~~~~~~~

380+------------------

381381

382382Let us take a closer look at the type of ``index``:

383383

@@ -420,7 +420,7 @@ help document a function by making the purpose of an argument more

420420clear.

421421

422422“``using``” notation

423−~~~~~~~~~~~~~~~~~~~~

423+--------------------

424424

425425Sometimes it is useful to provide types of implicit arguments,

426426particularly where there is a dependency ordering, or where the

@@ -460,7 +460,7 @@ appear within the block:

460460 There : Elem x xs -> Elem x (y :: xs)

461461

462462Note: Declaration Order and ``mutual`` blocks

463−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

463+---------------------------------------------

464464

465465In general, functions and data types must be defined before use, since

466466dependent types allow functions to appear as part of types, and their

@@ -485,7 +485,7 @@ depend on the reduction behaviour of any of the functions in the

485485block.

486486

487487I/O

488−---

488+===

489489

490490Computer programs are of little use if they do not interact with the

491491user or the system in some way. The difficulty in a pure language such

@@ -542,7 +542,7 @@ example for reading and writing files, including:

542542.. _sect-do:

543543

544544“``do``” notation

545−-----------------

545+=================

546546

547547I/O programs will typically need to sequence actions, feeding the

548548output of one computation into the input of the next. ``IO`` is an

@@ -573,7 +573,7 @@ can be overloaded.

573573.. _sect-lazy:

574574

575575Laziness

576−--------

576+========

577577

578578Normally, arguments to functions are evaluated before the function

579579itself (that is, Idris uses *eager* evaluation). However, this is

@@ -611,7 +611,7 @@ without any explicit use of ``Force`` or ``Delay``:

611611 boolCase False t e = e;

612612

613613Useful Data Types

614−-----------------

614+=================

615615

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

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

@@ -619,7 +619,7 @@ describes a few of these. The functions described here are imported

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

620620

621621``List`` and ``Vect``

622−~~~~~~~~~~~~~~~~~~~~~

622+---------------------

623623

624624We have already seen the ``List`` and ``Vect`` data types:

625625

@@ -692,7 +692,7 @@ remember that Idris is still in development, so if you don’t see

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

693693

694694Aside: Anonymous functions and operator sections

695−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

695+------------------------------------------------

696696

697697There are actually neater ways to write the above expression. One way

698698would be to use an anonymous function:

@@ -719,7 +719,7 @@ by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand

719719to ``\x => 2 * x``.

720720

721721Maybe

722−~~~~~

722+-----

723723

724724``Maybe`` describes an optional value. Either there is a value of the

725725given type, or there isn’t:

@@ -753,7 +753,7 @@ simply ``b``. Since the default value might not be used, we mark it as

753753discarding it would be wasteful.

754754

755755Tuples and Dependent Pairs

756−~~~~~~~~~~~~~~~~~~~~~~~~~~

756+--------------------------

757757

758758Values can be paired with the following built-in data type:

759759

@@ -774,7 +774,7 @@ contain an arbitrary number of values, represented as nested pairs:

774774 jim = ("Jim", 25, "Cambridge")

775775

776776Dependent Pairs

777−~~~~~~~~~~~~~~~

777+---------------

778778

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

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

@@ -852,10 +852,10 @@ We will see more on ``with`` notation later.

852852.. _sect-more-expr:

853853

854854More Expressions

855−----------------

855+================

856856

857857``let`` bindings

858−~~~~~~~~~~~~~~~~

858+----------------

859859

860860Intermediate values can be calculated using ``let`` bindings:

861861

@@ -884,7 +884,7 @@ pattern matching at the top level:

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

885885

886886List comprehensions

887−~~~~~~~~~~~~~~~~~~~

887+-------------------

888888

889889Idris provides *comprehension* notation as a convenient shorthand

890890for building lists. The general form is:

@@ -911,7 +911,7 @@ by the difference between ``a`` and ``b``. This works for any numeric

911911type, using the ``count`` function from the prelude.

912912

913913``case`` expressions

914−~~~~~~~~~~~~~~~~~~~~

914+--------------------

915915

916916Another way of inspecting intermediate values of *simple* types is to

917917use a ``case`` expression. The following function, for example, splits

@@ -965,7 +965,7 @@ matching ``let`` and lambda bindings. It will *only* work if:

965965 itself.

966966

967967Dependent Records

968−-----------------

968+=================

969969

970970*Records* are data types which collect several values (the record's

971971*fields*) together. Idris provides syntax for defining records and

@@ -1036,7 +1036,7 @@ length because it will not affect the type of the record:

10361036 : Class

10371037

10381038Nested record update

1039−~~~~~~~~~~~~~~~~~~~~

1039+--------------------

10401040

10411041Idris also provides a convenient syntax for accessing and updating

10421042nested records. For example, if a field is accessible with the

docs/tutorial/views.rst+4−4

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

11.. _sec-views:

3−=============================

3+*****************************

44Views and the “``with``” rule

5−=============================

5+*****************************

77Dependent pattern matching

8−--------------------------

8+==========================

1010Since types can depend on values, the form of some arguments can be

1111determined by the value of others. For example, if we were to write

@@ -25,7 +25,7 @@ case, the definition would not be well typed.

2525.. _sect-nattobin:

2626

2727The ``with`` rule — matching intermediate values

28−------------------------------------------------

28+================================================

2929

3030Very often, we need to match on the result of an intermediate

3131computation. Idris provides a construct for this, the ``with``