Inferring dependent sends

[np]

If we look at the case for Send in Ling.Check.Core.checkAct we see that no dependent send is ever inferred. Here is a rough dump of ideas:

Plan-1:

Only support dependent sends when sending data-constructors:

send c d. P`

Let's call S the inferred session for c in P, call D the type of the data-constructor ``d`.

!(x : D). case x of { d -> S, ... }`

But we're stuck filling the other branches...

Plan0:

• Have a support for let (both expressions and actions)
• Internally restrict the Send action to variables only
• Externally, send c t is replaced by let x = t. send c x
• ¿¿¿How can we use this variable in the session???

Plan1:

• Extend the Send session to singletons: !(x = t : T). S
• We can then safely infer the session above
• In a way we push the issue onto a form of sub-typing for sessions:
  S <: S'[x := t] ==> !(x = t : T). S <: !(x : T). S'
• This would capture:

    S <: S' ==> !(x = t : T). S <: !T. S'
    S <: S' ==> !(x = `c : T). S <: !(x : T). case x of { `c -> S', ... }

Plan2:

• Change the syntax of send to be more explicit about dependencies, something similar to the infamous match ... in ... return ... with
• In way we want to know the return session abstracted over what we sent: (x : T) -> Session
• To continue checking the actions independently from the continuation process we could ask for a session transform such as: (x : T)(S : Session)-> Session
• TO BE CONTINUED...

[np]

Unlike most of the mad ideas above. The commit 815244e basically implements Plan2 bullet 1.

Namely we can now put annotations on sends: c : !(x : A). S <- t.

This is verbose but complete. Some examples are sender.ll and oplus.ll.

An improvement could be to propagate session information [#33] such that we don't have to annotation a send if we happen to know what session the channel should have. This can both go really far and stay simple.