9202fa1 · Idris-dev · git.iko.soy

docs/effects/conclusions.rst+10−10

compare with master

unifiedsplit

@@ -13,17 +13,17 @@ paper [1]_.

13Some libraries and programs which use ``Effects`` can be found in the

14following places:

15

16−- http://github.com/edwinb/SDL-idris — some bindings for the SDL media

16+- https://github.com/edwinb/SDL-idris — some bindings for the SDL media

17 library, supporting graphics in particular.

18

19−- http://github.com/edwinb/idris-demos — various demonstration

19+- https://github.com/edwinb/idris-demos — various demonstration

20 programs, including several examples from this tutorial, and a “Space

21 Invaders” game.

22

23- https://github.com/SimonJF/IdrisNet2 — networking and socket

24 libraries.

25

26−- http://github.com/edwinb/Protocols — a high level communication

26+- https://github.com/edwinb/Protocols — a high level communication

27 protocol description language.

28

29The inspiration for the ``Effects`` library was Bauer and Pretnar’s

@@ -37,32 +37,32 @@ foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.

37.. [1] Edwin Brady. 2013. Programming and reasoning with algebraic

38 effects and dependent types. SIGPLAN Not. 48, 9 (September

39 2013), 133-144. DOI=10.1145/2544174.2500581

40− http://doi.acm.org/10.1145/2544174.2500581

40+ https://dl.acm.org/citation.cfm?doid=2544174.2500581

41

42.. [2] Andrej Bauer, Matija Pretnar, Programming with algebraic

43 effects and handlers, Journal of Logical and Algebraic Methods

44 in Programming, Volume 84, Issue 1, January 2015, Pages

45 108-123, ISSN 2352-2208,

46− http://dx.doi.org/10.1016/j.jlamp.2014.02.001.

46+ http://math.andrej.com/wp-content/uploads/2012/03/eff.pdf

47− (http://www.sciencedirect.com/science/article/pii/S2352220814000194)

47+

48

49.. [3] Ben Lippmeier. 2009. Witnessing Purity, Constancy and

50 Mutability. In Proceedings of the 7th Asian Symposium on

51 Programming Languages and Systems (APLAS '09), Zhenjiang Hu

52 (Ed.). Springer-Verlag, Berlin, Heidelberg,

53 95-110. DOI=10.1007/978-3-642-10672-9_9

54− http://dx.doi.org/10.1007/978-3-642-10672-9_9

54+ http://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9

55+

55

56

56.. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in

57.. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in

57 action. SIGPLAN Not. 48, 9 (September 2013),

58 action. SIGPLAN Not. 48, 9 (September 2013),

58 145-158. DOI=10.1145/2544174.2500590

59 145-158. DOI=10.1145/2544174.2500590

59− http://doi.acm.org/10.1145/2544174.2500590

60+ https://dl.acm.org/citation.cfm?doid=2544174.2500590

60

61

61.. [5] Martin Hyland, Gordon Plotkin, John Power, Combining effects:

62.. [5] Martin Hyland, Gordon Plotkin, John Power, Combining effects:

62 Sum and tensor, Theoretical Computer Science, Volume 357,

63 Sum and tensor, Theoretical Computer Science, Volume 357,

63 Issues 1–3, 25 July 2006, Pages 70-99, ISSN 0304-3975,

64 Issues 1–3, 25 July 2006, Pages 70-99, ISSN 0304-3975,

64− http://dx.doi.org/10.1016/j.tcs.2006.03.013.

65− (http://www.sciencedirect.com/science/article/pii/S0304397506002659)

65+ (https://www.sciencedirect.com/science/article/pii/S0304397506002659)

66

67.. [6] Paul Blain Levy. 2004. Call-By-Push-Value: A

68 Functional/Imperative Synthesis (Semantics Structures in

docs/effects/introduction.rst+1−1

@@ -3,7 +3,7 @@ Introduction

3************

4

5Pure functional languages with dependent types such as `Idris

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

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

7in the type system, promising that we can *know* a program will run

8correctly (i.e. according to the specification in its type) simply

9because it compiles. Realistically, though, things are not so simple:

docs/effects/state.rst+8−6

@@ -83,7 +83,7 @@ effectful program ``f`` has a type of the following form:

83

84.. code-block:: idris

85

86− f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs

86+ f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs

87

88That is, the return type gives the effects that ``f`` supports

89(``effs``, of type ``List EFFECT``) and the type the computation

@@ -419,7 +419,7 @@ underlying type ``EffM``:

419

420 EffM : (m : Type -> Type) -> (t : Type)

421 -> (List EFFECT)

422− -> (t -> List EFFECT) -> Type

422+ -> (t -> List EFFECT) -> Type

423

424This is more general than the types we have been writing so far. It is

425parameterised over an underying computation context ``m``, a

@@ -443,15 +443,15 @@ operations which can change the set of available effects are:

443 possible.

444

445While powerful, this can make uses of the ``EffM`` type hard to read.

446−Therefore the library provides an overloaded function ``Eff``

446+Therefore the library provides an overloaded function ``Eff``

447There are the following three versions:

448

449.. code-block:: idris

450

451 SimpleEff.Eff : (t : Type) -> (input_effs : List EFFECT) -> Type

452− TransEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->

452+ TransEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->

453 (output_effs : List EFFECT) -> Type

454− DepEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->

454+ DepEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->

455 (output_effs_fn : x -> List EFFECT) -> Type

456

457So far, we have used only the first version, ``SimpleEff.Eff``, which

@@ -521,7 +521,9 @@ the ``new`` function, though this is beyond the scope of this tutorial.

521.. [3] Edwin Brady. 2013. Programming and reasoning with algebraic

522 effects and dependent types. SIGPLAN Not. 48, 9 (September

523 2013), 133-144. DOI=10.1145/2544174.2500581

524− http://doi.acm.org/10.1145/2544174.2500581

524+ http://dl.acm.org/citation.cfm?doid=2544174.2500581

525+

526+

525

527

526.. |image| image:: ../image/effects-tree.png

528.. |image| image:: ../image/effects-tree.png

527 :width: 500px

529 :width: 500px

docs/faq/faq.rst+1−1

@@ -150,7 +150,7 @@ names ``Float`` and ``Double`` to represent floating point numbers of

150size 32 and 64 respectivly. Newer languages such as Rust and Julia

151have begun to follow the naming scheme described in `IEE Standard for

152Floating-Point Arithmetic (IEEE 754)

153−<http://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes

153+<https://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes

154single and double precision numbers as ``Float32`` and ``Float64``;

155the size is described in the type name.

156

docs/reference/erasure.rst+1−1

@@ -29,7 +29,7 @@ and we can use irrelevance-related methods to achieve erasure.

29However, sometimes we want to erase *indices* and this is where the

30traditional approaches stop being useful, mainly for reasons described

31in the `original proposal

32−<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.

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

33

34.. code-block:: idris

35

docs/reference/uniqueness-types.rst+1−1

@@ -15,7 +15,7 @@ They are inspired by linear types, `Uniqueness Types

15<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean

16<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

17ownership types and borrowed pointers in the `Rust

18−<http://www.rust-lang.org/>`__ programming language.

18+<https://www.rust-lang.org/>`__ programming language.

19

20Some things we hope to be able to do eventually with uniqueness types

21include:

docs/tutorial/conclusions.rst+1−1

@@ -7,7 +7,7 @@ Further Reading

7Further information about Idris programming, and programming with

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

9

10−- The Idris web site (http://idris-lang.org/) and by asking

10+- The Idris web site (http://www.idris-lang.org/) and by asking

11 questions on the mailing list.

12

13- The IRC channel ``#idris``, on

docs/tutorial/interactive.rst+1−1

@@ -20,7 +20,7 @@ hole, and even a basic proof search mechanism. In this

20section, we explain how these features can be exploited by a text

21editor, and specifically how to do so in `Vim

22<https://github.com/idris-hackers/idris-vim>`_. An interactive mode

23−for `Emacs <https://github.com/idris-hackers/idris-emacs>`_ is also

23+for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also

24available.

25

26

docs/tutorial/testing.rst+2−2

@@ -23,8 +23,8 @@ does not aggregate test results.

23

24For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

25

26+.. name: Math/NumOps.idr

26.. code-block:: idris

27.. code-block:: idris

27− :caption: Math/NumOps.idr

28

29 module Maths.NumOps

30

@@ -36,8 +36,8 @@ For example, lets take the following list of functions that are defined in a mod

36

37A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

38

39+.. name: Math/TestOps.idr

39.. code-block:: idris

40.. code-block:: idris

40− :caption: Math/TestOps.idr

41

42 module Test.NumOps

43