93772df · 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+6−6

@@ -232,7 +232,7 @@ Using this we can, for example, define a function which adds two

232 m_add : Maybe Int -> Maybe Int -> Maybe Int

233 m_add x y = do x' <- x -- Extract value from x

234 y' <- y -- Extract value from y

235− return (x' + y') -- Add them

235+ pure (x' + y') -- Add them

236

237This function will extract the values from ``x`` and ``y``, if they

238are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the

@@ -270,7 +270,7 @@ on the result of ``readNumber``:

270.. code-block:: idris

271

272 readNumbers : IO (Maybe (Nat, Nat))

273− readNumbers =

273+ readNumbers =

274 do x <- readNumber

275 case x of

276 Nothing => pure Nothing

@@ -286,7 +286,7 @@ we could try pattern matching on values of the form ``Just x_ok``:

286.. code-block:: idris

287

288 readNumbers : IO (Maybe (Nat, Nat))

289− readNumbers =

289+ readNumbers =

290 do Just x_ok <- readNumber

291 Just y_ok <- readNumber

292 pure (Just (x_ok, y_ok))

@@ -298,7 +298,7 @@ case back as follows:

298.. code-block:: idris

299

300 readNumbers : IO (Maybe (Nat, Nat))

301− readNumbers =

301+ readNumbers =

302 do Just x_ok <- readNumber | Nothing => pure Nothing

303 Just y_ok <- readNumber | Nothing => pure Nothing

304 pure (Just (x_ok, y_ok))

@@ -321,7 +321,7 @@ shorthand version, as follows:

321.. code-block:: idris

322

323 m_add : Maybe Int -> Maybe Int -> Maybe Int

324− m_add x y = return (!x + !y)

324+ m_add x y = pure (!x + !y)

325

326The notation ``!expr`` means that the expression ``expr`` should be

327evaluated and then implicitly bound. Conceptually, we can think of

@@ -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.