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.

steshaw (13) [Avatar] Offline
The definition of ListLast in the book is incorrect:
data ListLast : List a -> Type where
     Empty : ListLast []
     NonEmpty : (init : List a) -> (x : a) -> ListLast (xs ++ [x])

This was a bit difficult to spot since it compiles OK. For the NonEmpty constructor, the result type should read ListLast (init ++ [x]).

As a side-node, I've noticed this kind of thing happening from time to time with Idris (i.e. typos/mistakes introducing an implicit variable that isn't "connected" to the rest of the definition). I wonder if it might be possible for Idris to detect these situations?
steshaw (13) [Avatar] Offline
A little followup. When starting to define describe_help, it's probably better to start with List Int, rather than the given List a:
describe_help : (input : List a) -> (form : ListLast input) -> String
describe_help input form = ?describe_help_rsh

Otherwise it's easy to get into a situation such as:
describeHelp : (input : List a) -> (form : ListLast input) -> String
describeHelp [] Empty = "Empty"
describeHelp (init ++ [x]) (NonEmpty init x) = "Non-empty, initial portion =   " ++ show init

This code fails to compile with an unhelpful message:
When checking right hand side of describeHelp with expected type

Can't disambiguate since no name has a suitable type:
Prelude.List.++, Prelude.Strings.++

This happens because of the code: ++ show init. Unfortunately, there is no implementation of Show for a (the element type of the list).

Note that the refine step in the book does switch the type to List Int but it's easy to miss as I did.
Edwin Brady (66) [Avatar] Offline
I think I did mean it to be List Int all along too... I think I've edited the final definition here but missed the earlier ones. Thanks for spotting.

That's a good idea about the implicit error message too - it's a mistake I sometimes make. I'll have to think about the implications (it will sometimes be intentional after all) but some kind of warning does seem useful.
steshaw (13) [Avatar] Offline
I was hoping that it would be possible to have an error message but I spotted another example later in the book which has an implicit introduced in the result type (Ex and they probably come up more often than I was thinking. Pity because I've really been struggling sometimes to find the source of the error. Still, you've always got a compiling version in the source code for the book but I find I learn more if I can avoid using that except when necessary.
Edwin Brady (66) [Avatar] Offline
Even in this case, you could suppresss the warning with an implicit binding `{rest : _} ->` so maybe it's not so bad. But there's also situations which will come up later (in Chapter 13/14) involving state machines in types where this would start to get a bit noisy.

I'll try to think of something anyway...