Multisided new

[np]

Tasks:

• Generalized dual checking
• Adapting the syntax
• Compilation to C
• Tutorial
• Tests

new with more than two sides. The point being that there can be many readers for one writer.

new [c : !Int, d : ?Int, e : ?Int]

One general criterion for this setting is:

new [c0 : S0, ..., ci : Si, ..., cn : Sn]
  ⊢ S0, ..., Sn dual

where

Γ is a list of type binding, x : A
Δ is a multiset of sessions

  ----------------------------------
  Γ ⊢ Δ dual

?(x : A). Δ means ?(x : A). S0, ..., ?(x : A). Sn given Δ = S0, ..., Sn

Δ.n means the nth component of Δ

One sender many receivers

Γ, x : A ⊢ S, Δ dual
---------------------------------
Γ ⊢ !(x : A). S, ?(x : A). Δ dual

One par, many tensors

Γ ⊢ Δ.0, φ0.0, φn.0 dual
...
Γ ⊢ Δ.m, φ0.m, φn.m dual
length Δ = length φ0 = length φ1 = ... = m
------------------------------------------------
Γ ⊢ {Δ}, [ψ0], ..., [ψn] dual

[np]

For instance the following process:

com_with_log =
 \(S : Session)
  (p : <      S >)
  (q : <     ~S >)
  (s : < ~Log S >)->
  proc() 
  new[c : S,      c' : ~S]
  new[d : ~S,     d' : S]
  new[l : ~Log S, l' : Log S]
  ( @p(c) 
  | @q(d)
  | @s(l)
  | fwd S (d',c',l'))

Could be written as:

com_new3 =
 \(S : Session)
  (p : < S  >)
  (q : < ~S >)
  (s : < ~Log S >)->
  proc()     
  new[c : S, d : ~S, l : ~Log S]
  ( @p(c)
  | @q(d)
  | @s(l))

[np]

While the interesting part of this proposal is for new with more than 2 channels, for the sake of generality and consistency (with forwarders) thorough the language new with zero or only one channel should be accepted as well.

When no channels are given, new[] does nothing.

When a single channel is given, the session must be only made of sends !(x : A). Therefore given any session S, Log S would qualify. Log permits par {...} and seq [:...:] but tensor sessions [...] should be allowed too.

Here is an example:

proc()
new[c : [!Int,{!Int,[:!Int,!Int:]}]]
c[i0,{i1,[:i2,i3:]}]
( send i0 0
| send i2 2.
  send i1 1.
  send i3 3)

Raising a warning for this use of new is probably a good thing as this kind of code is useless. Fusion will reveal that by making this code disappear.

[np]

Another example would be the following:

new[d : !A.?B.?C, e : ?A.!B.?C, f : ?A.?B.!C]
( send d a. recv d (y : B). recv d (z : C)
| recv e (x : A). send e (fb x). recv e (z : C)
| recv f (x : A). recv f (y : B). send f (fc x y))

The same kind of example would work with dependent sessions as well.