Stream: Miscellaneous

Topic: Native arrays


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Oct 01 2020 at 10:55):

@Vincent Semeria the exposed interface is functional, otherwise it would break consistency

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Oct 01 2020 at 10:55):

so, as @Paolo Giarrusso wrote, the result does not depend on the evaluation order

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 01 2020 at 10:57):

I said “ignoring optimizations” ;-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:01):

@Vincent Semeria isn't there a pointer in the manual chapter?

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:01):

to the paper explaining the data structure?

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:01):

if there isn't, it was forgotten

view this post on Zulip Paolo Giarrusso (Oct 01 2020 at 11:01):

there is such a pointer.

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:02):

if you want to know the behavior, the manual description seems correct

view this post on Zulip Paolo Giarrusso (Oct 01 2020 at 11:02):

is “persistent union-find” the right paper?

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:03):

I think so, yes, by Filliâtre and Cochon

view this post on Zulip 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”

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:04):

yep, I wouldn't mind adding such a link if that's helpful

view this post on Zulip Paolo Giarrusso (Oct 01 2020 at 11:04):

and they probably don’t need to read the specific paper

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:04):

well, it depends, the paper explains how to do it for an array

view this post on Zulip Maxime Dénès (Oct 01 2020 at 11:04):

I don't know what the wikipedia page says

view this post on Zulip Paolo Giarrusso (Oct 01 2020 at 11:05):

I’m not proposing to drop the link to the paper

view this post on Zulip Paolo Giarrusso (Oct 01 2020 at 11:05):

but I’ll wait for Vincent’s answer to say more.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 01 2020 at 12:55):

(I'm not very familiar with OO design patterns)

view this post on Zulip Vincent Semeria (Oct 01 2020 at 14:10):

@Enrico Tassi Decorator is at runtime. I'll do the PR to Coq.

view this post on Zulip Vincent Semeria (Oct 01 2020 at 16:42):

@Enrico Tassi Here is the PR https://github.com/coq/coq/pull/13125/files

view this post on Zulip 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/

view this post on Zulip Karl Palmskog (Oct 01 2020 at 23:27):

chart.png


Last updated: Aug 19 2022 at 20:03 UTC