5
$\begingroup$

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

enter image description here

enter image description here

$\endgroup$
  • $\begingroup$ is Listing 1 your own example, not from the paper? it would be helpful to analyze this complicated setup further in Computer Science Chat $\endgroup$ – vzn Oct 28 '15 at 21:25
  • $\begingroup$ Yes, that is my own example. The paper uses slightly different syntax. I'm thinking haskell/lambda calculus. $\endgroup$ – Christophe De Troyer Oct 28 '15 at 23:20
  • $\begingroup$ while apropos/ significant think this question could be entirely radically rewritten to be clearer, self-contained & more concise. think you should cite the key rules/ lines in question (only a few are relevant). and you use $\Gamma, \Sigma$ without defining them at all. the question uses the specialized syntax of the paper. one would have to parse a large part of the paper to figure out their syntax, but your question can probably described in a far simpler way. my general thinking on this though is that arbitrary uses of lambdas has to be restricted in any strong typing system. $\endgroup$ – vzn Oct 29 '15 at 0:31
4
+150
$\begingroup$

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.
$\endgroup$
  • $\begingroup$ It is indeed the case. I have had a discussion with the author via e-mail in the mean while as well. It makes no sense to retype what you just said in another answer. There is a different paper that addresses these issues titled "linear type theory for async session types". $\endgroup$ – Christophe De Troyer Nov 3 '15 at 16:04
  • $\begingroup$ wondering, are there any solutions that restrict use of lambdas? $\endgroup$ – vzn Nov 3 '15 at 17:11
  • $\begingroup$ @vzn: I don't know what "restrict use of lambdas" means in this context. The type discipline already "restricts the use" since you can only use it where the types match (e.g. where the calling context \Sigma matches the one expected by the function). $\endgroup$ – Stefan Nov 3 '15 at 23:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.