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 close on the channel we have stored that operation inside a lambda. We will play typechecker one more.
The first part of the typechecking is the same as above. So we have arrived at typechecking the body of the second let, namely let f =.... At this point $\Sigma = c \rightarrow\ !Int.End$ and $\Gamma = x \rightarrow [!Int.End] , v \rightarrow Chan \ c$.
The body of the lambda uses a channel that is defined outside of the lambda, namely $v$. According to the paper, the required $\Sigma$ should be embedded in the type signature of the lambda. However, this is where things get unclear. If I follow the typing rules I would have written down the lambda as $(Lambda\ [c \rightarrow End,\ x:Int]\ .\ (close\ v))$. But this is impossible, I think.
Recall that the rule C-Accept uses $fresh$ to "generate" a symbol that will be the identifier in $\Sigma$ and the second part of the type of the channel (e.g., $Chan\ c$). This means that it is impossible for the programmer to write down this identifier. Unless, of course, the channel is the parameter of the lambda itself. Then we can use $\alpha$-renaming. But this is not the case here, the channel is simply captured by the lambda and the parameter is $x$ which is ignored in the body of the lambda.
So, there are two options the way I see it. The text in Listing 2 is illegal for the reason that you can not capture a channel that has not been passed to the lambda as a parameter. However, the paper shows an example of this at page 9. So this reasoning is probably faulty.
The second reasoning I can come up with is the following. At the time the lambda is typechecked (as the binding to $f$), the typechecker will error because we are calling close on a channel that has session type $!Int.End$ in $\Sigma$. But, this could then be resolved by delaying the typechecking of the lambda until the point that it is invoked. But then, this does not require the programmer to write down the $\Sigma$ in the type signature of the lambda.
I hope the problem I have sketched here is clear. Any feedback is appreciated.
[1] Paper discussed in this question
