Scalaの区切り継続のタイピングを理解しないでください（@cpsparam [b、c]）

Question

私は値がタイプのときに正確に何を意味するのかを理解するのに苦労しています 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-explainedin.html

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

しかし、彼らは私にこれにあまり直感を与えませんでした。最後のリンクでは、著者は明示的な説明をしようとしますが、とにかく十分に明確ではありません。

ここでのAは、計算の出力を表します。これは、その継続への入力でもあります。 Bはその継続のリターンタイプを表し、Cはその「最終」のリターンタイプを表します。シフトは返された値にさらに処理し、そのタイプを変更する可能性があるためです。

「計算の出力」、「継続のリターンタイプ」、「継続の最終的なリターンタイプ」の違いはわかりません。彼らは同義語のように聞こえます。

Answer 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 は String, C は List[String] なぜなら {"number" + _} （ここで）からの関数です Int に String との議論 shift, 、その関数を考えると、aを生成します List[String], 、の結果になります reset({...}).

Answer 2

私はまだここにある正確なタイピングルール/意味を把握しています。

上記のように、例のタイプが「うまくフィットするのに十分な単純」である場合、簡単/簡単に思えますが、Tiark Rompfによるタイピングと比較する際に、より感染/困難になります（少なくとも私にとっては）：

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

したがって、の結果 [|e|].map( (x: A) => {[|r|]} ) タイプがあります Shift[U,B,C] ティアークの論文で与えられたマップの定義によると。

ここであなたは必ずしもBと同じではありません

これまでのところ、私はあなたがbと違うことを許される理由を理解していませんU <: B Tiarkの論文のMAPの定義に記載されています。

ここで理解できないことを表現しているのは何ですか？

ヒント/アイデアはありますか？