The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

..., including the the exact word to be guessed

(the only once)
A minor thing, but nevertheless: In the course of developing checkEqNat in the Type/Define/Refine style

in step 6 (Define) Just eq is introduced (instead of Just x):

...We'll rename the Just x produced by the case split to something
more informative, and fill in the case where the recursive call
produces Nothing:

 checkEqNat (S k) (S j) = case checkEqNat k j of
                               Nothing => Nothing
                               Just eq => ?checkEqNat_rhs_2



Just eq is also used in step 8 (Refine, page 249), and step 9 (Refine, p 249)

Consequently when I work through the example and
look at the type of ?checkEqNat_rhs_2 in step 7
I get to see eq as well in the premisses:

  k : Nat
  j : Nat
  eq : EqNat k j
--------------------------------------
Main.checkEqNat_rhs_2 : Maybe (EqNat (S k) (S j))


ie. eq, not rec_eq as is currently printed for step 7 in the book:

  k : Nat
  j : Nat
  rec_eq : EqNat k j
--------------------------------------
checkEqNat_rhs_2 : Maybe (EqNat (S k) (S j))

OK, at the end of chapter 6 I have learned quite a lot about Idris and IO,
and have seen quite an impressive example (the data store, now refined).

However, if I am not mistaken: all the complete programs, that I have seen so
far, that involve IO, are examples of REPL programs (they use either repl or
replWith), ie. endless cycles of getting input from the user and giving back
answers (until the user explicitly quits the program).

While it's certainly worth knowing these kind of programs (and one can
learn a lot about IO along the way), REPL programs are rarely the
first ones I write when learning a new language.

I typically start out much simpler, with a program that gets some
input from the command line, like the example below (taking a recent
example from the mailing list: fibs, but many other examples one could
think of: Celcius to Fahrenheit or whatever). The point here is that
with getArgs one can build nifty little programs (that can be useful
in day to day work, and replace some shell scripts maybe). Maybe
something like this is worth showing in the book as well?


module Main


-- fibs : Stream Integer

fibs : Stream Nat
fibs = 1 :: 1 :: zipWith (+) fibs (tail fibs)


main : IO ()
main = do 
         (cmd::args) <- getArgs
         case args of
              []     => putStrLn "need an argument"
              (s::_) => putStrLn $ show $ take (cast $ s) fibs          
         return ()



p 212, second sentence n section 7.1.3:
"In some cases, methods are so closely related that they we can..."
should read
"...that we can..."






in the final listing 4.19 parseCommand takes a list of String

parseCommand: List String -> Maybe Command

whereas on the pages before it was explained to be of type:

parseCommand : String -> String -> Maybe Command.

Consequently the function parse (that calls parseCommand) is
different as well:

* in the final listing it's body is just:
parseCommand (words input)

* whereas on page 131 it was explained as:
case span (/= ' ') input of
(cmd, args) => parseCommand (ltrim args)

I assume the final listing should be in line with the explanations before,
or otherwise these further changes (simplifications) should be
mentioned.
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"
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"
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
x<-action
or
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.
"That is, in the pattern (x :: xs), word is a String, words is a vector of k Strings, and
for the output we need to provide a vector of Nat of length 1 + k, represented as S k."

should read (I would guess):
"That is, in the pattern (word :: words), ..."

(word::words) was introduced on p 74 already to make the pattern easier to read