Boxing and Unboxing

As we ob­served ear­lier, by de­fault func­tions and ca­pa­bilites are sec­ond class – they can­not be re­turned nor stored in mu­ta­ble cells and can only be passed as sec­ond-class pa­ra­me­ters to other func­tions. We can lift this re­stric­tion by box­ing these func­tions and ca­pa­bil­i­ties, reify­ing the set of cap­tured ca­pa­bilites from the binder to the type.

interface Greeter { def sayHello(): Unit }

def myGreeter() {
  try {
    // boxing a capability and storing it in a mutable variable
    var capturedGreeter = box greeter;

    // unboxing requires `greeter` to be in scope
    def user() { (unbox capturedGreeter).sayHello() }

    // automatic boxing of `user`, stored in a value binder
    val firstClassUser: () => Unit at {greeter} = user;

    // automatic unboxing of firstClassUser
    firstClassUser()
  } with greeter : Greeter {
    def sayHello() { println("Hello World!"); resume(()) }
  }
}

Here, we box greeter to store it in the mu­ta­ble cell capturedGreeter. Note that Sys­tem C sup­ports au­to­matic box­ing and un­box­ing, and we could have omit­ted box. We can also ex­plic­itly an­no­tate the ex­pected ca­pa­bil­ity set as box {greeter} greeter. In the func­tion user, we unbox the cap­tured first-class block and call sayHello. The fact that we unbox it is re­flected in the in­ferred ca­pa­bil­ity set an­no­tated on user.

Boxed val­ues act as nor­mal first-class val­ues in Sys­tem C until un­boxed. In par­tic­u­lar, they can be passed as val­ues to value-poly­mor­phic func­tions.

def invoke[T](v : T){f : (T) => Unit}: Unit { f(v) }

def indirectMyGreeter { greeter: Greeter }: Unit {
  val capturedGreeter = box greeter;
  invoke(capturedGreeter){ (f : Greeter at { greeter }) =>
    f.sayHello()
  }
}

Hov­er­ing over capturedGreeter shows how the cap­ture is re­flected in the type.

Rea­son­ing about Pu­rity

Boxes re­flect cap­ture of tracked vari­ables in their types. Let us as­sume the fol­low­ing func­tion in the stan­dard li­brary:

// def setTimeout(callback: () => Unit at {}, duration: Int): Unit

Its im­ple­men­ta­tion uses the FFI to JavaScript. Sys­tem C is im­ple­mented as a com­piler to JavaScript and re­quires a monadic run­time. The value passed to the JavaScript builtin window.setTimeout should not make use of any con­trol ef­fects or ef­fect han­dlers since it will be called later out­side of all pos­si­ble han­dlers. To ex­press this, we re­quire the call­back to be “pure” (i.e. () => Unit at {}).

We can still use the un­safe println func­tion, as il­lus­trated in the fol­low­ing ex­am­ple

setTimeout(box { () => println("Hello after 2 seconds!") }, 2000)