[ new ] Seq1

[Matthew-Mosior]

This PR adds Seq1 (Sized/Unsized), a linear (with thread-safe operations) Seq (Sized/Unsized).

[stefan-hoeck]

I have a question about this (and similar mutable and size-indexed data structures in here): If we use functions like cons, snoc but also tail on a Seq1 s n e, we get a new Seq1 s m e with a different size, but we may still use the original mutable value (which points to the same mutable reference internally), which will now - however - store a finger tree of size m internally. Is this safe and sound? I don't see how it can be.

[Matthew-Mosior]

I have a question about this (and similar mutable and size-indexed data structures in here): If we use functions like cons, snoc but also tail on a Seq1 s n e, we get a new Seq1 s m e with a different size, but we may still use the original mutable value (which points to the same mutable reference internally), which will now - however - store a finger tree of size m internally. Is this safe and sound? I don't see how it can be.

I've been thinking about this as well (before I create documentation for this repo).

In general, most of the functions associated with the mutable (postfixed 1) version of a given data structure are thread-safe, however, some will not be and inherently can't be, since they return an altered version of a respective mutable value.

Some examples of this:

• (++) operator for Seq1 (Sized/Unsized), which returns a new mutable value containing the result of appending two mutable Seq1s (with altering the original mutable values).
• take/drop for Seq1 (Sized/Unsized), which both return a new mutable value (without altering the original mutable value).

So I think this should be fine, since with those functions, we actually aren't internally mutating the original to create the new (we aren't utilizing applying any cas_ functions the original mutable value to create the new value).

Although, now I see that viewl and viewr, which underly head, last, tail, and toList, internally modify the original mutable value via casswap1, so I need to revisit these to ensure we aren't modifying the original mutable value.

[stefan-hoeck]

I actually don't see the point of this. Why have a mutable finger tree in the first place? What use is it to store this in and retrieve it from an mutable reference? Why not just use the immutable inner value instead?

[Matthew-Mosior]

I actually don't see the point of this. Why have a mutable finger tree in the first place? What use is it to store this in and retrieve it from an mutable reference? Why not just use the immutable inner value instead?

The idea behind the *1 versions are that they are thread-safe, so they can be used without issue in a multi-threaded environment.

For example, a thread-safe Seq might be used to implement a concurrent task scheduler.

[stefan-hoeck]

So you only need the immutable data structure in a mutable reference plus a CAS-loop for thread-safe mutation. Again, please have a look at idris2-async. I'd also argue that such a data structure is highly specialized. Not sure it should be in a general-purpose container library.

My main concern is that we currently have a whole bunch of container types in this library, quite a few of which seem to be actually unsound.

[Matthew-Mosior]

So you only need the immutable data structure in a mutable reference plus a CAS-loop for thread-safe mutation. Again, please have a look at idris2-async. I'd also argue that such a data structure is highly specialized. Not sure it should be in a general-purpose container library.

My main concern is that we currently have a whole bunch of container types in this library, quite a few of which seem to be actually unsound.

True, wrapping a given immutable data structure in a mutlable reference and utilizing CAS-loop allows for thread-safe mutation.

Yeah, I can see how this stuff is specialized, although they are essentially wrappers around a more basic immutable version, which is why I thought they might be nice to include in this library.

I believe the only unsound types as of now are Seq1 and BoundedQueue1, which I can work on fixing (as far as I can tell, RRBVector1 should be okay, but I'll look more at those as well).

I'm open to thinning down this library if you (or the community) feels strongly that these thread-safe mutable versions are out of scope for this library.

[stefan-hoeck]

I think the three issues currently open sum up my thoughts on this:

• The types should be safe and sound: An index of 10 should mean that the internal container always holds at least 10 values.
• Thread safety must be properly verified under high contention.
• We need documentation and examples for use cases (see [ doc ] Explain typical use cases for RRBVector1 and documentation in general #50 ).

If these are properly addressed, then I think we should be fine.