Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CC: Improve inference of functions (Typing boundary/break) #22481

Open
bracevac opened this issue Jan 29, 2025 · 0 comments
Open

CC: Improve inference of functions (Typing boundary/break) #22481

bracevac opened this issue Jan 29, 2025 · 0 comments
Labels
area:experimental:cc Capture checking related cc-experiment Intended to be merged with cc-experiment branch on origin itype:bug

Comments

@bracevac
Copy link
Contributor

Compiler version

Latest nightly

Minimized code

With recent support for capture variables, abstract capture members and paths
in and to captures, we can obtain a reasonable signature for boundary/break
or similar delimiter pairs that prevent leaking inner labels,
using path-dependent types:

import language.experimental.captureChecking
import caps.*

trait BoundaryBreak:

  trait Label extends Capability:
    type Cap >: CapSet <: CapSet^

  def boundary[T,C^](block: Label{type Cap = C} ->{C^} T): T = ???
  def suspend[U](label: Label)(handler: () ->{label.Cap^} U): U = ???

  def test =
    val x = 1
    boundary: outer =>
      val y = 2
      boundary: inner =>
        val z = 3
        suspend(outer): () =>
          println(inner) // error , good!
          x + y + z

  trait File extends Capability:
    def write(s: String): Unit
    def read(): String

  def test2 =
    val f1: File = ???
    boundary: outer =>
      val f2: File = ???
      suspend(outer): () =>
        f1.write("ynot") // error, but should be legal

Output

In test2, we get an error:

-- Error: local/boundarybreak.scala:36:8 ---------------------------------------
36 |        f1.write("ynot")
   |        ^^
   |reference (f1 : BoundaryBreak.this.File^) is not included in the allowed capture set {outer.Cap^}
   |of an enclosing function literal with expected type () ->{outer.Cap^} Unit

but we can make it work by explicitly annotating the expected capture set of the body:

 def test3 =
    val f1: File = ???
    boundary[Unit,CapSet^{f1}]: outer =>
      val f2: File = ???
      suspend(outer): () =>
        f1.write("ynot") // accepted now!

Expectation

Ideally, inference of types/captures would correctly infer CapSet^{f1}

@bracevac bracevac added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label cc-experiment Intended to be merged with cc-experiment branch on origin area:experimental:cc Capture checking related and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Jan 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:experimental:cc Capture checking related cc-experiment Intended to be merged with cc-experiment branch on origin itype:bug
Projects
None yet
Development

No branches or pull requests

1 participant