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.

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!

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).

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.

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.

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
where
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

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