Implicit forwarding

[np]

The suggestion to be discussed here is the following.

Explicitly forwarding is a burden, we have to introduce twice as many names and then connect them. Combined with the current shortcoming of the lack of inference for forwarders we have to carefully pick the session and the correct order.

Consider the following function composing two processes of matching types:

comp1 =
  \(S0 S1 S2 : Session)
   (p0 : < S0 -o S1 >)
   (p1 : < S1 -o S2 >)->
   proc(c : S0 -o S2)
     c{ni0,i2}
     new [i : S0 -o S1, ni]
     new [j : S1 -o S2, nj]
     ni[i0,ni1]
     nj[i1,ni2]
     ( @p0(i)
     | @p1(j)
     | fwd(S0)(i0,ni0)
     | fwd(S1)(i1,ni1)
     | fwd(S2)(i2,ni2))

I'm suggesting something along the lines of:

comp1 =
  \(S0 S1 S2 : Session)
   (p0 : < S0 -o S1 >)
   (p1 : < S1 -o S2 >)->
   proc(c : S0 -o S2)
     c{~i0,i2}
     new [i : S0 -o S1, ni]
     new [j : S1 -o S2, nj]
     ni[i0,~i1]
     nj[i1,~i2]
     ( @p0(i)
     | @p1(j))

Here I've marked the channels to be connected with ~ as I'm concerned of the unintended use of this feature. Still we can consider the fully implicit version.

We don't have patterns inside allocated channels but this would help even further:

comp1 =
  \(S0 S1 S2 : Session)
   (p0 : < S0 -o S1 >)
   (p1 : < S1 -o S2 >)->
   proc(c : S0 -o S2)
     c{~i0,i2}
     new [i : S0 -o S1, [i0,~i1]]
     new [j : S1 -o S2, [i1,~i2]]
     ( @p0(i)
     | @p1(j))

It remains that we need to implement some basic inference first.

Any comments?