Andreas Reuleaux (7) [Avatar] Offline
Fine with the NOTE on page 139, suggesting that the reader already familiar with Haskell can continue with section 5.3.

There is however something to be learned even for the experienced Haskeller (some difference worth mentioning in this NOTE maybe):

Whereas in ghci putStrLn evaluates and executes an expression

Prelude > putStrLn "hi"

in Idris evaluation and execution are two different things:

Idris> putStrLn "hi"
io_bind (prim_write "hi\n") (\__bindx => io_return ()) : IO ()
Idris> :exec putStrLn "hi"

then in the following sections, for the reader with no prior Haskell knowledge:

maybe mention that >>= is pronounced "bind", mentioned on pp 141/142 the first time, I think.
(knowing how to pronounce operators / being able to read out code loud,
is generally helpful).

summary 5.4 on page 164:
"We can produce pure values from interactive definitions by using the pure function"

not sure if the wording is well chosen, my understanding is:
"pure takes a pure value and puts it in Applicative"

Idris> :t pure
pure : Applicative f => a -> f a

and one gets a pure value from an interactive definition by executing the action,
and assigning/binding the result, with
action >>= \x => ...

maybe the above should read:
"we can *use* pure values *in* interactive definitions (actions) by putting them in the action
(lifting them into Applicative) with pure"

I just saw that pure is explained on page 148 already, the wording there is better:
"the pure function [...] constructs an IO action, which produces a value, with no other input or output effects"
(thus maybe use this explanation for the summary on page 164 as well)

Another idea: maybe use some boxes/NOTEs: "for the reader already familiar with Haskell" throughout the
text, that way experienced Haskeller's can
* fast skim some parts of the text, and still be sure they get to know the differences between Haskell and Idris

* within these boxes some more advanced concepts (like eg. Applicative/Monad etc) can just be named
(no need for a Haskeller to read through paragraphs motivating monads eg, but not daring to mention the
the word monad yet, just call them "monad" within a box "for the experienced Haskeller") etc.
Edwin Brady (65) [Avatar] Offline
Thanks for the comments. Though I think the distinction between execution and evaluation really is the same as in Haskell, and the difference is the way Idris works at the REPL, where you only get evaluation by default. This is partly because it's often useful to see how the type checker evaluates things.