Errata: January 30, 2019

Thank you for purchasing Type-Driven Development with Idris. We'll update this list as necessary. Thank you!

Unless otherwise noted, all corrections are pending in all versions.

Page 49:

The documentation for repl should read as follows:

Idris> :doc repl
Prelude.Interactive.repl : (prompt : String) ->
    (onInput : String -> String) -> IO ()
    A basic read-eval-print loop
    Arguments:
        prompt : String  -- the prompt to show

        onInput : String -> String  -- the function to run on reading
        input, returning a String to output 

Page 65:

"words is a vector of kStrings" should read as "words is a vector of k Strings."

Page 119:

The reference to "section 4.2.34.2.3", should read "section 4.2.3."

Page 120:

In the listing at the top of the page that reads:

getEntry : (pos : Integer) -> (store : DataStore) -> (input : String) 
           Maybe (String, DataStore)

there should be an "->" before Maybe, i.e.:

getEntry : (pos : Integer) -> (store : DataStore) -> (input : String) 
           -> Maybe (String, DataStore)

Page 249:

"elem follows a structure similar to decElem" should be "elem follows a structure similar to isElem."

Page 256

References to the guess function should be to the processGuess function.

Page 287

All mentions of showItems on this page should be listItems.

Page 305:

Exercise 3 should be Exercise 5.

Page 347:

"This simplifies the definition of quiz, at the cost of making the definition of ConsoleIO more complex" - ConsoleIO should be Command.

Page 354:

In listing 13.1 data DoorCmd : Type should be data DoorCmd : Type -> Type.

Page 360:

In Listing 13.4, in the line Refill : (bars : Nat) -> the word Refill should begin in the same column as GetCoins in the line above, and the : should be aligned with the : in the line above.

Page 405:

In the caption for Figure 15.1, "if lines A and C are executed before lines C and D" should be "if lines A and C are executed before lines B and D."

Page 410:

In the program listing "Send failed" should be "Receive failed".

Page 430:

In listing 15.19, the last line should be: MkWCData wcount lcount.