Ditch `FinMap` interface, and only have `gmap`
The map interface FinMap
and many of its instances natmap
, Pmap
, Nmap
, Zmap
predate the generic map implementation gmap
. We often have questions on Mattermost about the use of other map implementations, and the answer is always: "use gmap
".
There are some other issues with the generic setup:
- Lemmas have many implicit type class parameters, so if you do
Check
/About
, or see them inSearch
results they are difficult to read. - These type class parameters of operations that involve maps with different keys (e.g.,
kmap
ormap_preimage
) and the domain operations are even more complicated. - If you use a lemma wrongly, the errors can be interesting...
- In Iris we already specialize maps to
gmap
. So it's kind of challenging what you should use in aSearch
. If you want to have a map lemma that involves Iris constructs, you need to search forgmap
, if you want to have a generic map lemma, you need to search forFinMap
. Especially for non-experts this is not trivial to figure out.
So, the question is: Are there any uses of non-gmap
implementations, or major advantages of this generic setup? Or should we just specialize to gmap
?
I can come up with some reasons against:
- The interface is useful to ensure abstraction. However, proving anything in terms of the implementation of
gmap
is so complicated that the abstraction boundary is easily enforced by the reviewer of an MR. - If Coq ever gets quotients, a compelling use of the abstraction is to allow for more interesting instances, e.g., AVL trees or red-black trees. But as long as we do not have quotients, these implementations won't be instances of the interface since they don't have canonical representations (they thus violate
m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i
. - Similarly, the interface would allow for such instances if we generalize to setoids. (But that makes the interface even more generic, and thus difficult to use).
- We want to keep the generic setup for sets. After all, for sets we have implementations other than
gset
that have their own pros and cons:coPset
(which we use extensively in Iris for masks),propset
(not used that often, but useful if you want potentially infinite sets),listset
(which is a monad laws,gset
is not).