np/ling

LINear LaNGuage: Type Theory and Process Calculi for Distributed and High-precision programming

Here are some instructions on how to use the ling tool chain.

Requirements

If you're new to Haskell your simplest option might be to install stack: http://docs.haskellstack.org/en/stable/README.html#how-to-install

Building

Once the repository is cloned, you can setup a local Haskell environment:

$ stack setup

Then to build the tool chain:

$ stack build

Finally you can run the compiler on a simple example:

$ stack exec -- ling --seq --fuse --pretty --compile fixtures/compile/double.ll

The command above is type checking, apply sequencing and fusion. It finally prints the final version in Ling and in C.

Contributions

Various contributions can be made whether you know Haskell or not.

Beside hacking on the tool chain, you can:

• Write small programs in the language
• Submit bug reports
• Join the discussion on the evolution of the language
• Help with the documentations and tutorials

Documentation

• Tutorial: https://ling.readthedocs.org/en/latest/tutorial/
• Talk: https://nicolaspouillard.fr/talks/ling-32c3/

ling's Issues

Syntactic support for grouped local definitions

Internally,

let x = e in
let y = f in
g

... is represented as:

let
  x = e
  y = f
in g

but we have no syntactic support for that.

Notice that the scoping rules are to be defined.

More flexible telescopes

Allow to write (x y z : A) instead of (x : A)(y : A)(z : A). This should work both for Πs and λs.

Local definitions: `let` bindings in terms and processes

A self-explanatory example:

let_example =
   let T = Int in
   let f = _+_ in
   proc(c : ?T.!T)
   recv c (x : T).
   let y = (f x x).
   send c y

A form with type annotation let x : T = t would be equivalent to let x = (t : T) using #18.

Alternative syntax with a classic memory read/write style

An example:

cmd_syntax_example =
  cmd(i : [?Int, ?Int], o : !Int)
     i[i0,i1]
     ( (x : Int) := @i0
     | (y : Int) := @i1).
     @o := (x + y)

Essentially recv c (x : A) becomes (x : A) := @c and send c t becomes @c := t.

So far the use of @ conflicts with its use to embed terms but so far I think it goes nicely with the idea of a location.

A more aggressive change would be to always write channels with a @ symbol. This could help making things more obvious at many levels but also look noisy and reminds of too many scripting languages...

Splitting/Grouping channels using patterns

The process language and type system was designed to keep the burden of where/when splitting tensors & pars really low.

Channel splitting

This means that channel splittings can be done early and freely ordered.
However we could directly name the sessions deeply and automate these splittings.

Example:

pattern_example = proc[ a : !Int, [: b : !Int, c : !Int :], { d : [!Int, !Int], e : {?Int, ?Int} } ]
   (send a 1 | send b 2. send c 3 | fwd [!Int,!Int] (d,e))

Which should desugar to:

pattern_example_expanded =
  proc(abcde : [!Int, [: !Int, !Int :], { [!Int, !Int], {?Int, ?Int} } ])
    abcde[a, bc, de]
    bc[: b, c :]
    de{d, e}
    (send a 1 | send b 2. send c 3 | fwd [!Int,!Int] (d,e))

Splitting patterns are not only for processes-as-terms but should be allowed for normal splitting as well:

pattern_example_2 = proc(abcde)
   abcde[ a : !Int, [: b, c :], { d, e } ]
   (send a 1 | send b 2. send c 3 | fwd [!Int,!Int] (d,e))

This example also recalls that session annotations are optional.

Patterns for grouping

[Grouping has been implemented in commit 72a3388]

When injecting a term as a process one must pass in some channels.
For instance consider we want to inject the term above in another process where the protocol is equivalent up-to some permutations.

-- notice how various parts gets commuted
test_pat =
  proc[ [: b : !Int, c : !Int :], a : !Int, { e : {?Int, ?Int}, d : [!Int, !Int] } ]
  @pattern_example[a, [: b, c :], {d, e}]

Alternatively with pattern splitting expanded:

test_pat_expanded_splitting =
  proc(bcaed : [[: !Int, !Int :], !Int, { {?Int, ?Int}, [!Int, !Int] } ])
    bcaed[bc, a, ed]
    bc[: b, c :]
    ed{e, d}
  @pattern_example_expanded[a, [: b, c :], {d, e}]

These grouping patterns can be expanded away as well. While we need to have this expansion in place eventually it is better to check the process un-expanded.

The expansion of grouping patterns for our example is:

test_pat_expanded_grouping =
  proc[ [: b : !Int, c : !Int :], a : !Int, { e : {?Int, ?Int}, d : [!Int, !Int] } ]
  new(f, g)
  ( @pattern_example(f)
  | g[a, [: b, c :], {d, e}])

So expansion of grouping patterns rely on the expansion of splitting patterns.

Syntax of Patterns

[also in commit 72a3388]

After the keyword proc we change `"(" ChanDecs ")", into TopPatt.

TPOld. TopPatt ::= "(" [Patt] ")" ;
TPPar. TopPatt ::= "{" [Patt] "}" ;
TPTen. TopPatt ::= "[" [Patt] "]" ;
TPOrd. TopPatt ::= "[:" [Patt] ":]" ;

PaVar. Patt ::= Name ":" Session ;
PaPar. Patt ::= "{" [Patt] "}" ;
PaTen. Patt ::= "[" [Patt] "]" ;
PaOrd. Patt ::= "[:" [Patt] ":]" ;

Implementation sketch

Implicit forwarding

The suggestion to be discussed here is the following.

Explicitly forwarding is a burden, we have to introduce twice as many names and then connect them. Combined with the current shortcoming of the lack of inference for forwarders we have to carefully pick the session and the correct order.

Consider the following function composing two processes of matching types:

comp1 =
  \(S0 S1 S2 : Session)
   (p0 : < S0 -o S1 >)
   (p1 : < S1 -o S2 >)->
   proc(c : S0 -o S2)
     c{ni0,i2}
     new [i : S0 -o S1, ni]
     new [j : S1 -o S2, nj]
     ni[i0,ni1]
     nj[i1,ni2]
     ( @p0(i)
     | @p1(j)
     | fwd(S0)(i0,ni0)
     | fwd(S1)(i1,ni1)
     | fwd(S2)(i2,ni2))

I'm suggesting something along the lines of:

comp1 =
  \(S0 S1 S2 : Session)
   (p0 : < S0 -o S1 >)
   (p1 : < S1 -o S2 >)->
   proc(c : S0 -o S2)
     c{~i0,i2}
     new [i : S0 -o S1, ni]
     new [j : S1 -o S2, nj]
     ni[i0,~i1]
     nj[i1,~i2]
     ( @p0(i)
     | @p1(j))

Here I've marked the channels to be connected with ~ as I'm concerned of the unintended use of this feature. Still we can consider the fully implicit version.

We don't have patterns inside allocated channels but this would help even further:

comp1 =
  \(S0 S1 S2 : Session)
   (p0 : < S0 -o S1 >)
   (p1 : < S1 -o S2 >)->
   proc(c : S0 -o S2)
     c{~i0,i2}
     new [i : S0 -o S1, [i0,~i1]]
     new [j : S1 -o S2, [i1,~i2]]
     ( @p0(i)
     | @p1(j))

It remains that we need to implement some basic inference first.

Any comments?

`new` floating and dependent types

This is a potential issue regarding the theory.

Typically the channel allocations/restriction, aka new in Ling, is allowed to commute upward (of course renaming channels to avoid conflicts).

Consider the following program:

recv c (i : Int)
new (v : ? Vec A i, v')
( .... | .... )

Here the new cannot float upward because of the type dependency.

At least this might force the types to be kept around in the compiler phases involving these floating rules.

Make `as i` be optional in `slice`

slice (c, ...) r should be expanded as slice (c, ...) r as _.

Allow ~ to be a valid channel name part

We could then write:

new (c, ~c)

Not only as a leading char since one might want to name ~a~b a channel of session {~A,~B}

Arbitrary sequencing of processes

Notice that this is implemented now. This remains a place holder for discussions around this topic.

Typically right-nested sequencing is preferable since we can clearly scope the newly introduced channels and variables.

However in several we break this rule, for instance fwd and @ can be sequenced and they might expand into a process which cannot be right-nested. Another cause is slice which has a sub-process and should have a sequential continuation. As in this example:

rotate_seq =
  \(A : Type)
   (n : Int)->
   proc(i : [: ?A ^(1 + n) :], o : [: !A ^(n + 1) :])
   i[:iL, iH^n:]
   o[:oL^n, oH:]
   recv iL (xL : A).
   (slice (iH, oL) n as _
      fwd(?A)(iH, oL)).
   send oH xL

Merge Fmt.hs and Ling.hs

This should reduce unnecessary recompilation and allow for more combinations of features.
The program ling-fmt could still exist as a tiny wrapper.

Propagate session type information downwards

Most constructs involving channels can have optional annotations.
Sometimes this information is only checked against the inferred information.
However annotations on send (#13) and recv could be inferred this way.

Annotations on channel allocation

One has yet to design the level of control on the channel allocation.

This reminds me of C qualifiers such as static or volatile. Notice how these qualifiers are independent from the type. All what can be made an annotation will improves modularity since it does not affect the type.

First, a list of applications of such a mechanism:

• Naive: the channel is allocated, in memory. This is what happens so far with the C backend since new is translated as a variable allocation.
• Fused: we apply fusion (which corresponds to a single cut-elimination), this makes the channel allocation goes away.
• More precisely the fusion can be recursive or not. For instance, without recursion, eliminating an array (or tuple) still creates one sub-channel for each cell. Similarly for continued sessions (e.g. !Int. ?Bool). It is not clear what is the benefit of non-recursive fusion, apart from debugging.
• If one chose to keep the allocation, one might want to chose the kind of storage. This is ideal to enforce precise control on where storing data: registers, cache, RAM, disk...
• Different layouts could be possible either for performance reasons (various ways to implement nested arrays) or compatibility reasons (mimicking other languages calling convention and array/struct layouts)
• Potential applications might be found in security akin to what has been done in the field of information-flow security.
• Finally, if these annotations are to be used a lot, they should not cause useless code duplication. Therefore they should be first-class: be represented as terms and have a type. Then we can write high-level code and specialize afterward.

The first practical question is of the syntax of these annotations. For instance:

new/fused (c : !Int, d)

The / indicate the annotation. We could then have a signature in the prelude:

fused : Allocation
fuse : (depth : Int) -> Allocation
alloc : Allocation
auto : Allocation

To fuse only one level we could write:

new/fuse 1 (c : !Int. ?Bool, d)

Which would fuse the Int but allocate the Bool.

The default allocation behavior for new should remain unspecified and could be called auto.

Multisided `new`

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

Translating λ-terms to processes...

This is an attempt at translating λ-terms to processes it does not work yet.
I'm welcoming your insights.

_° : Typ → Session
(A → B)° = A° -o B°
(A × B)° = [A°, B°]
Int°     = !Int

(_:_)° : (A : Typ) → (t : A) → < A° >
(t : A)° = proc (c : A°) (A, t, c)°

(_,_,_)° : (A : Typ) → (t : A) → c : A°
(A × B,t,c)° = c[c0,c1] ((A,fst t,c0)° | (B,snd t,c1)°)
(A → B,t,c)° = c{i,o} π(A,x,i). (B,t x,o)°
(Int  ,t,c)° = send c t

π(_,_,_) : (A : Typ) → (x : A)× i : ~A°
π(Int,  x,i) = recv i (x : Int)
π(B × C,x,i) = i{i0,i1} (π(B,x0,i0) | π(C,x1,i1)). let x = (x0,x1)
  -- Ok, we don't have `let` as a prefix yet...
π(B → C,x,i) = i[i0,o0] ... no clue ...
  -- A = B → C
  -- A° = {~B°, C°}
  -- ~A° = [B°, ~C°]
  -- i : ~A°
  -- i0 : B°
  -- o0 : ~C°

If terms are kept in normal form, constructs such as fst t,
snd t, and t x above can be reduced on the fly.

(Int → Int → Int, λx→ λy→ x+y, c)° =
  c{i0,io}
  recv i0 (x : Int).
  io{i1,o}
  recv i1 (y : Int).
  send o (x + y)

((Int × Int) → Int, λx→ fst x + snd x, c)° =
  c{i,o}
  i{i0,i1}
  ( recv i0 (x0 : Int)
  | recv i1 (x1 : Int) ).
  let x = (x0,x1)
  send o (fst x + snd x).

(Int → (Int × Int), (λx→(x,x)), c)° =
  c{i,o}
  recv i (x : Int).
  o[c0,c1]
  ( send c0 x
  | send c1 x)

(Int, (λx→ x) 1, c)° =
  send c ((λx→ x) 1)

π(Int → Int, x, i) =
  i[c0,c1]
  ( send c0 1
  | c1 <-> o)

((Int → Int) → Int, λf→ f 1, c)° =
  c{i,o}
  i[c0,c1]
  ( send c0 1
  | c1 <-> o)

(Int → (Int → Int) → Int, λx→ λf→ f x, c)° =
  c{i0,io}
  recv i0 (x : Int).
  io{i1,o}
  i1[c0,c1]
  ( send c0 x
  | c1 <-> o)

Use pretty-show instead of ghci-pretty

A backend targeting the Go language

So far Ling has a backend to C. However supporting multiple target language would be interesting.

Go seems like a good target language which would strike a balance between modern and efficient.
While Go has a GC, it is claimed that "Go gives the programmer considerable control over memory layout and allocation, much more than is typical in garbage-collected languages." which seems just about what we need.

The task would be to follow what has been done for C.

Here is a rough roadmap:

AST/Printer for Go

While there is a package on hackage it seems unmaintained and incomplete.
Moreover we do not need a something complete as we target a small subset anyway (at least at first).
So I would recommend writing down the grammar for the subset we are interested in using BNFC.

Ling.Compile.C

This module converts a sequentialized Ling program to C, what matters the most are the following parts:

• Ling terms gets translated to Go expressions (starting with function application and literals)
• Ling actions gets translated to Go statments (starting with send/recv, then new, then split)
• Ling processes defined at top-level gets translated to Go functions (no return type, at first only basic sessions such ?Int and !Int)
• Ling sessions and types gets translated to Go types (atomic types such as Int and Double, then arrays of those)

Let's keep in mind that the processes are sequentialized at that point. So new(c:S,d) declares a variable l of a type translated from S and we now track c and d has being associated to l.
The command send c t assigns the result of the expression translated from t to the location associated to c. The command recv c (x : A) assigns the variable associated to c to a local variable derived from x.

Fusion

This issue is a stub to track the progress on fusion.

Syntactic sugar to combine processes

Consider a process p of type: < A > for some session A, to use it we need a channel following session A, a typical pattern is to allocate such a channel and consume its dual:

example = proc()
   new (c : A, d : ~A)
   ( @p(c)
   | PROC_USING_d )

Initial suggestion with terse syntax:

example = proc()
   @p(d : ~A)
   PROC_USING_d

Others suggestions are welcome

Extending the assertion language

One should be able to specify a context.

AEnv. Assertion ::= [VarsDec] "|-" Assertion ;

Dependent sessions

Two kinds of dependencies should be supported at first.

Simple dependencies: indexing

(this is supported since 5657a0a)

Example:

dep_fun_server =
  \(A : Type)
   (B : (x : A)-> Type)
   (f : (x : A)-> B x)->
   proc(c : ?(x : A). !B x)
   recv c (x : A).
   send c (f x)

Large-elimination over finite data types

Example:

case_fun_server =
  proc(c : ?(x : Bool). case x of { `true -> !String, `false -> {!String,!String} })
  recv c (x : Bool).
  case x of
    `true -> send c "Hello World!"
    `false ->
       c{d,e}
       send d "Hello".
       send e "World"

However since case is not part of process but of terms the example above is rejected, instead one can write:

case_fun_server =
  proc(c : ?(x : Bool). (case x of { `true -> !String, `false -> {!String,!String} }))
  recv c (x : Bool).
  @(case x of
    `true -> proc (c) send c "Hello World!"
    `false ->
       proc (c)
       c{d,e}
       send d "Hello".
       send e "World"
  )(c)

Which is rejected so far with the following message:

Expected a protocol type, not:
case x of {
  `false -> < {!String, !String}> ,
  `true -> < !String >
}

Here the fix seems straightforward the type above should be equivalent to:

< case x of { `false -> {!String, !String} , `true -> !String } >

Generalize new (allocation) even more...

So we have new [ c : S, d : ~S ], new [: c : Log S, ~Log S :], and other variations where the number of channels is not only 2. For now, let's omit this form: new (c : A) which would bring only confusion to the point here.

All of these variations have a syntax which is made to recall how channels have to be used: in parallel or in sequence.

Now let's consider the following new (cd : [ S, ~S ]) this is declaring a single channel but of a particular shape (here a tensor with dual sessions). Here is how we would use it:

new (cd : [ S, ~S ]).
split cd as [c,d].
(@P(c) | @Q(d))

Of course in most cases the other forms are more convenient to use, however this form is somewhat more unique and the goal could be to capture all the soup of variations using this one.

Now we need a technique similar to how the Log function can be use to generally capture a session only made of sends.

Possible directions:

• A predicate: New : Session -> Type
• A function: New : Session -> Session (which would need to find a simple way to target only valid «new» sessions types)

Sequential `new`

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.

Embed sessions in terms

Example:

Sorter = \(n : Int) -> ? Vec Int n. ! Vec Int n
Sorter' = \(n : Int) -> {? Vec Int n, ! Vec Int n}

Implementation try to add:

TSession. Term ::= Session ;

If this yield too many ambiguities revert to something like:

TSession. Term ::= "session" Session ;

Parallel prefixes

See https://github.com/np/ling/SEQUENCING.md for an explanation of the change

• Change internal representation (ef58a34)
• Accept parallel prefixes in concrete syntax (470933f)
• Check parallel prefixes (143302b)
• Write more tests (4b17f84)
• Enforce proper use of . for sequencing

Exponentials

Why exponentials?

I'd like to gather here examples of the use of exponentials in the context of Ling, my conclusion so far is that they do not address the need for client/server behavior. If you disagree let's be constructive and have some examples.

Exponentials Now

First since Ling can views processes as terms and send/recv terms it does support a form of exponention [citation needed about Contextual Modal Linear Logic]:

• ? S becomes ? < S > which means receiving a process following session S.
• ! S becomes ! < S > which means sending a process following session S.

Upon receiving a process you can decide to use as many times as you want which is the expected behavior.
Sending a process require this process to be replicable, this is the case since you first need to wrap it as a term with proc(c : S). Thus, while you can still use the processes received as terms, your (linear) context only contains c.

I don't see how this form of exponential adrresses the client/server behavior, in a way you get to first download the code and then run it. Moreover it does not gives you access to more resources than you had before.

One might however consider a more direct support for exponentials.

A deeper integration of exponentials

In order to best integrate exponentials, I propose to mark the channels with exponentials. In this proposal the mark is a leading * in the channel name to express the repetition effect. The focus is first on the why not connective (noted ? in linear logic but this would conflict with our use of ? for sessions to receive data). The why not connective is essentially a flexible/repeatble version of par (⅋).

Let's assume S a Session used as the basis, we then have *c : S (in Linear Logic we would have something like c : ?S).

I'm proposing a syntax which enrich the current par splitting, for instance:

*c{c0,c1,*c2,*c3}

means that *c is splitted in four parts, with the following session assignment:

c0 : S
c1 : S
*c2 : S
*c3 : S

Therefore c0 and c1 can be used right away and *c2 and *c3 can be split further.

Getting rid of an unneccessary * channel can be done with empty splitting *c2{} for instance.

This design is (seems) compatible with the inference done on the processes.

The standard treatment of exponentials would be the following: Upon splits check that all the sessions are equivalente and propagate upward such session. One caveat is that when the split is empty we have no information to start with. The workaround could be to ignore the sessions which are *ended.

What about *c[ ... ] or *c[: ... :], they could be accepted as well with their corresponding rules. This would be consistent since we have mix ([Γ] ⊸ {Γ}) and ([:Γ:] ⊸ {Γ}). Intuitively if you have the choice of the processing order ({Γ}) you can decide to restrict yourself to proccessing in parallel ([Γ]) or in-order ([:Γ:]).

However the dual side will not be able to take advantage of these additional restrictions and will have to process all the request independently.

Language Specification

Collecting here the different issues (potentially closed for now) about the design:

• Local definitions #17
• Annotations on channel allocations #24
• Sequential new #28
• Multi-sided new #4
• Parallel prefixes #

Use wl-pprint-extras to replace the pretty-printer

The current printer is a hack, as much as what BNFC produces to be fair.

We would replace the printer if the need for width sensitive printing become too important.

Options:

• Teach BNFC how to use a proper pretty-printer (would be the best)
• Keep most of the existing printer and somehow adapt the render function to use the API from wl-pprint-extras (the cheapest but not sure this works)
• Just write a proper printer

One might wait a little that the syntax stabilizes though.

First example in the tutorial doesn't compile

Dunno if this is the right place to file this issue, but anyway...

The tutorial opens with the following code example:

sum_int = proc(a : {?Int ^ 10}, r : !Int)
  new/alloc [itmp : !Int.?Int, tmp]
  ( send itmp 0.
    fwd(?Int)(itmp, r)
  | a{ai}
    slice (ai) 10 as i
      recv ai  (x : Int).
      recv tmp (y : Int).
      send tmp (x + y))

When I try to build this with a freshly cloned and built ling compiler it gives me an error:

While checking `sum_int`
  While checking `ai`
    Replication factors are not equivalent.
    Annotation:
      1
    Inferred:
      10

Internally forwarders should be terms

Internally we have At for term-as-a-process and Ax for forwarders (axioms). Ideally I think Ax should disappear and become At (Def fwdName ...).

• This would remove some redundant code
• This would allow to use fwd in terms directly instead of proc(cs...) fwd ... (cs...)
• Improvements made on term-as-a-process would benefit forwarders

Now we have two forms of forwarders:

• fwd <Nat> <Session> <Channel>
• fwd <Session> ( <Channel>* )

The first form can be given a general type:

fwd : (n : Int)(S : Session) -> < Fwd n S >

The second is using a flat sequence of sessions and we cannot express this type as only Session is exposed and not [RSession].

Therefor using the first form internally seems more appropriate.

The second form would then be a consequence of a more liberal form of term-as-a-process.

Note that so far what we have internally is the reverse the first form is a wrapper around the second.

Extensional `case` equivalence

Consider the following:

assert (x : Bool)-> (case x of { `true -> < ?Int > , `false -> < !Int > })
     = (x : Bool)-> < case x of { `true -> ?Int , `false -> !Int } >
     : Type

This is rejected so far but I wish we accept by checking that setting x to true andfalse leads to the resulting terms to be equivalent.

Inferring dependent sends

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...

Syntactic sugar to receive on channels within terms

<-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))

Arbitrary type annotation

Given a term t and a type A, (t : A) is a term which enforce that the type of t is A.