Question about "Type checking a multithreaded functional language with session types" by Vasconcelos et al

I have been reading the paper[1] in the title. But there are some parts of it that are unclear to me, more specifically the way you typecheck a lambda. I have attached the typing rules below as images[2] [3] Typing them all in Mathjax would have been a lot of work.

I will explain the issue I am having by means of an example.

Given the program in listing 1, we first apply the rule C-Let. This means that we typecheck the first binding, namely new !Int.End which yields the type [!Int.End]. $\Gamma$ now contains a mapping $x \rightarrow [!Int.End]$. Then we typecheck the next let, using C-Let once more. This time we typecheck accept x, which first makes sure that $x$ is of the proper type. $\Gamma$ contains this mapping so that is indeed the case. This yields the type Chan c. Note that when you look at the typing rule for accept, $c$ in this case is a so-called "fresh" variable. The rule C-Accept also inserts the session type into $\Sigma$. So $\Sigma$ contains a mapping $c \rightarrow\ !Int.End$ and $\Gamma$ contains two mappings, namely $\Gamma = x \rightarrow [!Int.End] , v \rightarrow Chan \ c$

We then proceed to typecheck the last body of the most-inner let. The first statement is a send statement so we apply rule C-SendD. Typechecking the number $5$ yields type Int, so that part is correct. $v$ yields the type $Chan\ c$. $\Sigma$ indeed contains a mapping $c \rightarrow\ !Int.End$. So the rule C-SendD finally yields the type $\Sigma;Unit;c:End$ where the first part of the entry in $\Sigma$ has been consumed, leaving the session type for $c$ to $End$.

Finally we can apply the rule C-Close which also typechecks properly.

Listing 1

let x = new !Int.End in
let v = accept x in
  send 5 on v;
  close v;

We can now transform the above example to the following:

Listing 2

let x = new !Int.End in
let v = accept x in
let f = (Lambda x:Int . (close v))
  send 5 on v;
  (f 1);

Listing 2 shows that instead of just calling `cl

I think

(Lambda [c→End, x:Int] . (close v))

is indeed what you need to write. As you mention, it's "impossible" to write it because "c" is fresh. From my reading of it, it does seem to be a problem in the paper.

I don't think this is a very serious problem, tho, since the same problem appears in other systems and has known solutions (look at the papers about "Calculus of Capabilities" or "Alias Types", for example).

• if, as you do in your own syntax, you rely on type-inference, the problem disappears: the type inference can write the "c" since by that time it is known.

• you can change accept and request to return two things: a type c and a value of type Chan C. I.e. introduce "channel type parameters". Indeed Chan c is a singleton type, so you need c to be able to parameterize over c in order to be able to do anything useful.

StackExchange Computer Science Q#48701, answer score: 4