After having used the fast-vect library and really come to appreciate the static guarantees provided by it (shoutout to @sigma-andex for the amazing work there), I’ve found a few cases where this addition could be useful.
Just dropping the PR with the proposed addition to the library here in case anyone would also find it useful.
sigma-andex:main ← albertprz:min-len-vect
opened 02:33PM - 22 Nov 23 UTC
## Rationale
The current `Vect` API provided in `Data.FastVect.FastVect` can … be useful in many scenarios where arrays are created statically. However, in cases when dealing with dynamically sized vectors, still partial static length information can be preserved throughout multiple transformations. This PR aims to leverage the existing `Vect` implementation to have some static guarantees for dynamically sized arrays and possibly to enable one unifed API to many operations performed on either an `Array` or a `NonEmptyArray` by offering a more lax guarantee on the type level index.
One particular application of this could be that appending a dynamically sized `Array` to a `Vect` would preserve the minimum length information of the resulting `MinLenVect` being able to safely index or extract as many elements from the resulting `MinLenVect` up to the `Vect` length. Also inspired by the Haskell [minlen package](https://hackage.haskell.org/package/minlen).
## New `MinLenVect` API
Included `Data.FastVect.MinLenVect` module for minimum length indexed vectors.`MinLenVect` newtype replicating `Vect`. The API is the same as for `Vect` with the exception of:
- Exclusion of the `adjust` and `adjustM` functions as it does not make much sense to have those for minimum length indexed vectors IMO
- `fromArray` successfully generates a `MinLenVect` in case the array length is greater or equal than the supplied type level minimum length index.
- Inclusion of `fromNonEmptyArray`
- Inclusion of `fromUnsizedArray` and `fromUnsizedNonEmptyArray` , that only take the array as an argument and return a `MinLenVect 0 elem` and a `MinLenVect 1 elem` in each case.
- Inclusion of `toVect` that attempts to convert to a standard length indexed `Vect` if the array length is equal to the type level minimum length index and `fromVect` that just converts a `Vect` to a `MinLenVect`
## Implementation
The implementation is the same as in `Data.FastVect.FastVect` except for the few API changes in the new module, which could be a concern for maintability because of all the code duplication. I was not aware how to keep both APIs completely separate without exposing implementation details in neither of them and at the same time avoid all the duplication. I guess one option could be to extract the common API from both modules into a common one, but that would be more intrusive in terms of modifying the existing `Vect` API in `Data.FastVect.FastVect`