43e7ec9 · Idris-dev · git.iko.soy

docs/effects/simpleeff.rst+4−4

compare with master

unifiedsplit

@@ -495,8 +495,8 @@ values:

495 Env = List (String, Integer)

496

497 eval : Expr -> Eff Integer [EXCEPTION String, STATE Env]

498− eval (Val x) = return x

498+ eval (Val x) = pure x

499− eval (Add l r) = return $ !(eval l) + !(eval r)

499+ eval (Add l r) = pure $ !(eval l) + !(eval r)

500

501Note that we are using ``!``-notation to avoid having to bind

502subexpressions in a ``do`` block. Next, we add a case for evaluating

@@ -506,7 +506,7 @@ subexpressions in a ``do`` block. Next, we add a case for evaluating

506

507 eval (Var x) = case lookup x !get of

508 Nothing => raise $ "No such variable " ++ x

509− Just val => return val

509+ Just val => pure val

510

511This retrieves the state (with ``get``, supported by the ``STATE Env``

512effect) and raises an exception if the variable is not in the

@@ -559,7 +559,7 @@ has been generated:

559

560 eval (Random upper) = do val <- rndInt 0 upper

561 putStrLn (show val)

562− return val

562+ pure val

563

564If we try this without extending the effects list, we would see an

565error something like the following:

docs/guides/type-providers-ffi.rst+2−2

@@ -53,8 +53,8 @@ actions. Let's write a simple one now:

53 putStrLn "I'm sorry, I don't know how big size_t is. Can you tell me, in bytes?"

54 resp <- getLine

55 case readInt resp of

56− Just sizeTSize => return (Provide sizeTSize)

56+ Just sizeTSize => pure (Provide sizeTSize)

57− Nothing => return (Error "I'm sorry, I don't understand.")

57+ Nothing => pure (Error "I'm sorry, I don't understand.")

58 -- the readInt function is left as an exercise

59

60We assume that whoever's compiling the library knows the size of

docs/reference/ffi.rst+1−1

@@ -361,4 +361,4 @@ timeouts:

361 timeout <- jscall "setTimeout(%0, %1)"

362 (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)

363 (MkJsFn f) millis

364− return $ MkTimeout timeout

364+ pure $ MkTimeout timeout

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

@@ -212,7 +212,7 @@ the following sort of bad program being implemented:

212 foo xs = do let f = \x : Int => showU xs

213 putStrLn $ free xs

214 putStrLn $ f 42

215− return ()

215+ pure ()

216

217Since ``lend`` is implicit, in practice for functions to lend and borrow

218values merely requires the argument to be marked as ``Borrowed``. We can

docs/tutorial/interfaces.rst+1−1

@@ -388,7 +388,7 @@ Then the comprehension is converted to ``do`` notation:

388

389.. code-block:: idris

390

391− do { qual1; qual2; ...; qualn; return exp; }

391+ do { qual1; qual2; ...; qualn; pure exp; }

392

393Using monad comprehensions, an alternative definition for ``m_add``

394would be:

docs/tutorial/typesfuns.rst+2−2

@@ -635,12 +635,12 @@ The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of

635type ``IO a``, and puts the result, of type ``a`` into the variable

636``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``

637has type ``String``. Indentation is significant — each statement in

638−the do block must begin in the same column. The ``return`` operation

638+the do block must begin in the same column. The ``pure`` operation

639allows us to inject a value directly into an IO operation:

640

641.. code-block:: idris

642

643− return : a -> IO a

643+ pure : a -> IO a

644

645As we will see later, ``do`` notation is more general than this, and

646can be overloaded.