Skip to content
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

Closed
vicuna opened this issue Sep 2, 2016 · 6 comments
Milestone

Comments

@vicuna
Copy link

vicuna commented Sep 2, 2016

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.

@vicuna
Copy link
Author

vicuna commented Sep 2, 2016

Comment author: @gasche

You are perfectly right that the documentation should be clarified, but the idea is indeed that returning None does not include the key in the returned map. So it is a "generalized union" function rather than a union function -- I would agree that the "union" name is a bit awkward in this context.

(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.)

@vicuna
Copy link
Author

vicuna commented Sep 2, 2016

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).

@vicuna
Copy link
Author

vicuna commented Dec 6, 2016

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) =
match find_opt k m1, find_opt k m2 with
| None, None -> None
| Some v1, None -> Some v1
| None, Some v2 -> Some v2
| Some v1, Some v2 -> f v1 v2

I leave this PR open in case we want to update the documentation.

@vicuna
Copy link
Author

vicuna commented Dec 6, 2016

Comment author: @xavierleroy

Alternatively, in terms of merge:

union f m1 m2 is extensionally equal to merge f' m1 m2, where
f' None None = None
f' (Some v1) None = Some v1
f' None (Some v2) = Some v2
f' (Some v1) (Some v2) = f v1 v2

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...

@vicuna
Copy link
Author

vicuna commented Dec 6, 2016

Comment author: @xavierleroy

As you can see, the "find_opt" operation introduced recently in preparation for 4.05 is super useful for specification.

@vicuna
Copy link
Author

vicuna commented Feb 18, 2017

Comment author: @xavierleroy

Documentation added for Map.merge and Map.union in release 4.05.

@vicuna vicuna closed this as completed Feb 18, 2017
@vicuna vicuna added the stdlib label Mar 14, 2019
@vicuna vicuna added this to the 4.05.0 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant