Expose a polymorphic "copy" function

[rrnewton]

This would be a nice building block for any stop-gap manual memory management on the way to fully automated GC (e.g. #100). If we had type classes, it could have a qualified type that says you can only use it on Gibbon packed data:

copy :: GibPack a => a -> a

But actually, I think it's fine for it to have this simple type:

copy :: a -> a

In the L0 language, the meaning of copy on functions or unpacked types is just an identity function. Indeed, it is semantically the identity function for packed data too, but it has the operational effect of creating a fresh region.

Problems:

• If copy had a linear type, we could call free on the old data after immediately after copying. Without linearity, we're going to have a lot of trouble arranging for the old version to come to the end of its let-region scope and be destroyed.
• Furthermore, even if it did have a linear type, then we still need to know (or ensure during inference) that the target of the copy is in a "singleton region" (containing one root / one value) so that destroying the (root) object is equivalent to destroying the region.

Example:

server st = if _ then shutdownReturn else server (copy (update st))

Here, the non-linear copy won't help us, because x's region is still in scope until the server shuts down. (Does this touch on the polymorphic recursion issue that MLkit struggled with?)

Alternatives

copy could be called compact....

Depends on

• [#103]

[ckoparkar]

This would be a nice building block for any stop-gap manual memory management

+1

Until we have a notion of linearity in the compiler, perhaps we can run ghc/linear-types to typecheck linear_copy.

[rrnewton]

Oh, that was the ONLY notion of linearity I would ever propose to support (don't reimplement). We can have GHC/linear-types do the type check, and then gibbon can just "trust" that the linear annotations are correct.

[rrnewton]

Btw, you could use the same argument to argue that we don't really need to run type inference at all for L0, but I think it's good that you implemented it @ckoparkar, because (1) it's a good sanity check, and (2) we can probably give better error messages, especially if there's a problem/bug in monomorphization. That is, it passes GHC type checking but runs up against some limitation that means its not supported by Gibbon. Better to catch those as early in the compiler as possible.

[ckoparkar]

We now have the following polymorphic functions:

• copyPacked :: Packed a => a -> a
• travPacked :: Packed a => a -> ()
• printPacked :: Packed a => a -> ()