Pure values

[treeowl]

A special case of a movable value is one whose unrestricted version can be formed by forcing zero or more thunks in it. It would be really nice not to have to copy these sorts of values at all. I don't see a way to do that without some compiler support (or, of course, unsafe coercions, which are bad). If you ignore linearity for a moment, the way we'd do this for, say, Data.Map, would look something like this:

move Tip = Tip
move m@(Bin (s :: Int) x l r)
  | Ur s' <- move s
  , Ur x' <- move x
  , Ur l' <- move l
  , Ur l' <- move r
  = if ptrEq x' x && ptrEq l' l && ptrEq r' r
       then m
       else Bin s' x' l' r'

This avoids a deep copy when appropriate. Would it be worth trying to get some special GHC support for this sort of thing?

[aspiwack]

A good example of such pure value type is Int#, though in this case copy is indistinguishable, operationally, from copying. Maybe ByteArray# is an example where not copying matters more than just cosmetically.

I don't know how to handle such types. I had a whiteboard session scheduled with some of my friends in Academia who may have solutions for this particular problem. This session was cancelled by the 2020 start of the pandemic. But maybe I'll be able to revisit it some time soon.

We could of course add this support in a shallow fashion by adding linear primitives to base moveInt# :: Int# %1 -> Ur# Int#, moveByteArray# :: ByteArray# %1 -> Ur# ByteArray# (whatever Ur# is). These primitives can be implemented as the identity function one way or another.

This would at the very least allow move @Int to be implemented without an unsafe coercion…

But these primitives are not there, and it would be better if the type system could recognise that such types need no moving (in a similar spirit as the Copy trait in Rust).

[treeowl]

For Int# and such, we would probably want moveIntRep# and so on. The actual primitives might well be quite unsafe, and that's fine—at that level it probably isn't possible to know reliably what's supposed to be restricted.

[treeowl]

For many/most primitive types, we likely want something more like forall (a :: TYPE IntRep). Coercible ((%m->) a) ((%m->) b).

[aspiwack]

Ah, re-reading, I see what you are hinting at. In a standard, linear-logic-like, implementation, move does a deep copy, but really, the copy is identical to the original version after forcing it deep enough.

So, instead of a copy, you would like to share the same representation (simply tying a bunch of deep-forcing to the forcing of Ur).

This is one of the ways in which call-by-need differs from call-by-name (where deep copy is, in contrast, absolutely essential). We could teach that to the compiler. I'm don't really know how to do this though.

For many/most primitive types, we likely want something more like forall (a :: TYPE IntRep). Coercible ((%m->) a) ((%m->) b).

On the other hand, I don't understand this comment.

[treeowl]

You don't understand the comment because i mangled it. I meant

forall (a :: TYPE IntRep) m n. Coercible ((%m->) a) ((%n->) a)

That is, a function taking something like an Int# at any multiplicity is equivalent to a function doing so at any other multiplicity. We shouldn't have to do anything, operationally, to change one into the other.

[aspiwack]

Understood. This is a perfectly reasonable characterisation, indeed. But we may also want it to “just hold”, like the compiler could understand that f, below, is correct.

f :: Int# %1 -> Int#
f x = x +# x

[treeowl]

@aspiwack, yes, we want such things to "just hold", but I think we also want to be able to do things like

flub :: IntMap (Int# m-> a) %1-> IntMap (Int# %n-> a)
flub = Data.Coerce.coerce

(Yes, the above code assumes that Data.Coerce.coerce will eventually have a linear or multiplicity-polymorphic type, but it really should. Writing coerce id gets pretty tiresome.)