Linear Mutable Arrays with Linear Values via Ownership

[Divesh-Otwani]

Is your feature request related to a problem? Please describe.

We can't have linear values inside Data.Array.Mutable.Linear because then we can't freeze. Namely,

freeze :: Array (Array Int) %1-> Ur (Vector (Array Int))

would be unsafe because the inner arrays can now be read and duplicated, though they are mutable references which need to be single-threaded.

Describe the solution you'd like

We can get around this with some notion of an ownership witness that allows you to freeze because using the inner values requires the witness. This is incorrect but gets at the rough idea:

data Arr :: Own -> Type -> Type where ...

deepFreeze :: Arr o (Arr o' Int) -> Owned o %1-> Ur (Vector (Arr o' Int), Owned o')

use :: Owned o %1-> (Owned o %1-> Ur b) %1-> Ur b
write :: Arr o a -> Int -> a %1-> Owned o %1 -> (Arr o' a, Owned o')

This ^ will require some careful thought to tease out.

[utdemir]

This is incorrect but gets at the rough idea

I don't get it :). flip use seems like just id, and I don't see how that Owned would witness the linearity without doing existential tricks like ST.

But I was wondering about a similar issue recently, so I just wanted to share what I was thinking:

---

I was thinking about changing the implementation of an Array (and other mutable collections, except HashMap keys, and Set's) to store linear values instead. So, the current implementation would be isomorphic to Array (Ur a). This would require considerable changes to the interface:

• We won't be able to implement read, but we can still have modify.
• Functions like Array.resize will need to be accommodated for consuming the values and creating new ones.

But, on the plus side we could have type ArrayU a = Array (Ur a) and implement something similar to the current interface to work on ArrayU's (there might be some performance costs from the extra indirection).

However, there still are some problematic functions, especially freeze. Because then the freeze needs to have a signature like Array (Ur a) %1-> Ur (Vector a), but then we wouldn't be able to do a constant time cast since we would need to unwrap the Ur's.

So, I thought the complexity on the interface wouldn't be worth it; but it might be advantageus in future to have a separate variant of an Array with linear contents (something between V and []).

---

However, if your ownership idea allows us to solve this (without incurring significant interface complexity), I'd be very happy with that. If it'd be costly, simply creating a new linear Array type with linear contents would be simple enough, I think (althought I guess it still won't have a constant time freeze, if the values are lazy; but I can not think of a way to have a linear value inside an unrestricted collection with unrestricted accessors; unless we implement a dual to Ur which wouldn't be referentially transparent).

[Divesh-Otwani]

I don't get it :). flip use seems like just id, and I don't see how that Owned would witness the linearity without doing existential tricks like ST.

Neither do I, but maybe some ownership like thing could work. Perhaps, we use existentials somewhere or something. Another idea is to provide an unrestricted vector, but maybe reads return an allocation function:

deepFreezeRead :: Vector (Arr Int) -> Int -> ((Arr Int %1-> Ur b) %-> Ur b)
-- calling this twice on the same index, should return a copy, but each copy is itself mutable

This is an open question: can we freeze the outer array but keep inner linear?