You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 6138 Reporter:@ppedrot Status: acknowledged (set by @damiendoligez on 2013-08-26T15:00:34Z) Resolution: open Priority: normal Severity: feature Category: standard library Tags: patch
Bug description
It would be nice to have a domain function in the Map functor, i.e. recovering the set of the keys contained in the map, with the following signature:
module Make(Ord:OrderedType) :
sig
...
val domain : 'a t -> Set.Make(Ord).t
...
end
which would be essentially identity, except for forgetting the additional node information worn by the map node. That would result in a O(n) operation, while currently one has to do it by hand by using Map.fold and Set.add, resulting in a O(n log n) operation.
Actually, we do this operation quite often in Coq, so that it would be nice to have it built-in more efficiently.
Additional information
I made a hackish implementation using unsafe features, and attached it to this message, to see the point.
This is an interesting suggestion, thanks. What worries me is that even if we put "domain" inside the implementation of Map.Make, we still need unsafe features to build the set of keys -- the type sealing around Set.Make is that strong. Or we'd need to duplicate the implementation of Set inside Map...
Yet another way would be for Map.Make to export a substructure (let's call it Keys) that would have the exact same signature as Set.Make(Ord) but be implemented internally as maps. This would make "domain" a constant-time operation.
What about merging the two functors into a single one? For instance, one could arrange so that Map.Make(Ord) contains a Set submodule, and re-export a Set functor for backward compatibility (with a sharing constraint so that Set.Make(Ord).t = Map.Make(Ord).Set.t).
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.
Original bug ID: 6138
Reporter: @ppedrot
Status: acknowledged (set by @damiendoligez on 2013-08-26T15:00:34Z)
Resolution: open
Priority: normal
Severity: feature
Category: standard library
Tags: patch
Bug description
It would be nice to have a domain function in the Map functor, i.e. recovering the set of the keys contained in the map, with the following signature:
module Make(Ord:OrderedType) :
sig
...
val domain : 'a t -> Set.Make(Ord).t
...
end
which would be essentially identity, except for forgetting the additional node information worn by the map node. That would result in a O(n) operation, while currently one has to do it by hand by using Map.fold and Set.add, resulting in a O(n log n) operation.
Actually, we do this operation quite often in Coq, so that it would be nice to have it built-in more efficiently.
Additional information
I made a hackish implementation using unsafe features, and attached it to this message, to see the point.
File attachments
The text was updated successfully, but these errors were encountered: