search

tweag / linear-base

Standard library for linear types in Haskell.
MIT License
335 stars 37 forks source link

A way to enforce uniqueness in typeclass instances #183

Open utdemir opened 4 years ago

utdemir commented 4 years ago

Most linear data structures require a way to enforce and maintain their uniqueness. And we have a few different ways to satisfy this requirement (see #130). However, some typeclass functions does not provide a way to enforce this property, so we can not implement them neatly as we'd like to.

Below is an example (originally posted at https://github.com/tweag/linear-base/issues/130#issuecomment-689509565)

Most operations on linear mutable vectors rely on the vector being unique, so the usual way to create a vector is to take a linear callback (alloc :: ... -> (Vector a #-> Unrestricted b) #-> Unrestricted b).

Today, I was implementing the Monoid instance for linear mutable vectors. Implementing mappend went well, since we already get two vectors, we can create a new one using the fact that we have access to some unique values.

However, I had a problem when implementing mempty :: a, because it doesn't provide a way to create a unique value. With the suggestion on #130 , we could have something like mempty :: Source #-> a instead. Otherwise, I need something like mempty :: forall b. (a #-> Unrestricted b) #-> b which is not pretty. Or we somehow have to accept that linear mutable vectors (at least with the current representation) are not monoids.

aspiwack commented 4 years ago

You can't really change the Monoid type class: it has the correct definition. And, yes, it does imply that Ur mempty :: Ur a is well typed. For all monoids. It's the case in any model of linear logic.

However, let me submit a thought for this particular case: it may be fine for the empty vector to be unrestricted. After all, there is just one of them. And it can't be mutated (as long as it is truly the vector based on the empty array). We have to be a bit careful there. But maybe it's not a problem.

PS: we could have a variant of Monoid, which would be a monoid in the (linear) Reader Source Kleisli category. But I'm not sure that it's worth it. Not yet, anyway.

utdemir commented 4 years ago

... it may be fine for the empty vector to be unrestricted. After all, there is just one of them. And it can't be mutated ... . We have to be a bit careful there.

I think you are right. Using the fact that there is an empty mutable array inside, and there's nothing to modify, and the only way to resize it is to copy it; an empty vector can be Ur. But, it feels a bit shaky, to be honest. I was more comfortable with the invariant that "all Vector's are unique".

I haven't thought this through, so likely I'm mistaken, but here's a thought. The same logic also applies to Array's too (they have a very similar representation with Vector's). But then, they also have a function like:

-- | Allocate a constant array given a size and an initial value,
-- using another array as a uniqueness proof.
allocBeside :: Int -> a -> Array b #-> (Array b, Array a)

That makes me uneasy. Combined with a mempty :: Array a, it feels like now we have a way to get any array as Unrestricted. This might be incorrect, so I am happy if you think this is fine.

aspiwack commented 4 years ago

That makes me uneasy. Combined with a mempty :: Array a, it feels like now we have a way to get any array as Unrestricted. This might be incorrect, so I am happy if you think this is fine.

This is a good point. So probably we simply don't want Vector to be a monoid. Is it a serious limitation?

utdemir commented 4 years ago

Technically, Vector's don't have a allocBeside function, also not have Vector a #-> Array a. So specifically in the Vector case, we might be safe. But having to choose between the allocBeside function and a Monoid instance is strange.

Is it a serious limitation?

No. I just thought it was interesting, since I'd expect Vector's to be monoids; I was just surprised when I couldn't do that. If you think this is not an issue that needs to be addressed somehow, I'm happy to close this issue.

sjoerdvisscher commented 4 years ago

Can somebody explain allocBeside to me? Having an unrestricted empty Array makes sense to me, so if that means that with allocBeside you can get any Array as Unrestricted could that not mean that the issue is with allocBeside?

facundominguez commented 4 years ago

Some discussion of it here: https://github.com/tweag/linear-base/pull/152#discussion_r482977454. allocBeside could be fixed by #130.

and the only way to resize it is to copy it; an empty vector can be Ur.

I don't understand. Wouldn't push empty a be an unrestricted non-empty vector?

aspiwack commented 4 years ago

I don't understand. Wouldn't push empty a be an unrestricted non-empty vector?

You are absolutely right. An unrestricted empty vector would be no good. In a way, it's reassuring: it means we don't have this weird tension between two features.