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.

Susan Harkins (424) [Avatar] Offline
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
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
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
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
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
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
Exercise 3 on page 305 should be exercise 5.
Ilya Yanok (16) [Avatar] Offline
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
Page 410, Listing 15.5.
printLn "Send failed"

should be

printLn "Receive failed"
Ilya Yanok (16) [Avatar] Offline
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
P.65, paragraph just before 'Overloading names' has typo in
of :: and Nil : 1 :: 2 :: 3 :: Nil
Artem Pelenitsyn (1) [Avatar] Offline
P. 354, Listing 13-1
data DoorCmd : Type where
should be
data DoorCmd : Type -> Type where
Alex Gryzlov (3) [Avatar] Offline
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
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
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
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
P209, bullet point 3 should be:
Returning True whether ....
B.C. van Duuren (1) [Avatar] Offline
Page 119 under bullet point 4 " Using integerToFin, as described in section" should be "Using integerToFin, as described in section 4.2.3".
Adam Gashlin (3) [Avatar] Offline
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)
                                          (item :: items)

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

setDifficulty : Nat -> GameState -> GameState

should be

setDifficulty : Int -> GameState -> GameState
Vilem (2) [Avatar] Offline
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
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
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
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
pg 255, "Invalid guess <----- Putput by readGuess" ; should be "Output"
155078 (3) [Avatar] Offline
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
pg 376, Figure 14.3
data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState)

should be
data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type
Kostiantyn Rybnikov (2) [Avatar] Offline
Could somebody explain the "expected result" from listToTree in chapter 4 exercises? With this code:

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x (Node left val right) = case compare x val of
                                      LT => Node (insert x left) val right
                                      EQ => Node left val right
                                      GT => Node left val (insert x right)

listToTree : Ord a => List a -> Tree a
listToTree xs = go xs Empty
    go : List a -> Tree a -> Tree a
    go [] acc = acc
    go (x :: xs) acc = go xs (insert x acc)

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node tree x tree1) = treeToList tree ++ [x] ++ treeToList tree1

I'm getting:

??> listToTree [1,4,3,5,2]
Node Empty
     (Node (Node (Node Empty 2 Empty) 3 Empty) 4 (Node Empty 5 Empty)) : Tree Integer

But the book says I should get:

Node (Node Empty 1 Empty)
     (Node (Node Empty 3 (Node Empty 4 Empty)) 5 Empty)

Both are fine but I can't work out book's implementation out of the result.
io.nathan (1) [Avatar] Offline
Due to changes in Idris 1.2.0 where an additional Abs interfaces was introduced, the example of listing 7.9 of page 196 and 197 does not work anymore as printed. One must add the Abs interface in the constraints on num of eval, remove the abs method implementation from Neg Expr and and implement Abs for Expr:

eval : (Neg num, Integral num, Abs num) => Expr num -> num

Neg ty => Neg (Expr ty) where
  negate x = 0 - x
  (-)      = Sub

Abs ty => Abs (Expr ty) where
  abs = Abs
536055 (1) [Avatar] Offline
In Chapter 10 section 10.2.3 - Traversing multiple arguments: nested with blocks

In Step 4. Refine, the 4th pattern match for isSuffix is this

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

It should be

isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec)
Susan Harkins (424) [Avatar] Offline
An updated errata list for Type-Driven Development with Idris is available at Thanks for participating in this process. Your comments help us and other readers.

Susan Harkins
Errata Editor