Susan Harkins (274) [Avatar] Offline
#1
Please post errors found in the published version of Type-Driven Development with Idris here. If necessary, we'll publish a comprehensive list. Thank you!

Susan Harkins
Errata Editor
Manning Publications
Ilya Yanok (16) [Avatar] Offline
#2
It's a minor one, but on the page 49, the first line of the output of the :doc repl is truncated.
Ilya Yanok (16) [Avatar] Offline
#3
Page 67, under 4 Type:
words is a vector of kStrings
should be words is a vector of k Strings.
Ilya Yanok (16) [Avatar] Offline
#4
Page 249, above the Listing 9.6:
elem follows a structure similar to decElem

should be

elem follows a structure similar to isElem
Ilya Yanok (16) [Avatar] Offline
#5
Page 256 mentions guess function (twice) but there is no function with this name in this section! Probably, it was meant to be game or processGuess (I think this paragraph is actually talking about both of them).
Ilya Yanok (16) [Avatar] Offline
#6
Page 287,
For both showItems and filterKeys
should be

For both listItems and filterKeys

Also on the same page
implementations of showItems and filterKeys
should be

implementations of listItems and filterKeys
Ilya Yanok (16) [Avatar] Offline
#7
Exercise 3 on page 305 should be exercise 5.
Ilya Yanok (16) [Avatar] Offline
#8
Chapter 15, Figure 15.1 caption
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.
Ilya Yanok (16) [Avatar] Offline
#9
Page 410, Listing 15.5.
printLn "Send failed"

should be

printLn "Receive failed"
Ilya Yanok (16) [Avatar] Offline
#10
This is a small bug in the doCount function on page 430, Listing 15.19
mkWCData lcount wcount

should be

mkWCData wcount lcount

This results in the wrong doCount output on the same page:
MkWCData 2 3 : WCData

should be

MkWCData 3 2 : WCData

as well as incorrect output of the whole word-counting example on the page 433:

Words: 4
Lines: 7

should be

Words: 7
Lines: 4
241018 (1) [Avatar] Offline
#11
P.65, paragraph just before 'Overloading names' has typo in
of :: and Nil : 1 :: 2 :: 3 :: Nil
Artem Pelenitsyn (1) [Avatar] Offline
#12
P. 354, Listing 13-1
data DoorCmd : Type where
should be
data DoorCmd : Type -> Type where
.
Alex Gryzlov (3) [Avatar] Offline
#13
p.347:
This simplifies the definition of quiz, at the cost of making the definition of ConsoleIO more complex.


ConsoleIO here should probably be changed to Command, since the latter's definition changes in the chapter, not the former's. There's even an explicit comment about that earlier on p.342:
There’s no need to update ConsoleIO, because it merely sequences Commands.
Alex Gryzlov (3) [Avatar] Offline
#14
pp. 369-370:

Listing 13.12 starts with:
data StkInput = Number Integer
              | Add

strToInput : String -> Maybe StkInput

Yet Listing 13.13 begins with
strToInput : String -> Maybe RPNInput

(RPNInput should be changed to StkInput)
William DeMeo (2) [Avatar] Offline
#15
p. 120

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


should be

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


(note the third `->` is missing)

zilinc (4) [Avatar] Offline
#16
241018 wrote:P.65, paragraph just before 'Overloading names' has typo in
of :: and Nil : 1 :: 2 :: 3 :: Nil


I personally don't think it's a typo, but just poor wording w.r.t. fonts.
It wants to say "... to a sequence of :: and Nil[, which is] 1 :: 2 :: 3 :: Nil, in this case.
zilinc (4) [Avatar] Offline
#17
P209, bullet point 3 should be:
Returning True whether ....
B.C. van Duuren (1) [Avatar] Offline
#18
Page 119 under bullet point 4 " Using integerToFin, as described in section 4.2.34.2.3" should be "Using integerToFin, as described in section 4.2.3".
Susan Harkins (274) [Avatar] Offline
#19
Adam Gashlin (3) [Avatar] Offline
#20
pg. 113 Listing 4.16 addToData should use another name for items, as published it produces this error:
When checking left hand side of Main.addToStore, addToData:
Can't match on Main.addToStore, addToData (S size)
                                          size
                                          items
                                          newitem
                                          (item :: items)

I think due to a clash with addToStore's parameter of the same name.
MichelNielsen (7) [Avatar] Offline
#21
Listing 12.23 and Listing 12.24

setDifficulty : Nat -> GameState -> GameState


should be

setDifficulty : Int -> GameState -> GameState
Vilem (2) [Avatar] Offline
#22
p436: to install the atom editor plugin, one can also invoke
apm install language-idris


This assumes that Atom > Install Shell Commands has been run on the system at some point (mac).
Vilem (2) [Avatar] Offline
#23
p27:
SUBTRACTION WITH NATS Because Nats can never be negative, a Nat can only be subtracted from a larger or equal Nat.
519065 (1) [Avatar] Offline
#24
Page 294
Chapter 11
Listing 11.1

Missing comma in the type signature of label.

label : List a -> List (Integer a)


Should instead be:

label : List a -> List (Integer, a)
155078 (3) [Avatar] Offline
#25
Error in the errata: "p430 In listing 15.9, the last line should be: MkWCData wcount lcount." should read "... 15.19 ..."
155078 (3) [Avatar] Offline
#26
pg 255, "Invalid guess <----- Putput by readGuess" ; should be "Output"
155078 (3) [Avatar] Offline
#27
pg277, fairly sure that

isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc rec) | (Snoc z)

should be

isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec)
Brandon Dyck (1) [Avatar] Offline
#28
pg 376, Figure 14.3
data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState)

should be
data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type