Syntactic sugar to receive on channels within terms

[np]

<-c could be made a term (as in Go). For instance (<-c : A) would desugar to a receive action let x : A <- c.

Given some type inference the syntax <-c would work without type annotation.

More precisely given an action act all the occurrences (within the terms in act) of a <-c gets replaced by a fresh variable (say x_c). All the receive actions are then combined in parallel and occurs just before act.
All the channels on which we receive must then be distinct, which is enforced because of the parallel combination.

Example:

split de[d,e]
c <- (<-d : Int) + (<-e : Int)

Becomes:

split de[d,e]
(let (x_d : Int) <- d | let (x_e : Int) <- e).
c <- (x_d + x_e)

The biggest advantage of this syntax is that being shorter it pushes the programmer to write more parallel receives which leads to more convenient types.

Caveat

As mentioned in Issue #8, <-c within a local definition should have a specific syntax (using <= instead of =) to avoid suggesting that one can freely replace such definitions.

I suggest to forbid receive expression to be under additional binders. The worse would be that the type of the received message depends on such additional binder. Less critical but \(x : A)-> (recv c : B) would suggest that the receive is down when the function is called. For instance this would be rejected:

d <- (\(x : A)-> (<-c : B))

[np]

Updated the syntax.