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.

iv (2) [Avatar] Offline
groupByN doesn't compile

When checking left hand side of with block in Main.groupByN:
    Can't match on with block in Main.groupByN a n (n_xs ++ rest) Exact

After fixing the code to:

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | Exact n_xs = n_xs :: groupByN n rest

I was able to proceed.

groupByN doesn't halt when n = 0

This can be seen in ex 2, where I effectively called groupByN (length [1] `div` 2) [1] = groupByN 0 [1]. Not sure if this is my fault, a bug in the exercise code or unclear instructions.
Edwin Brady (66) [Avatar] Offline
I've fixed the error for the next version, thanks. I think I hadn't kept the text consistent with the code.

groupByN won't terminate if n is 0 (you'll see that Idris doesn't believe it's total, for this reason). I'll add a note on this, especially since termination is covered in the next section.
iv (2) [Avatar] Offline
Thanks! It might also be good to be explicit about how halves should work when given an odd list. The [1] example kind of covers that, but I'd give an example with a longer list (e.g. [1..11]) and explicitly say why we choose to put the longer list second.