Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007343OCamlstandard librarypublic2016-09-02 17:012017-02-18 16:49
Assigned To 
PrioritynormalSeveritytextReproducibilityhave not tried
PlatformOSOS Version
Product Version4.03.0 
Target Version4.05.0 +dev/beta1/beta2/beta3/rc1Fixed in Version 
Summary0007343: 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,
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
gasche (administrator)
2016-09-02 17:08

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.)
frisch (developer)
2016-09-02 17:08

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).
xleroy (administrator)
2016-12-06 20:06

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.
xleroy (administrator)
2016-12-06 20:09

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...
xleroy (administrator)
2016-12-06 20:12

As you can see, the "find_opt" operation introduced recently in preparation for 4.05 is super useful for specification.
xleroy (administrator)
2017-02-18 16:49

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

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker