Не понимайте типизацию продолжений Scala с разделителями (A @cpsParam [B, C])

Я пытаюсь понять, что именно это означает, когда значение имеет тип A @cpsParam[B,C] и какие типы этой формы я должен назначать своим значениям при использовании средства ограничений с разделителями.

Я посмотрел на некоторые источники:

http://lamp.epfl.ch/~rompf/continuations-icfp09.pdf

http://www.scala-lang.org/node/2096

http://dcsobral.blogspot.com/2009/07/delimited-continuations-explained-in.html

http://blog.richdougherty.com/2009/02/delimited-continuations-in-scala_24.html

но они не дали мне много интуиции в это. В последней ссылке автор пытается дать явное объяснение, но в любом случае это недостаточно ясно.

Здесь A представляет результат вычисления, который также является вкладом в его продолжение. B представляет тип возврата этого продолжения, а C представляет его "конечный" тип возврата, потому что сдвиг может выполнять дальнейшую обработку возвращаемого значения и изменять его тип.

Я не понимаю разницы между "выводом вычислений", "возвращаемым типом продолжения" и "окончательным типом возврата продолжения". Они звучат как синонимы.

Ответ 1

Итак, люди помогли мне с этим в другом месте. Вот ответ:

reset ({
    ...
    ...shift((k:A=>B) => ...::C)::A...
    ...
}::B)::C

Итак, shift является дырой типа A при вычислении {...} типа B. Аргумент shift возвращает значение типа C и поэтому reset ({...}) имеет тип C.

Основной трюк в понимании этого материала заключался в том, чтобы увидеть, что {...} и reset {...} имеют различный тип в зависимости от того, какой тип возвращает аргумент shift.

Например:

reset ({
    "number "+shift((k:Int=>String) => List(k(1), k(2), k(3)))
})

возвращает List("number 1", "number 2", "number 3").

Здесь A есть Int, B is String, C is List[String], потому что {"number" + _} есть (здесь) функция от Int до String и аргумент shift, учитывая, что функция производит a List[String], что становится результатом reset({...}).

Ответ 2

Я все еще в процессе выяснения точных правил/последствий ввода, которые здесь присутствуют.

Кажется легким/легким, если типы в примерах достаточно просты для того, чтобы "подходить хорошо", как показано выше, но это становится более интересным/трудным (по крайней мере для меня) при сравнении вещей с типизацией, предоставляемой tiark rompf:

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

поэтому результат [|e|].map( (x: A) => {[|r|]} ) будет иметь тип Shift[U,B,C] в соответствии с определением отображения, данным в работе tiark.

Здесь U не обязательно совпадает с B.

До сих пор я не понимаю, почему U разрешено отличаться от B без чего-то вроде U <: B, заданного в определении отображения в работе tiark.

Что я пропущу повторно, не понимая здесь?

Любые советы/идеи?