|Anonymous | Login | Signup for a new account||2018-06-23 21:58 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007343||OCaml||standard library||public||2016-09-02 17:01||2017-02-18 16:49|
|Priority||normal||Severity||text||Reproducibility||have not tried|
|Target Version||4.05.0 +dev/beta1/beta2/beta3/rc1||Fixed in Version|
|Summary||0007343: request for clarification about Map.Make.union (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t|
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,
|Tags||No tags attached.|
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.)
|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).|
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.
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...
|As you can see, the "find_opt" operation introduced recently in preparation for 4.05 is super useful for specification.|
|Documentation added for Map.merge and Map.union in release 4.05.|
|2016-09-02 17:01||berenger||New Issue|
|2016-09-02 17:08||gasche||Note Added: 0016263|
|2016-09-02 17:08||frisch||Note Added: 0016264|
|2016-09-07 16:46||shinwell||Target Version||=> 4.05.0 +dev/beta1/beta2/beta3/rc1|
|2016-12-06 20:06||xleroy||Note Added: 0016656|
|2016-12-06 20:06||xleroy||Severity||minor => text|
|2016-12-06 20:06||xleroy||Status||new => acknowledged|
|2016-12-06 20:09||xleroy||Note Added: 0016657|
|2016-12-06 20:12||xleroy||Note Added: 0016658|
|2017-02-18 16:49||xleroy||Note Added: 0017332|
|2017-02-18 16:49||xleroy||Status||acknowledged => resolved|
|2017-02-18 16:49||xleroy||Resolution||open => fixed|
|2017-02-23 16:43||doligez||Category||OCaml standard library => standard library|
|Copyright © 2000 - 2011 MantisBT Group|