Vincent Semeria (Oct 01 2020 at 10:29): Vincent Semeria (Oct 01 2020 at 10:29):The doc of native arrays https://coq.github.io/doc/master/refman/language/core/primitive.html?highlight=primitive#primitive-arrays mentions "the most recent copy of an array" but does not tell when such arrays are copied. For example, consider a singleton nat array initialized to 7, what is the result of this computation ?
a.[0] + a.[0 <- 2].[0]
Depending on whether we evaluate the left or right term of the addition first, the result is either 9 or 4. Or maybe the array is copied before, so that the 2 addition terms don't interact, but then what is the state of the array after the whole addition ?
Paolo Giarrusso (Oct 01 2020 at 10:52):The evaluation order isn’t part of the interface. But that doesn’t affect results, because these arrays don’t expose mutable state.
Paolo Giarrusso (Oct 01 2020 at 10:53):Ignoring optimizations, “modifying” an array really creates an entirely separate array with the updated contents, and leaves the original array aside.
Maxime Dénès (Oct 01 2020 at 10:55):@Vincent Semeria the exposed interface is functional, otherwise it would break consistency
Paolo Giarrusso (Oct 01 2020 at 10:55):in your specific case, the 2 addition terms don’t interact, and the a remains the same
Maxime Dénès (Oct 01 2020 at 10:55):so, as @Paolo Giarrusso wrote, the result does not depend on the evaluation order
Vincent Semeria (Oct 01 2020 at 10:56):Then what does the doc mean by "Update and access to an element in the most recent copy of an array are constant time operations." ? Each set copies the array, that's a linear time operation, not constant time.
Paolo Giarrusso (Oct 01 2020 at 10:57):I said “ignoring optimizations” ;-)
Paolo Giarrusso (Oct 01 2020 at 10:58):“persistent data structure” is a technical term that the text takes for granted, and the text won’t make sense until you look it up.
Paolo Giarrusso (Oct 01 2020 at 10:59):and the manual should probably be fixed not to do that so much — at least the core point about semantics can be explained otherwise.
Paolo Giarrusso (Oct 01 2020 at 10:59):I also have no clue how to implement a persistent _array_, so I cannot comment there — most persistent data structures are easier.
Paolo Giarrusso (Oct 01 2020 at 11:01):e.g., you could define an inefficient set : nat -> list T -> list T in Coq, with similar semantics
Maxime Dénès (Oct 01 2020 at 11:01):@Vincent Semeria isn't there a pointer in the manual chapter?
Maxime Dénès (Oct 01 2020 at 11:01):to the paper explaining the data structure?
Maxime Dénès (Oct 01 2020 at 11:01):if there isn't, it was forgotten
Paolo Giarrusso (Oct 01 2020 at 11:01):there is such a pointer.
Maxime Dénès (Oct 01 2020 at 11:02):so, if you want to know how it is implemented, you can look up the paper
Maxime Dénès (Oct 01 2020 at 11:02):if you want to know the behavior, the manual description seems correct
Paolo Giarrusso (Oct 01 2020 at 11:02):is “persistent union-find” the right paper?
Maxime Dénès (Oct 01 2020 at 11:03):I think so, yes, by Filliâtre and Cochon
Paolo Giarrusso (Oct 01 2020 at 11:03):but my point was that most readers would be helped already by a link to Wikipedia on “persistent data structures”
Maxime Dénès (Oct 01 2020 at 11:04):yep, I wouldn't mind adding such a link if that's helpful
Paolo Giarrusso (Oct 01 2020 at 11:04):and they probably don’t need to read the specific paper
Maxime Dénès (Oct 01 2020 at 11:04):well, it depends, the paper explains how to do it for an array
Maxime Dénès (Oct 01 2020 at 11:04):I don't know what the wikipedia page says
Paolo Giarrusso (Oct 01 2020 at 11:05):I’m not proposing to drop the link to the paper
Paolo Giarrusso (Oct 01 2020 at 11:05):but I’ll wait for Vincent’s answer to say more.
Vincent Semeria (Oct 01 2020 at 11:11):The only purpose of native arrays is to optimize lists, so the efficiency of this optimization should be given in Coq's manual. At least a summary of it, so that we know when to use native arrays without reading a 9-page research paper. If each set operation copies the full array it would be a disaster for speed and memory, but the article of Filliâtre and Cochon looks like it's smarter.
Enrico Tassi (Oct 01 2020 at 11:38):I think the best to is write an informal definition of persistent. Something like: It is a functional data structures that offers the performances of the corresponding mutable data structure if don't keep a pointer to an old copy of it. If you do, it is still sound, but it has to keep the history of the changes so that the old copy can be reconstructed on demand. @Vincent Semeria would a sentence like this one have helped you?
Vincent Semeria (Oct 01 2020 at 11:46):@Enrico Tassi Yes, what you describe is clearer. The Coq's manual could say it is enough to read section 2.3 of Filliâtre's article, the rest of their union-find problem is out of scope here. I would also ban the word "copy", because the persistent array is never copied. The implementation looks more like the decorator pattern https://en.wikipedia.org/wiki/Decorator_pattern, where you start with a base object and stack up modifications on it.
Enrico Tassi (Oct 01 2020 at 12:54):Then would you mind opening a PR/issue on Coq with the proposed text.
I'm also OK mentioning the decorator pattern if it speaks to a larger audience, but AFAICT a decorator can be a static feature, while here it the logging is really at runtime, so one may need to add a few words to avoid this kind of confusion.
Enrico Tassi (Oct 01 2020 at 12:55):(I'm not very familiar with OO design patterns)
Vincent Semeria (Oct 01 2020 at 14:10):@Enrico Tassi Decorator is at runtime. I'll do the PR to Coq.
Vincent Semeria (Oct 01 2020 at 16:42):@Enrico Tassi Here is the PR https://github.com/coq/coq/pull/13125/files
Karl Palmskog (Oct 01 2020 at 23:24):this is a nice overview of what persistence means: https://existentialtype.wordpress.com/2011/04/09/persistence-of-memory/
Karl Palmskog (Oct 01 2020 at 23:27):
Last updated: May 31 2023 at 03:30 UTC