Finite maps and finite sets

[jakobbotsch]

There are a lot of finite map and finite set implementations out there and I think it would be good to discuss what the shape of these types should be in stdlib2. Off the top of my head there are implementations in the stdlib, coq-containers, coq-stdpp and probably others I am not aware of or familiar with. Each of these implementations have different characteristics. Here is an incomplete list of some of them:

stdlib

• Finite maps and finite sets based on modules (no inference)
• Finite sets (but not maps) based on typeclasses
• Different implementations:
  • Ordered and unordered lists of key-value pairs
  • AVL trees

coq-containers

• Based on typeclasses
• Requires a total decidable order on keys, and exhibits many instances:
  • Z, nat, positive, bool, unit
  • Pairs and sums of ordered types
  • Lists of ordered types
  • Finite maps and finite sets of ordered types
• Includes plugin to automatically derive orders for user types which is very convenient
• No extensionality (even for implementations with canonical representations)
• Different implementations:
  • Ordered lists of key-value pairs
  • AVL trees

stdpp

• Based on typeclasses
• Only few types of keys allowed: Z, nat, positive, string (and from a cursory glance seems a little difficult to implement maps with other key types) Maps implemented for any countable type of keys (see comments below)
• Sets implemented in terms of maps
• Extensionality for its maps

If I have gotten anything wrong here then feel free to correct or in general just expand on it.

Personally, as a user coming from object oriented languages, I think that coq-containers was the easiest to use in terms of just working like I would expect. For instance, declaring a map with type Map[A, B] just worked out of the box for even complicated A's. In stdpp it appears you need to find a concrete implementation of a map with your key (Zmap, Nmap, etc.) which is much less discoverable (wrong, there is a finite map for any countable type of keys -- see below). I have not used stdlib extensively, but in my attempts it also seemed to suffer from poor discoverability due to the use of modules. Just figuring out how to make a function that takes an stdlib MSet was a task in itself.

[spitters]

@robbertkrebbers @letouzey

[robbertkrebbers]

In stdpp it appears you need to find a concrete implementation of a map with your key (Zmap, Nmap, etc.) which is much less discoverable.

The map implementation that you probably want to use is gmap K A, it works for any type of keys K that is countable.

Most of the implementations for concrete types like Nmap and Zmap are legacy, and subsumed by gmap. I guess we should document this somewhere :).

[jakobbotsch]

Thank you @robbertkrebbers, I have edited the OP. I need to give stdpp another try in my own development then. 👍