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.
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
coq-containers
Z,nat,positive,bool,unitstdpp
Only few types of keys allowed:Maps implemented for any countable type of keys (see comments below)Z,nat,positive,string(and from a cursory glance seems a little difficult to implement maps with other key types)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 ((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.Zmap,Nmap, etc.) which is much less discoverable