32fc703 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3034 from jfdm/doc-fixes

Doc fixes

commit32fc7035cf99b1981e44357944f0f1b238ce0c75 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateFri 18 Mar 2016, 14:41 (11 years ago) parentec97cac 8f2456f

2 files changed+27−13

compare with master

unifiedsplit

docs/effects/simpleeff.rst+11−10 docs/tutorial/typesfuns.rst+16−3

docs/effects/simpleeff.rst+11−10

@@ -578,16 +578,17 @@ this simply by updating the type of ``eval`` to include ``STDIO``.

578578

579579 eval : Expr -> Eff Integer [STDIO, EXCEPTION String, RND, STATE Env]

580580

581−Note that using ``STDIO`` will restrict the number of contexts in

582−which ``eval`` can be ``run`` to those which support ``STDIO``, such

583−as ``IO``. Once effect lists get longer, it can be a good idea instead

584−to encapsulate sets of effects in a type synonym. This is achieved as

585−follows, simply by defining a function which computes a type, since

586−types are first class in Idris:

581+.. note:: Using ``STDIO`` will restrict the number of contexts in

582+ which ``eval`` can be ``run`` to those which support

583+ ``STDIO``, such as ``IO``. Once effect lists get longer, it

584+ can be a good idea instead to encapsulate sets of effects in

585+ a type synonym. This is achieved as follows, simply by

586+ defining a function which computes a type, since types are

587+ first class in Idris:

587588

588−.. code-block:: idris

589+ .. code-block:: idris

589590

590− EvalEff : Type -> Type

591− EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]

591+ EvalEff : Type -> Type

592+ EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]

592593

593− eval : Expr -> EvalEff Integer

594+ eval : Expr -> EvalEff Integer

docs/tutorial/typesfuns.rst+16−3

@@ -137,7 +137,7 @@ Unlike Haskell, there is no restriction on whether types and function

137137names must begin with a capital letter or not. Function names

138138(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,

139139``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are

140−all part of the same namespace. By convention, however,

140+all part of the same namespace. By convention, however,

141141data types and constructor names typically begin with a capital letter.

142142We can test these functions at the Idris prompt:

143143

@@ -495,9 +495,20 @@ vector. For example:

495495 testVec : Vect 4 Int

496496 testVec = 3 :: 4 :: 5 :: 6 :: Nil

497497

498− inVect : IsElem 5 testVec

498+ inVect : IsElem 5 Main.testVec

499499 inVect = There (There Here)

500500

501+

502+.. important:: Implicit Arguments and Scope

503+

504+ Within the type signature the typechecker will treat all variables

505+ that start with an lowercase letter **and** are not applied to

506+ something else as an implicit variable. To get the above code

507+ example to compile you will need to provide a qualified name for

508+ ``testVec``. In the example above, we have assumed that the code

509+ lives within the ``Main`` module.

510+

511+

501512If the same implicit arguments are being used a lot, it can make a

502513definition difficult to read. To avoid this problem, a ``using`` block

503514gives the types and ordering of any implicit arguments which can

@@ -510,6 +521,8 @@ appear within the block:

510521 Here : IsElem x (x :: xs)

511522 There : IsElem x xs -> IsElem x (y :: xs)

512523

524+

525+

513526Note: Declaration Order and ``mutual`` blocks

514527~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

515528

@@ -583,7 +596,7 @@ example for reading and writing files, including:

583596

584597 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

585598 closeFile : File -> IO ()

586−

599+

587600 fGetLine : (h : File) -> IO (Either FileError String)

588601 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())

589602 fEOF : File -> IO Bool