Type of `get` in `Data.Vector.Mutable.Linear`

Learn
1

I am noticing that the type of the function get here is

get :: HasCallStack => Int -> Vector a %1 -> (Ur a, Vector a)

This seems to suggest that the vector is ‘consumed’ when an element is accessed. Thus, one cannot successively use multiple gets on the same vector.

Why is this the case, even though this is only a read operation?

2

You get the vector back, in the second element of the tuple.

1 Like
3

Yes, I see that. But I am curious why the vector had to be consumed at all?

Why not just:

get :: HasCallStack => Int -> Vector a -> a
4

Oh, I see.

That’s because for something like

open :: Text -> File %1
write :: File %1 -> Text -> ()
close :: File %0 -- "invalidate" the file handle

file = open PATH
write file "Hi!"
close file
write file -- <- this should be an error

the compiler must know that file “is invalid” after close.

5

Let’s say you have a function that modifies the vector in some way:

f :: Vector a %1 -> Vector a

Now say you want to write a function that gets an element of the vector and then applies f. How would you do that? With the “consuming” version you can write it like this:

foo :: Int -> Vector a %1 -> (Ur a, Vector a)
foo i v = get i v & \(Ur x, v') -> (Ur x, f v')

But there is no way to write this function with your “non-consuming” get.

Also, you can implement your “non-consuming” get in terms of the current “consuming” get:

get' :: Int -> Vector a -> a
get' i v = get i v & \(Ur x, v) -> freeze v & \(Ur _) -> x
6

Not with a “sensible” implementation of linearity, as your lambda uses v' two times in the constructor of the tuple.

v' -> (get i v', set i v' 1)
-- is the same as
v' -> Tuple (f v', g v')
-- which must be an error
1 Like
7

The answers in the thread already get at the heart of the issue. Here are a few other ways to say the same thing.

  • One invariant of the Vector API here, is that a variable xs :: Vector a is always linear. Therefore, if you have a function get :: Int -> Vector a -> a it could never be called, since it requires a non-linear vector, and there is no such thing.
  • Writes must invalidate reads, otherwise you could do read 57 xs `seq` write 57 xs 42 `seq` read 57 xs. By definition of purity both read 57 xs should be the same result. But we’ve modified the array in between the two calls. This means that the type of read must be restricted. In this API, the only way is by requiring that everything be passed linearly.

A big part of the objective of linear constraints is to alleviate the burden on this sort of expression. That being said, with just linear types, I don’t think there’s a way to avoid sequencing reads (it’s just that instead of passing arrays you pass permissions, but the basic restriction is the same).

6 Likes