286919 (2) [Avatar] Offline
#1
The final line of listing 4.15:
addToData (item :: items) = item :: addToData items


wouldn't compile for me, until I changed items to items'

Not sure if it was matching against the items defined earlier in the outer function?
Edwin Brady (65) [Avatar] Offline
#2
Which Idris version? Everything is checked against the latest version, which works fine, and I am cleaning up some things as I go, so it'll probably be a good idea to check you have the latest Idris when each chapter is released.
justjoheinz (6) [Avatar] Offline
#3
Is there an advantage/reason to implement the function as suggested over:

addToStore: (store: DataStore) -> String -> DataStore
addToStore (MkDataStore size items) x = MkDataStore (S size ) (x :: items)


(In my first version of the implementation I wrote (size +1) which does not typecheck. How could I get hold of the proof (I know - not covered yet), that (n + 1 = S nat)?

Markus

Edwin Brady (65) [Avatar] Offline
#4
If you do it as you suggest, the new items will go at the beginning of the list rather than the end, so when looking up by index, every time you add an item the index of items you've previously added will change. So it's adding things at the end to avoid that.

As for the proof, it's a little tricky without having already explained the details of equality (which is going to be introduced in Chapter 6) but if you'd like to look ahead, take a look at the prelude function 'replace', and the brief tutorial at http://docs.idris-lang.org/en/latest/proofs/index.html.

More detail on this is coming soon, I promise smilie.
justjoheinz (6) [Avatar] Offline
#5
Given that my implementation was an error in terms of the desired implementation, and that the interface of the signature did not give a hint about the implementation, it would be interesting to know how a List type/proof could be designed which prohibits changing ids of its contents. I know that this is far ahead of the material already being covered smilie
286919 (2) [Avatar] Offline
#6
Edwin Brady wrote:Which Idris version? Everything is checked against the latest version, which works fine, and I am cleaning up some things as I go, so it'll probably be a good idea to check you have the latest Idris when each chapter is released.


Verision is 0.9.19.1 - I think this is the latest version?
Perhaps a typo on my part somewhere.
(4) [Avatar] Offline
#7
The latest version is 0.9.20.1 at this moment, however I can reproduce the same error with this version, so I guess there is either a regression in the latest version, or the example should be modified (replacing items with items', as OP suggested, works).

Update: in chapter 5 from listing 5.9 onwards this variable is renamed to store.
371392 (9) [Avatar] Offline
#8
I also see this error with version 0.9.20.
3354 (2) [Avatar] Offline
#9
I saw this error too. I think it's a clash of names (items in the outer addToStore scope and again in the inner addToData). If I rename items to items' it type checks. I.e., the revised listing that works for me is:

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newitem = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newitem]
    addToData (item' :: items') = item' :: addToData items'
Debasish Ghosh (116) [Avatar] Offline
#10
Yes .. I think there's a name clash of items with the enclosing addToStore. Changing to items' fixes the issue.