New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
request for clarification about Map.Make.union (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t #7343
Comments
Comment author: @gasche You are perfectly right that the documentation should be clarified, but the idea is indeed that returning (Note: the reason why the two input maps are asked to be at the same type is that keys that have a binding in only one of the two maps are reused as is. It could also be mentioned because I keep forgetting about it. For type-changing transformations the less efficient "merge" can be used.) |
Comment author: @alainfrisch The semantics is indeed that the key is dropped when the function returns None. Perhaps the documentation should be more explicit about it (and I agree the name might be a bit confusing, but it's too late to change it). |
Comment author: @xavierleroy If I may venture a formal specification, this would be: forall f m1 m2 k, find_opt k (union f m1 m2) = I leave this PR open in case we want to update the documentation. |
Comment author: @xavierleroy Alternatively, in terms of merge: union f m1 m2 is extensionally equal to merge f' m1 m2, where Moreover, forall f m1 m2 k, find_opt k (merge f m1 m2) = f (find_opt k m1) (find_opt k m2) It's so much clearer with formal specs... |
Comment author: @xavierleroy As you can see, the "find_opt" operation introduced recently in preparation for 4.05 is super useful for specification. |
Comment author: @xavierleroy Documentation added for Map.merge and Map.union in release 4.05. |
Original bug ID: 7343
Reporter: berenger
Status: resolved (set by @xavierleroy on 2017-02-18T15:49:51Z)
Resolution: fixed
Priority: normal
Severity: text
Version: 4.03.0
Target version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Category: standard library
Bug description
Hello,
Let's say someone must implement another map, that must expose the same interface and behavior than the map of the stdlib.
What is the precise semantics of this f function ?
In: Map.union f m1 m2
what should implementers do in case (f v1 v2) returns None ?
Should the key k (bound to v1 in m1 and v2 in m2) be dropped ?
Then, the output map would not hold a union of the key sets and
the function would look badly named.
Should I assert(false) ?
Should I consistently choose v1 (or v2) ?
Thanks a lot,
F.
The text was updated successfully, but these errors were encountered: