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

git.iko.soy/Idris-dev

Fix links

commit9202fa1c7690607a76872f9758e36600387013e0 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateTue 25 Aug 2015, 17:17 (11 years ago) parent2fdf033

9 files changed+26−24

compare with master

unifiedsplit

docs/effects/conclusions.rst+10−10 docs/effects/introduction.rst+1−1 docs/effects/state.rst+8−6 docs/faq/faq.rst+1−1 docs/reference/erasure.rst+1−1 docs/reference/uniqueness-types.rst+1−1 docs/tutorial/conclusions.rst+1−1 docs/tutorial/interactive.rst+1−1 docs/tutorial/testing.rst+2−2

docs/effects/conclusions.rst+10−10

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

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

1414following places:

1515

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

1717 library, supporting graphics in particular.

1818

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

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

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

2121 Invaders” game.

2222

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

2424 libraries.

2525

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

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

2727 protocol description language.

2828

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

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

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

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

3939 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

4141

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

4343 effects and handlers, Journal of Logical and Algebraic Methods

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

4545 108-123, ISSN 2352-2208,

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

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

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

47+

4848

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

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

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

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

5353 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+

5556

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

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

5859 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

6061

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

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

6364 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)

6666

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

6868 Functional/Imperative Synthesis (Semantics Structures in

docs/effects/introduction.rst+1−1

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

33************

55Pure 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

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

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

99because 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:

8383

8484.. code-block:: idris

8585

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

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

8787

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

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

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

419419

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

421421 -> (List EFFECT)

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

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

423423

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

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

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

443443 possible.

444444

445445While 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``

447447There are the following three versions:

448448

449449.. code-block:: idris

450450

451451 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) ->

453453 (output_effs : List EFFECT) -> Type

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

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

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

456456

457457So 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.

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

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

523523 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+

525527

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

527529 :width: 500px

docs/faq/faq.rst+1−1

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

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

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

152152Floating-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

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

155155the size is described in the type name.

156156

docs/reference/erasure.rst+1−1

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

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

3030traditional approaches stop being useful, mainly for reasons described

3131in 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>`__.

3333

3434.. code-block:: idris

3535

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

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

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

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

1717ownership types and borrowed pointers in the `Rust

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

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

1919

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

2121include:

docs/tutorial/conclusions.rst+1−1

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

77Further information about Idris programming, and programming with

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

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

1111 questions on the mailing list.

1212

1313- 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

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

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

2222<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

2424available.

2525

2626

docs/tutorial/testing.rst+2−2

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

2323

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

2525

26+.. name: Math/NumOps.idr

2627.. code-block:: idris

27− :caption: Math/NumOps.idr

2828

2929 module Maths.NumOps

3030

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

3636

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

3838

39+.. name: Math/TestOps.idr

3940.. code-block:: idris

40− :caption: Math/TestOps.idr

4141

4242 module Test.NumOps

4343