Linear Array type with unrestricted gets?

In this particular case, where the array only contains unrestricted a-s, it may be possible to give such a type signature to get. It doesn't scale to a situation where the inner a is linear, but a lot of things get weirder in this case, anyway.

The status of the 0 multiplicity is still in flux, but let's say that one of the possible designs would allow such a signature (as well as length :: [a] %0-> Ur Int, etc…).

We also have come up with another, maybe more general, approach to reduce the syntactic bureaucracy of linear types. We just wrote a paper about it, and it's freshly available in Arxiv: Linear Constraints.

Originally posted by @aspiwack in https://github.com/tweag/linear-base/issues/318#issuecomment-796634908

So, how did this shake out in the end? Does linear haskell have linear Array types with nonlinear unrestricted gets? If not, I'd like to make this a feature request for this. This idea could extend to other read-only ops, allowing potentially large bodies of code to access a large object without requiring linear typing in it. I am thinking about code patterns like this:

newState :: (State -o y) -> y

main :: IO ()
main = let
    loop state = act state >>= \feedback -> state & mutate feedback & loop
    in newState loop

where State is large, act is not linear and mutate is.

Start by reviewing the discussion in issue 318 and the Linear Constraints paper linked there. Determine whether linear Haskell currently supports unrestricted reads from linear arrays and how the proposed design applies to the shown State, act, and mutate pattern. No repository files or tests are identified, so the completion criteria would need to be established first.