More efficient `Countable` instance for list and make `namespaces` independent of that.

It turns out we once had a more efficient Countable instance for lists, see 54954f55.

I have reverted that commit and fixed up namespaces.

This closes #28 (closed) ?

Someone an idea which version of Countable is more efficient, the one in this MR or the one in #28 (closed)? It appears that they are both linear at least.

(a) please make this a coqdoc, (b) it might be worth explaining that this is super inefficient and exponential but we don't care, and we do need namespace_encode_suffix.

Yes, that's a good idea. It might also be explaining what this stuff is doing at all. I have just been porting the old Countable stuff for lists without actually understanding what I was doing :P

Do you still recall how this works? I have to admit, I forgot...

Uh... the point is to be able to represent "the upclosure of a namespace" as a coPset. Somehow, for that to work, namespace needs to have a particular encoding as a positive...?

Someone an idea which version of Countable is more efficient, the one in this MR or the one in #28 (closed)? It appears that they are both linear at least.

I like how this reuses some existing infrastructure.

@jakobbotsch could you check if this version if "fast enough" for you, maybe even benchmark it against the one you wrote?

This implementation was the first thing I tried. Unfortunately this is exponential in the length of the list, which for most cases is even worse! The problem is the way products are interleaved. At each additional element, the encoding will double in size.

It is not really because products are interleaved -- using the list encoding (duplicating bits) in products would have the same problem. I think it would work if products change encoding to have the first projection length-prefixed (for example, duplicate bits to encode the length and then just encode the actual projection without duplication). Then an iterated product will not explode in size.

Right, thanks!

Am I correct that your encoding is doing the following:

• For each list element, turn 0 into 00 and 1 into 11.
• Glue all elements together using 10 as a separator

Yes, that's exactly how it works although it also discards the last 1-bit of each element (the separator means a new element is starting and we know its last bit will be 1).

So, I guess the best way forward is that I only include the namespace part in this MR and @jakobbotsch makes another MR for the new list encoding?

Following up on that, @jakobbotsch if you like, you could already make the MR, and just leave namespaces broken. Once this lands, you can rebase.

Done. !62 (merged)

mentioned in merge request !62 (merged)

!62 (merged) subsumes this MR. Closing.

closed