The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Thu, May 14, 2020 at 12:35 AM Gregory Malecha <gmalecha AT gmail.com> wrote:

Hello --

I am wondering what people suggest as an efficient representation of finite maps. Normally I use positive maps but for this purpose I have a *very* sparse key space so it actually makes sense to store pairs of the key and the element. The standard library has an implementation of AVL trees, but the proof term that is store with data is prohibitively expensive.

I can attest that, after extraction to OCaml, Coq's FMapAVL are very efficient.  So it must be the proof terms, indeed.  If I understand correctly, maps are represented by sigma-types `{m : Raw.t | wf m }`, and the proof term for `wf m` is never evaluated.  Yet, the proof term grows by a constant factor every time an "add" or "remove" operation is performed.  So, after N adds and M removes from the empty map, the map has size O(N + M).  Is that what makes it "prohibitively expensive"?

The problem I see here is that most efficient data structures I can think of are not freely generated by constructors, but have richer structural invariants that need to be maintained using predicates and proof terms.  (For example, Frédéric Besson mentioned Patricia trees.  I played with them in Coq a while ago and they have plenty of structural invariants.)  So, this phenomenon of proof terms growing linearly with the number of operations performed seems hard to avoid.

It could be that there is a fundamental tension between 1) having efficient data structures, and 2) building valid proof terms.  That would make me sad.

Best,

- Xavier Leroy

 

Are there other implementations of finite maps that the community can recommend?

Thanks.

--

gregory malecha

gmalecha.github.io