Annotations on channel allocation

[np]

One has yet to design the level of control on the channel allocation.

This reminds me of C qualifiers such as static or volatile. Notice how these qualifiers are independent from the type. All what can be made an annotation will improves modularity since it does not affect the type.

First, a list of applications of such a mechanism:

• Naive: the channel is allocated, in memory. This is what happens so far with the C backend since new is translated as a variable allocation.
• Fused: we apply fusion (which corresponds to a single cut-elimination), this makes the channel allocation goes away.
• More precisely the fusion can be recursive or not. For instance, without recursion, eliminating an array (or tuple) still creates one sub-channel for each cell. Similarly for continued sessions (e.g. !Int. ?Bool). It is not clear what is the benefit of non-recursive fusion, apart from debugging.
• If one chose to keep the allocation, one might want to chose the kind of storage. This is ideal to enforce precise control on where storing data: registers, cache, RAM, disk...
• Different layouts could be possible either for performance reasons (various ways to implement nested arrays) or compatibility reasons (mimicking other languages calling convention and array/struct layouts)
• Potential applications might be found in security akin to what has been done in the field of information-flow security.
• Finally, if these annotations are to be used a lot, they should not cause useless code duplication. Therefore they should be first-class: be represented as terms and have a type. Then we can write high-level code and specialize afterward.

The first practical question is of the syntax of these annotations. For instance:

new/fused (c : !Int, d)

The / indicate the annotation. We could then have a signature in the prelude:

fused : Allocation
fuse : (depth : Int) -> Allocation
alloc : Allocation
auto : Allocation

To fuse only one level we could write:

new/fuse 1 (c : !Int. ?Bool, d)

Which would fuse the Int but allocate the Bool.

The default allocation behavior for new should remain unspecified and could be called auto.