Iter constructs

[laumann]

This adds iteration constructs to the session type "DSL". Specifically three new structs are added with matching dual implementations (phantom data markers omitted):

struct IterOut<R, N>;
struct IterIn<R, N>;
struct IterEps;

impl<R: HasDual, N: HasDual> HasDual for IterOut<R, N> {
    type Dual = IterIn<R::Dual, N::Dual>;
}

with a mirror implementation for IterIn. IterEps is its own dual.

The idea is that R may be repeated zero or more times, where the party with the IterOut construct decides whether to iterate or not (better names for the structs are welcome).

IterOut allows two functions:

impl<E, R, N> Chan<E, IterOut<R, N>> {
    pub fn in_while(self) -> Chan<(IterOut<R, N>, E), R> { ... }
    pub fn exit_while(self) -> Chan<E, N> { ... }
}

where the implementation communicates the decision to the other party (as a boolean). IterIn then obtains the decision to iterate or not and must act accordingly.

impl<E, R, N> Chan<E, IterIn<R, N>> {
    pub fn out_while(self) -> Result<Chan<(IterIn<R, N>, E), R>, Chan<E, N>> { ... }
}

The inner body of the recursive construct (denoted R above) must indicate its end using IterEps.

impl<E, R> Chan<(R, E), IterEps> {
    pub fn iter(self) -> Chan<E, R> { ... }
}

---

Semantically, the iteration constructs are equivalent to a Rec<Choose<P, R>> construct, but where the Rec struct lacks a notion of a "next" action, the iteration construct provides this as the second type parameter (N above).

Note that there is no gain in expressivity! Any program using Rec<Choose<P, R>> can be rewritten to use IterIn/IterOut (but not the reverse - see the discussion below), but the lack of sequencing in Rec may be jarring to some users. I would suggest that we only provide one of these constructs though!

EDIT: Update based on discussion below

[laumann]

See the examples/ticket_ordering.rs for an example of using these iteration constructs.

[Munksgaard]

I don't feel like we should merge this. It's added complexity for no clear reason. There's lack of sequencing in Rec, yes, but it doesn't have any effect on the expressiveness of the language, as you said. For example:

IterIn<Send<u8, IterEps>,
    Recv<u8, Eps>>

is exactly equivalent to

Rec<Offer<Send<u8, Var<Z>>,
    Recv<u8, Eps>>

The only benefit being that it is clear, simply from the name of the construct, that the once we enter second branch of IterIn we cannot go back to the first. However, the same is equally true in the Rec<Offer case, as there is no Var<Z> inside that branch, it's just not immediately apparent from the name of the first construct.

It's also true that after having entered the second branch of IterIn, we no longer need to keep the whole construct on the stack, but that doesn't make much of a difference, since having entered the second branch of the Rec<Offer, we'd ignore the stack anyway, and use generics in real code. Thus, the full types become: Chan<E, Recv<u8, Eps>> in both cases.

Additionally, IterEps only allows one to iterate back a single level, while Var allows one to go up one or more levels on the stack.

[Munksgaard]

That said, I think it's a worthwhile experience to have had. We've explored this path, and so far it hasn't turned out to provide us with much added power of expression.

[kfl]

Just to make sure that we agree.

What you are arguing are:

1. All types written with IterIn/IterOut can be (mechanically) (re-)written using Rec. (I find that easy to believe.)

2. All types written with Rec can be (mechanically) (re-)written using IterIn/IterOut.

   This is more surprising, thus I'd like to see some argument for that. And I'm not sure I can follow Philip's argument.

[laumann]

What I meant to express was: Any protocol written using Rec can be rewritten using IterIn/IterOut to allow the same sequences of interactions - sends and receives discounting information exchange in choose()/offer() and in_while()/exit_while()

But any given Rec cannot in general be (mechanically) (re-)written. Specifically in Rec can enforce infinite recursion, which cannot be expressed in a finite type description using IterIn/IterOut. The simplest example is Rec<Var<Z>>. Attempting to rewrite it as an iterative construct would result in an infinite type: IterX<IterEps, IterX<IterEps, IterX<IterEps, ...>>> where IterX means either IterIn or IterOut.

This discussion seems to indicate that Recs are more expressive and IterIn/IterOut don't add anything but syntactical sugar.

EDIT: Add parenthesis EDIT: Strike-out the claim of some equivalence in expression of Rec and IterIn/IterOut (eating my own words). See the discussion below.

---

@Munksgaard In response to your earlier comment:

Additionally, IterEps only allows one to iterate back a single level, while Var allows one to go up one or more levels on the stack.

True, but it doesn't prevent nested loops. I'm not sure I see how this is a problem

[laumann]

@kfl Regarding @Munksgaard's argument I think he's referring to the types of the channels once iteration stops. For the IterIn case it will looks like this

Chan<(), Recv<u8, Eps>>

and for the Rec case the type will look like this:

Chan<(Offer<Send<u8, Var<Z>>, Recv<u8, Eps>>, ()), Recv<u8, Eps>>

Although the types are different, we can effectively ignore the stack, as the protocol in the second branch does not allow us to recurse.

IIRC rustc is even helpful here: if we wanted to pass the channel at this point to another function we could write:

fn finish_it<E>(c: Chan<E, Recv<u8, Eps>>) { ... }

and rustc would infer E as appropriate (we cannot do the same with the Recv<u8, Eps> part)

( @Munksgaard please correct me if I'm wrong)

[kfl]

What I'm trying to say is, that sometimes it is a feature to be less expressive. Meaning that Rec might be too general.

However, now I'm even more confused. Because it seems that Rec is not expressive enough, by the example you give.

The type:

Chan<(), Recv<u8, Eps>>

is (too me) rather different than:

Chan<(Offer<Send<u8, Var<Z>>, Recv<u8, Eps>>, ()), Recv<u8, Eps>>

The former allows a finite sequence of communications whereas the later allows infinite sequences of communications. It's like saying that the regular expression b*|a is just as good as the regular expression a because 'we can effectively ignore the stack, as the protocol regular expression in the second branch does not allow us to recurse iterate'.

[laumann]

What I meant to express was: Any protocol written using Rec can be rewritten using IterIn/IterOut to allow the same sequences of interactions - sends and receives discounting information exchange in choose()/offer() and in_while()/exit_while()

I have had some time to think and I don't agree with this statement anymore:

Rec<Send<u8, Var<Z>>> only allows an infinite sequence of of 'sends' which cannot be expressed in a (finite) iter construct. For example, IterOut<Send<u8, IterEps>, Eps> allows an infinite sequence of 'sends', but also allows any finite sequence.

---

@kfl Chan<(Offer<Send<u8, Var<Z>>, Recv<u8, Eps>>, ()), Recv<u8, Eps>> cannot recurse anymore - even though the stack contains the Offer there is no way to get it back (that requires a Var<Z>)

In terms of the regular expression b*|a, at the moment you decide to consume a, there is no way to go back and consume more bs. The types above reflect the type at that specific point in the protocol, when the choice has been made to choose a branch from which we cannot iterate/recurse (I hope this makes sense :confused:)

[laumann]

What I'm trying to say is, that sometimes it is a feature to be less expressive. Meaning that Rec might be too general.

Right, in particular the iter constructs only allow protocols that can terminate: If we leave out the Rec and Var from the session type DSL, the only terminating constructs (in that they don't have a "next" action) are IterEps and Eps. Even though we allow IterEps with the empty environment - Chan<(), IterEps> - it is not a useful nor "dangerous" channel type (well-typed programs can only drop the value - they cannot interact with the channel in any way). In other words, channel types that can actually be interacted with in well-typed programs must enclose IterEps in IterIn or IterOut, as they are the only constructs that can grow the stack. In case our protocol P does not contain any iter constructs its protocol must end in Epss. If P contains any iter constructs, we eventually must end with a protocol IterX<Q, R> where R is only terminated by Epss.

I'm trying to explain it to myself as I go along, so I apologise for any confusion...

[Munksgaard]

I'm closing this, as I think we've established that we don't want this for now.