Linear Array type with unrestricted gets?

[ewtoombs]

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 #318 (comment)

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.

[Jashweii]

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.

[ewtoombs]

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.

[Jashweii]

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

[ewtoombs]

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

[Jashweii]

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.

[ewtoombs]

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.

[Jashweii]

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.

[ewtoombs]

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

[Jashweii]

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