93772df · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'siddharthist-fix/tutorial-return'

commit93772df08ddf57a515b75eb43b8d4e8850a8fbec authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateFri 30 Sep 2016, 09:38 (10 years ago) parentecc4bb7 43e7ec9

6 files changed+16−16

compare with master

unifiedsplit

docs/effects/simpleeff.rst+4−4 docs/guides/type-providers-ffi.rst+2−2 docs/reference/ffi.rst+1−1 docs/reference/uniqueness-types.rst+1−1 docs/tutorial/interfaces.rst+6−6 docs/tutorial/typesfuns.rst+2−2

docs/effects/simpleeff.rst+4−4

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

495495 Env = List (String, Integer)

496496

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

498− eval (Val x) = return x

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

498+ eval (Val x) = pure x

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

500500

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

502502subexpressions 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

506506

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

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

509− Just val => return val

509+ Just val => pure val

510510

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

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

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

559559

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

561561 putStrLn (show val)

562− return val

562+ pure val

563563

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

565565error something like the following:

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

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

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

5454 resp <- getLine

5555 case readInt resp of

56− Just sizeTSize => return (Provide sizeTSize)

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

56+ Just sizeTSize => pure (Provide sizeTSize)

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

5858 -- the readInt function is left as an exercise

5959

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

docs/reference/ffi.rst+1−1

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

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

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

363363 (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:

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

213213 putStrLn $ free xs

214214 putStrLn $ f 42

215− return ()

215+ pure ()

216216

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

218218values 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

232232 m_add : Maybe Int -> Maybe Int -> Maybe Int

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

234234 y' <- y -- Extract value from y

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

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

236236

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

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

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

270270.. code-block:: idris

271271

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

273− readNumbers =

273+ readNumbers =

274274 do x <- readNumber

275275 case x of

276276 Nothing => pure Nothing

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

286286.. code-block:: idris

287287

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

289− readNumbers =

289+ readNumbers =

290290 do Just x_ok <- readNumber

291291 Just y_ok <- readNumber

292292 pure (Just (x_ok, y_ok))

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

298298.. code-block:: idris

299299

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

301− readNumbers =

301+ readNumbers =

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

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

304304 pure (Just (x_ok, y_ok))

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

321321.. code-block:: idris

322322

323323 m_add : Maybe Int -> Maybe Int -> Maybe Int

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

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

325325

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

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

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

388388

389389.. code-block:: idris

390390

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

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

392392

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

394394would be:

docs/tutorial/typesfuns.rst+2−2

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

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

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

637637has 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

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

640640

641641.. code-block:: idris

642642

643− return : a -> IO a

643+ pure : a -> IO a

644644

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

646646can be overloaded.