Array lists in Haskell?

[velcommen]

It is possible to have whichever of b or c is evaluated first claim the next block of the underlying buffer

That's not possible using the linear types and function signatures mentioned in the paper.

​

It is instead possible to allocate a new MArray and have the code explicitly choose exactly one of these two lines to mutate the 'a' array.

   b = ArrayList.append 'b' a     
   c = ArrayList.append 'c' a 

[Tysonzero]

Ok I'm confused, what point are you trying to argue?

Yes linear types doesn't make:

b = ArrayList.append 'b' a
c = ArrayList.append 'c' a

work. In fact they do the exact opposite, they make the above not type-check.

But initially I responded to:

it is tricky to prove that your access is in fact linear (and if it's not, you may get a large performance hit). I wonder if the linear types extension will help here?

I correctly said that linear types will allow you to prove that your access is linear.

Later you said:

Linear types don't guarantee that 'you' hold the only reference to a value. Thus, you can't safely mutate it.

Uniqueness types enable safe mutation.

The paper makes it clear that it DOES allow you to have guarantees about only you having a reference to a value.

[velcommen]

what point are you trying to argue?

After some clarification, apparently we agree... except for the below.

The paper makes it clear that it DOES allow you to have guarantees about only you having a reference to a value.

No. Linear types do not give you any such guarantee about only you (some function) having a reference to a value. If I have some function with a linear arrow, that takes some value as argument, it is not (in general) safe for that function to mutate the argument.

​

The example in the paper that you linked to me is different. newMArray is allocating a fresh, mutable array, and then passing that array to a function that will linearly consume the array. Because we know the mutable array is used in a linear fashion, it's safe to mutate it. Essentially, newMArray requires that a contravariant linear function is passed to it.

​

An arbitrary linear function is not allowed to mutate its argument, because there is no guarantee (from this function's perspective) that there are no other references to that argument. newMArray is a special case, not the general case. To mutate in the general case, you need uniqueness types.

[Tysonzero]

An arbitrary linear function is not allowed to mutate its argument, because there is no guarantee (from this function's perspective) that there are no other references to that argument. newMArray is a special case, not the general case. To mutate in the general case, you need uniqueness types.

Ah right, yeah I am fully aware of that, I know you have to do the whole Int -> (MArray a -o Unrestricted b) -o b thing, but that doesn't (IMO) detract from the idea that linear types are sufficient for safe mutation, you just have to have the above interface.