links-lang / links

Links: Linking Theory to Practice for the Web
http://www.links-lang.org
Other
318 stars 42 forks source link

Interaction between session-typed communication and effects is broken even without multi-shot continuations #1161

Closed thwfhk closed 1 year ago

thwfhk commented 1 year ago

As mentioned in #544 , handlers which use multi-shot continuations can duplicate a linear channel. However, it is still possible to break Links without multi-shot continuations by directly using the linear channel in the handler clauses. The reason seems to be that for handle M with H, the current type checking considers the usage of linear resources in M and H individually. The following program illustrates the problem:

fun deadlock() {
  var ch = fork(fun(ch) {
     var ch = send(42, ch);
     close(ch)
  });

  handle({
    # Nondeterministic choice.
    ignore(do Flip);
    var (i, ch) = receive(ch);
    println("Int: " ^^ intToString(i));
    close(ch)
  }) {
    case Return(_) -> ()
    case Flip(resume) -> {
      var (i, ch) = receive(ch);
      println("Int: " ^^ intToString(i));
      close(ch);
      resume(true)
    }
  }
}

I think for deep handlers, we should disallow the usage of linear resources in handler clauses. And for shallow handlers, we should split the linear resources context for M and H, and also use the same linear context for every clause in H (just like the typing rule for if or case statement).