Capture tracking and primitive types

Language Design
1

Currently, Scala capture checking silently drops capture set from primitive types.

Example:

 import language.experimental.captureChecking                                                                                                 
  import caps.*   

  class Box(val value: String)

  val cap1: SharedCapability^ = ???                                                                                                            
   
  def extract[T](x: List[T]): T^{cap1} = ???                                                                                                   
                  
  // Box: capability is preserved
  def testBox(): Unit =
    val x = extract(List(Box("hello")))
    val y: Box = x              // error
                                                                                                                                               
  // String: capability is silently dropped
  def testString(): Unit =                                                                                                                     
    val x = extract(List("hello"))
    val y: String = x           // no error, but should be

On one side, it’s understandable when capturing tracking a ‘real value in closure’ than primitives shoule be excluded.

But we can have virtual properties that are usually described by phantom types.
An example is security analysis: are we receiving this string from trusted sources?
And analysis basically the same as capture tracking – we bind the property to the value (i.e. add property {is-untrusted/trusted}, depends from type of analysis, in the capture-set)

So, question - is it possible to define a marker trait for the Cap, which will not drop on primitive types?

2

I believe that this is because String (and also the primitive classes) is hardcoded in the compiler to be “pure”

3

If you want to model an untrusted string, then that would need a wrapper class (didnt try if opaque type could work)

4

I mean, think about the possibility of adding a special type of Cap. (PhantomCap ?), which can be used to track properties on primitives.

This will enable code like:

@failsWith[Int]
trait GreetService derives HttpService:
  @get("/greet/{name}")
  def greet(@path name: String ^ {untrusted} ): String

  @post("/greet/{name}")
  def setGreeting(@path name: String ^ {untrusted}, @body greeting ^ {untrusted}: String): Unit

And then in Endpoint:

     e.greet.handle: name =>
        val greeting = db.query(
            "select  text from greeting where name=${name}"). // error - name is untrusted
        Right(s"$greeting, $name")
1 Like
5

so to clean the string there is some sandbox API like def check(name: String^{untrusted}): String?

6

yes