Scala継続の正式な定義

Question

Scalaの継続については、（hereとhere）についていくつか質問があります。しかし、答えはそれを説明しようとするだけです。だからこの質問では、（Scalaの）区切りの継続が何であるかの正式な定義を求めています。私は例を必要としませんが（それは助けになるかもしれませんが）、可能であれば簡略化された形式化として覚えておいてください。

形式化には構文（文法的な意味ではなく、f is a function and c is a foo）と意味（計算の結果となるもの）が含まれている必要があります。 wikipediaを引用する

Answer 1

スカラを継続プラグインで実装さ継続を区切りシフトとの適応がDanvyとFilinskiによって導入制御オペレータがリセットされます。その抄録コントロールと表す制御を参照してください：1990年と1992年からのCPS変換papersの研究を型付き言語の文脈では、EPFLチームの仕事はの仕事浅井を拡張します。 2007年の論文hereを参照してください。

これは形式が豊富でなければなりません。私はそれらを見て、残念ながらラムダ計算表記の流暢さが必要です。

は一方で、私は、Shiftキーと、次のプログラミングを発見し、tutorialをリセットし、私はスカラ座の例を翻訳するために始めたとき、私は本当に理解する上で画期的なを持っていたようにそれは感じていると私はセクション「2.6に着いたとき区切られた継続を抽出する方法 "。

resetオペレータは、プログラムの一部を区切ります。 shiftは、値が存在する場所（おそらくUnitを含む）で使用されます。あなたはそれを穴と考えることができます。それを◉で表現しよう。

それでは、次の式を見てみましょう：何shift

reset { 3 + ◉ - 1 }     // (1) 
reset {        // (2) 
    val s = if (◉) "hello" else "hi" 
    s + " world" 
} 
reset {        // (3) 
    val s = "x" + (◉: Int).toString 
    s.length 
} 

は、あなたが（このプロセスが具体化と呼ばれる）にアクセスできる機能にリセット内部のプログラムを有効にすることです。上記のケースでは、関数は、次のとおり

val f1 = (i: Int) => 3 + i - 1  // (1) 
val f2 = (b: Boolean) => { 
    val s = if (b) "hello" else "hi" // (2) 
    s + " world" 
} 
val f3 = (i: Int) => {    // (3) 
    val s = "x" + i.toString 
    s.length 
} 

機能が継続と呼ばれる、独自の引数の引数として提供されます。シフトシグネチャは：

shift[A, B, C](fun: ((A) => B) => C): A 

継続は（A => B）関数であると誰shift内部コードを書き込みすることと（または実行しない）何をすべきかを決定するであろう。あなたが本当にそれを返すだけで何ができるのかを感じ取ることができます。 resetの結果は、計算自体を具体化という、その後です：

val f1 = reset { 3 + shift{ (k:Int=>Int) => k } - 1 } 
val f2 = reset { 
      val s = 
      if (shift{(k:Boolean=>String) => k}) "hello" 
      else "hi" 
      s + " world" 
     } 
val f3 = reset { 
      val s = "x" + (shift{ (k:Int=>Int) => k}).toString 
      s.length 
     } 

私は具体化の局面は本当にScalaの区切り継続を理解することの重要な側面だと思います。

タイプの観点から、kタイプが（A => B）の場合、shiftはタイプA@cpsParam[B,C]です。 Cのタイプは、shiftの中に返却するものによって純粋に決定されます。 cpsParamまたはcpsで注釈された型を返す式は、impureとEPFL論文で修飾されています。これはの純粋な式とは対照的で、cps-annotatedタイプはありません。

不純な計算は、Shift[A, B, C]オブジェクト（現在は標準ライブラリのControlContext[A, B, C]と呼ばれています）に変換されます。 Shiftのオブジェクトは継続モナドを拡張しています。彼らの正式な実装は、EPFL paperのセクション3.1ページ4にあります。mapメソッドは、Shiftオブジェクトとの純粋な計算を組み合わせています。 flatMapメソッドは、不正な計算とShiftオブジェクトを組み合わせます。

継続プラグインは、EPLF paperのセクション3.4で与えられたアウトラインに従ってコード変換を実行します。基本的にshiftはShiftオブジェクトになります。後に出現する純粋な表現はマップと組み合わされ、純粋でない表現はフラットマップと組み合わされる（詳細は図4を参照）。最後にすべてが包囲リセットに変換されると、すべての型チェックですべてのマップとflatMapsの後の最終ShiftオブジェクトのタイプがShift[A, A, C]になるはずです。 reset関数は、含まれているShiftを再定義し、引数としてID関数を持つ関数を呼び出します。

結論として、私はEPLF論文には何が起こるかについての正式な記述が含まれていると思います（セクション3.1と3.4、図4）。私が言及しているチュートリアルには、区切られた継続のための素晴らしい感覚を与える非常によく選択された例があります。

Answer 2

：

限定継続、構成可能な継続または部分的な継続は、関数に具体化された 継続フレームの「スライス」です。このため

Scalaの構文は次のとおり

// Assuming g: X => anything 
reset { 
    A 
    g(shift { (f: (X) => Y) => /* code using function f */ }) 
    B 
} 

継続フレーム上resetで区切られたブロックの終わりまで後shiftを実行されるすべてです。これには、という関数を呼び出すことが含まれます。これは、shiftと評価されたの後にのみと呼び出され、さらにすべてのコードがBになります。

関数gは必須ではありません。代わりにメソッドを呼び出すか、shiftの結果を完全に無視することができます。 shift呼び出しが使用できる値を返すことを明確にすることを示します。言い換えれば

、その継続フレームには、以下の関数となる：

// Assuming g: X => anything 
def f: (X) => Y = { x => 
    g(x) 
    B 
} 

全体リセットボディはこのようになります。Bの最後の文はタイプYを持たなければならないこと

// Assuming g: X => anything 
A 
def f: (X) => Y = { x => 
    g(x) 
    B 
} 
/* code using function f */ 

注意。計算の結果は、上記の翻訳で起こるように、shiftブロックの内容の結果です。

さらに精度が必要な場合は、check the paperで、Scalaで区切られた継続を記述します。正確なタイプはAPI documentationにあります。