You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This document should track the introduction of two additional forms for new which matches the existence of sequencing. For instance !Int.?Int and [:!Int, !Bool:].
Currently new[...] imposes parallelism to the sub processes interacting with the new channel, this is out of place in the context of sequential computation.
The simplest form of sequential new would only take the type of the data exchanged on the channel, moreover a single channel name is introduced. For instance: new (c : Int) creates a sequential channel on which one can send and receive values of type Int. The only constraint on the use of c is to send/write before one receives/reads.
Consider a process such as new (c : A). P one simply infers the protocol for P at the channel c and checks that it matches a non-empty sequential repetition of !A.?A.
The second form of sequential new is taking two channels (maybe more) surrounded by [:...:], namely new[: c : S, c' : S' :]. The first session must be a source, namely only made of !A, {...}, [...] and [:...:]. The second session must have ?A instead of !A but arrays could be non dual.
This last condition is a bit subtle if S' is the dual of S then we have the guarantee that we can fuse the channel, this guarantee further extends when tensors meet ([!A,!B] vs [?A,?B]) since we can still fuse these. The only case we cannot fuse is when pars meet ({!A,!B} vs {?A,?B}) indeed the processing order is arbitrary on both sides so we really need this intermediate space. Since we want new to support fusion by default. To solve this we will require new to be annotated by alloc (Issue #24) when a par meets a par.
The text was updated successfully, but these errors were encountered:
This document should track the introduction of two additional forms for
new
which matches the existence of sequencing. For instance!Int.?Int
and[:!Int, !Bool:]
.Currently
new[...]
imposes parallelism to the sub processes interacting with the new channel, this is out of place in the context of sequential computation.The simplest form of sequential new would only take the type of the data exchanged on the channel, moreover a single channel name is introduced. For instance:
new (c : Int)
creates a sequential channel on which one can send and receive values of typeInt
. The only constraint on the use ofc
is to send/write before one receives/reads.Consider a process such as
new (c : A). P
one simply infers the protocol forP
at the channelc
and checks that it matches a non-empty sequential repetition of!A.?A
.The second form of sequential new is taking two channels (maybe more) surrounded by
[:...:]
, namelynew[: c : S, c' : S' :]
. The first session must be a source, namely only made of!A
,{...}
,[...]
and[:...:]
. The second session must have?A
instead of!A
but arrays could be non dual.This last condition is a bit subtle if
S'
is the dual ofS
then we have the guarantee that we can fuse the channel, this guarantee further extends when tensors meet ([!A,!B]
vs[?A,?B]
) since we can still fuse these. The only case we cannot fuse is when pars meet ({!A,!B}
vs{?A,?B}
) indeed the processing order is arbitrary on both sides so we really need this intermediate space. Since we wantnew
to support fusion by default. To solve this we will requirenew
to be annotated byalloc
(Issue #24) when a par meets a par.The text was updated successfully, but these errors were encountered: