Generalize new (allocation) even more...

[np]

So we have new [ c : S, d : ~S ], new [: c : Log S, ~Log S :], and other variations where the number of channels is not only 2. For now, let's omit this form: new (c : A) which would bring only confusion to the point here.

All of these variations have a syntax which is made to recall how channels have to be used: in parallel or in sequence.

Now let's consider the following new (cd : [ S, ~S ]) this is declaring a single channel but of a particular shape (here a tensor with dual sessions). Here is how we would use it:

new (cd : [ S, ~S ]).
split cd as [c,d].
(@P(c) | @Q(d))

Of course in most cases the other forms are more convenient to use, however this form is somewhat more unique and the goal could be to capture all the soup of variations using this one.

Now we need a technique similar to how the Log function can be use to generally capture a session only made of sends.

Possible directions:

• A predicate: New : Session -> Type
• A function: New : Session -> Session (which would need to find a simple way to target only valid «new» sessions types)