Linear Array type with unrestricted gets? about linear-base HOT 9 OPEN

Wouldn't %0 introduce order of evaluation problems for the places using in place mutation?
What if you destroy an internally used buffer for example then query it, or create a query thunk and then modify it and evaluate the thunk?
I could imagine it working for part that isn't mutated in place (e.g. the Int length if Array a is an Int and Ptr a, rather than a Ptr to a block including the length), but then you are accessing old data.

from linear-base.

The order of evaluation is always clear. In the example I wrote, act is evaluated before mutate. If there were another nonlinear function, it would also be evaluated before mutate. A second linear function would not be allowed though.

from linear-base.

I don't see how it's clear, wouldn't something like this be allowed?

-- x :: X %1
-- observe0 :: X %0 -> B
-- modify1 :: X %1 -> X
let a = observe0 x
    b = observe0 x
    x' = modify1 x
    c = observe0 x
in (a,b,x',c)

Even if let bindings were sequential (which isn't what I typically expect from Haskell code but may be a fact with strict bindings?) there's a problem if either observe0 or modify1 are lazy or if c is allowed, assuming observe reads what modify mutates

from linear-base.

c = observe0 x would be evaluated before x' = modify1 x.

from linear-base.

That's not intuitive to me at all to both make order of evaluation relevant and have the compiler silently re-arrange uses, plus what if there is something polymorphic in multiplicity and the compiler can't dispatch on whether something is 0 or not? It seems more like a band-aid. The way I would expect %0 to work, not useless but far less broadly applicable, is that the order doesn't matter at all unless you are using seq/undefined (as in regular Haskell) and if you have these %0 operations for your type then any of your %1 operations better not modify anything they observe.
There's still the issue of laziness in that example, in which case (in that expression) potentially nothing is even evaluated and the user can control the order by seqing the resulting tuple.

from linear-base.

It is perfectly intuitive. It is just exactly what would happen without linear typing. The only difference is now, it's possible to reuse memory.

from linear-base.

Maybe in another language (though I don't know any that would re-arrange when order matters like that) but it's not exactly what would happen in Haskell, and linear types and ST both already allow re-using memory. Is it so bad to use a linear state monad instead to enforce the order? If you use QualifiedDo or an indexed state monad you can make certain things like extracting the state more convenient.

from linear-base.

Yes, it is exactly what would happen in Haskell. The only difference is how the memory is handled. No monads required.

from linear-base.

In the example above, getting the tuple out of the result does not cause any of the mutation or observation to actually occur if observe0 or modify1 returns a lifted type (which it will since it is being placed in an ordinary haskell tuple).
Even if it wasn't lifted or was !d it might contain a thunk. It's not until you strictly evaluate the components that they start occurring, and in the order you strictly evaluate them.
This would lead to different results from the same argument depending on which part of the tuple you first sequenced.
What you're suggesting above would involve GHC silently inserting seq of its own volition (including on the input so it isn't stored as a thunk), even if this worked in every situation (and again I doubt it can be done when you take multiplicity polymorphism into account) it changes the semantics of strictness for the function unintuitively.
In either case it certainly isn't what GHC would do today and you can see that by writing a non linear version of the above with unsafePerformIO, NOINLINE and IORefs, printing one of the observations, evaluating the modified ioref component and printing another of the observations (which we know are identical expressions, observe0 x for the same x) - it will give different results

from linear-base.