Are there any libraries that build on and extend the array theory? For example, providing functionality like decidable equality and such.

`stdpp`

build lots of theory for finite map theory and then instantiate that on lists and vectors (fixed size arrays with dependent typing for the size) as finite maps from integers to values. It also provides decidable equality for those. I don't know if that helps

@Gregory Malecha which array theory? Are you thinking of Coq’s new primitive arrays?

Specifically, I'm thinking about the Coq `PArray`

.

For context, I have a (fairly) memory-efficient representation of strings using arrays and need to fill in some of the theory to actually make it a replacement for coq-bytestring (http://coq.io/opam/coq-bytestring.0.9.0.html)

to clarify, the memory efficiency is very important in this context since I've got a lot of fairly long strings in my file, but I do almost no computation on them

@Gregory Malecha I’ve never seen a generic library on PArray but I’d be curious for an even more efficient bytestring implementation :) I feel we’re missing an initialization function in PArray to build basically immutated strings efficiently: `A -> int -> (int -> A) -> array A`

I feel it might also be beneficial to have a primitive char/uint8 datatype to use instead of Byte.byte. In many applications we compare bytes and currently the most efficient implementation with just two matches on byte takes an enormous amount of memory due to code size. In MetaCoq we switched back to doing comparison on N by converting byte to N but it should really be constant time. Another option would be to use `int`

to represent bytes as that’s not more wasteful at the Coq level (tByte of char and tInt of Int63.t take the same space I think, on 64 bits architectures). However when we can’t extract that anymore to `char`

(e.g in CertiCoq) without losing confidence

@Matthieu Sozeau I agree on byte. Currently in the bytestring library I believe that we convert to `positive`

to do the comparison, but it isn't ideal and should be constant time.

I have an implementation based on packing 7 characters into an int63. The downside is that there are 7 wasted bits which means that there is junk in the representation so `=`

is not exactly what you'd ideally want, but it is 7x smaller than other representations

Related to strings...it would be nice to have C-style escapes, e.g. "\n". That probably isn't something that you would be need, but it would make Coq a bit more uniform with the rest of the world ;-)

Last updated: Sep 26 2023 at 13:01 UTC