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. + a.[0 <- 2].
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 ?
The evaluation order isn’t part of the interface. But that doesn’t affect results, because these arrays don’t expose mutable state.
Ignoring optimizations, “modifying” an array really creates an entirely separate array with the updated contents, and leaves the original array aside.
@Vincent Semeria the exposed interface is functional, otherwise it would break consistency
in your specific case, the 2 addition terms don’t interact, and the
a remains the same
so, as @Paolo Giarrusso wrote, the result does not depend on the evaluation order
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.
I said “ignoring optimizations” ;-)
“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.
and the manual should probably be fixed not to do that so much — at least the core point about semantics can be explained otherwise.
I also have no clue how to implement a persistent _array_, so I cannot comment there — most persistent data structures are easier.
e.g., you could define an inefficient
set : nat -> list T -> list T in Coq, with similar semantics
@Vincent Semeria isn't there a pointer in the manual chapter?
to the paper explaining the data structure?
if there isn't, it was forgotten
there is such a pointer.
so, if you want to know how it is implemented, you can look up the paper
if you want to know the behavior, the manual description seems correct
is “persistent union-find” the right paper?
I think so, yes, by Filliâtre and Cochon
but my point was that most readers would be helped already by a link to Wikipedia on “persistent data structures”
yep, I wouldn't mind adding such a link if that's helpful
and they probably don’t need to read the specific paper
well, it depends, the paper explains how to do it for an array
I don't know what the wikipedia page says
I’m not proposing to drop the link to the paper
but I’ll wait for Vincent’s answer to say more.
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.
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?
@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.
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.
(I'm not very familiar with OO design patterns)
@Enrico Tassi Decorator is at runtime. I'll do the PR to Coq.
@Enrico Tassi Here is the PR https://github.com/coq/coq/pull/13125/files
this is a nice overview of what persistence means: https://existentialtype.wordpress.com/2011/04/09/persistence-of-memory/
Last updated: Jan 29 2023 at 08:28 UTC