scala delimited continuations typing

Question

I am still in a process of figuring out the exact typing rules/implications involved in here.

It seems easy/easier if the types in the examples are "simple enough" to "fit well" as in almost all simple examples is the case, but it becomes more interresting/difficult (at least for me) in comparing things to the typing given by tiark rompf:

|- e: A@cpsParam[B,C]; {[|r|]}: U
-----------------------------------------------------
[|val x: A = e; r|] = [|e|].map( (x: A) => {[|r|]} )

so the result of [|e|].map( (x: A) => {[|r|]} ) will have the type Shift[U,B,C] according to the definition of map given in tiark's paper.

Here U is not necessarily the same as B.

So far I do not understand why U is allowed to be different from B without something like U <: B given in the definition of map in tiark's paper.

What am I missing respectively failing to understand here?

Any tips/ideas?

toni toni · Accepted Answer · 2010-11-23T19:08:48

I had a second look at this as wanted to see what the result of the selective cps transform will yield in both cases.

U <: B
U is not a subtype of B

I used the following simple example:

package sample

import scala.util.continuations._

class Depp {
  override def toString = "DEPP"
}

class Sepp extends Depp {
  override def toString = "DEPP->SEPP"
}

object Sample extends Application {
  val depp = new Depp
  val sepp = new Sepp
  val res = reset {
    shift {
      (k: Int => Depp) => k(7)
    }
    val z = sepp
    z
  }
  println("Result = "+ res)
}

Compiling this using

scalac -P:continuations:enable -Xprint:selectivecps Sample.scala

proves successful and yields the following (interesting part only):

private[this] val res: sample.Depp = scala.util.continuations.package.reset[sample.Sepp, sample.Depp]({
   package.this.shiftR[Int, sample.Depp, sample.Depp](((k: (Int) => sample.Depp) => k.apply(7))).map[sample.Sepp]
     tmp1;
     val z: sample.Sepp = Sample.this.sepp;
     z
   }))

ok so the type of the resulting (application of map) Shift object is [Sepp,Depp,Depp] as expected :)

which is fine because i understand how Shift objects like A@cpsParam[A,C] come into existence (the reset function given in Tiark's paper operates on such Shift objects)

Now changing the following in the simple example to yield a type unrelated to Depp: z.asInstanceOf[Float]

compiling this with

scalac -P:continuations:enable -Xprint:selectivecps -explaintypes Sample.scala

brings up the following error which tells what is actually checked:

Sample.scala:16: error: type mismatch;
 found   : Float @scala.util.continuations.cpsParam[sample.Depp,sample.Depp] @scala.util.continuations.cpsSynth
 required: Float @scala.util.continuations.cpsParam[Float,sample.Depp]
  val res = reset {
                  ^
Float @scala.util.continuations.cpsParam[sample.Depp,sample.Depp] @scala.util.continuations.cpsSynth <: Float @scala.util.continuations.cpsParam[Float,sample.Depp]?
  scala.util.continuations.cpsParam[sample.Depp,sample.Depp] <: scala.util.continuations.cpsParam[Float,sample.Depp]?
    Float <: sample.Depp?
      <notype> <: sample.Depp?
      false
    false
  false
false
one error found

ahh and here is the test: Float <: sample.Depp? so it fails because Float of course isn't a subtype of Depp

question: shouldn't the transformation rule then better be given as:

e: A@cpsParam[B,C]  {[|r|]}: U  U <: B
-----------------------------------------------------
[|val x: A = e; r|] = [|e|].map( (x: A) => {[|r|]} )

to clearly express this?

scala delimited continuations typing

1 Answers