tweag
Pull array index isn't safe
I'm not sure Pull.Array.index is safe. For instance, I could take some non-dupable x :: a, put it into a singleton Pull Array, then linearly take its 0th element twice, giving me two copies of x and the array around, meaning I've duplicated x (with some spare).
Hi @b-mehta , happy to hear from you: it's been a while.
You're absolutely right, of course. Thanks for flagging it.
In the implementation, it's singleton which uses Unsafe.linear, maybe unwisely. I'd need to think about this library a bit more to remember why it's designed the way it is. Maybe just dropping index is the right solution, but converting linearly from and to Vector is also pretty heroic (I guess it doesn't matter much because Vector can't be consumed by linear functions).
I imagine that what I was going for was to view Vector a as a tuple of a-s, and as that Vector such distributes with Ur. In that case, index needs to go (not that it's a particularly useful function in the context of fusion pipelines anyway).
Hi! :) It has - but I kept notifications on for this repo and I thought I'd have a quick look at #470, then I noticed this!
I'm pretty sure singleton is actually safe, and the real problem is that the type of Pull.Array doesn't really reflect what it should do. And the library is designed (iirc) so that that fact shouldn't be exposed, but index breaks this.
The one save I can think of for index is for its second argument should be the array with the indexed element missing, which would restore safety. But this still isn't that useful...
I vaguely remember we (maybe separately) thought about improving the definition of PullArray to try and avoid some of the unsafety, it still seems interesting but difficult.