More efficient list encoding for Countable

This changes the encoding used for finite lists of values of countable types to be linear instead of exponential. The encoding works by duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then separating each element with 10. The top 1-bits are not kept since we know a 10 is starting a new element which ends with a 1.

Please don't hold back on feedback. I'm sure this could do with some improvements :)

added 1 commit

• bb3c7917 - More efficient list encoding for Countable

Compare with previous version

mentioned in merge request !61 (closed)

I started thinking a bit more about this, and also how it relates to the issue with namespaces in !61 (closed).

Could we do the following:

• Have functions positives_flatten : list positive → positive and positives_unflatten : positive → list positive in numbers.v that are basically this MRs encode and decode.
• We could then use these in namespaces, without having to duplicate an encoding function there. The proposed positives_flatten function enjoys the suffix property that we need.
• For the Countable instance, we could then use encode xs := positives_flatten (encode <$> xs) and decode p := fmap decode <$> positives_unflatten p.

Does this sound reasonable @jakobbotsch @jung?

I don't understand. positives_flatten : list positive -> positive would be the unary version? If so, then how is that different from what is currently there?

The current encode_list has type list A → positive for any countable A.

In my proposal, we would first define these functions on mere positives (in numbers.v, where we collect all kinds of stuff about positives), and then later lift them to any countable type.

Right, but positives_flatten would need to be my version (or similarly efficient) to solve the exponential problem. You decouple namespaces from countable, but we still need to prove the suffix properties for my encoding. I had some problems proving the _eq one when I tried, but maybe I just didn't stare at it for long enough.

Yes, you are entirely right, positives_flatten should be your version.

In that case sounds reasonable. Shall I move my things to numbers.v then?

Yes, please, but only the flatten/unflatten things, the Countable (list A) instance should remain in countable.v.

Did you mean for positives_unflatten to be positive -> option (list positive)? And is there some elegant monadic way of going from list (option A) to option (list A)?