Skip to content

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

Open
@bracevac

Description

@bracevac

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}

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions