Formalna definicja kontynuacji Scala

Question

Istnieją pewne pytania dotyczące kontynuacji Scala (here i here). Ale odpowiedzi tylko próbują to wyjaśnić. W tym pytaniu proszę o formalną definicję kontynuacji (Scala's) wytyczonych w kontynuacji. Nie wymagam przykładu (choć może to pomóc) i proszę o prostą i zrozumiałą jak to tylko możliwe formalizację, może nawet ignorując pisanie, jeśli to pomaga.

Formalizacja powinna obejmować składnię (nie w sensie gramatycznym, ale raczej jak f is a function and c is a foo) i semantykę (jaki będzie wynik obliczeń).

Answer 1

Scala rozdzielany kontynuacje, realizowanej w ramach kontynuacji wtyczki są adaptacją przesunięcia i zresetować operatorów kontroli wprowadzonych przez Danvy i Filiński. Zobacz ich abstrahując sterowania i Reprezentowanie Sterowanie: studium transformacji CPSpapers od 1990 do 1992. W kontekście język maszynowy, praca z zespołem EPFL wydłuża pracę Asai. Zobacz artykuły 2007: here.

To powinno być dużo formalizmu! Spojrzałem na te i niestety wymagają one płynności w notacji rachunku lambda.

Z drugiej strony, znalazłem następujące Programowanie z Shift i Resettutorial i czuje się jak miałem naprawdę przełom w zrozumieniu, kiedy zacząłem tłumaczyć przykłady Scala i kiedy wróciłem do sekcji „2.6 Jak wyodrębnić rozdzielone kontynuacje ".

Operator reset ogranicza fragment programu. shift jest używany w miejscu, w którym występuje wartość (w tym prawdopodobnie w jednostce). Możesz myśleć o tym jak o dziurę. Przedstawmy to za pomocą ◉.

Więc spójrzmy na następujących wyrażeń:

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

Co shift robi to, aby włączyć program wewnątrz reset do funkcji, które można uzyskać dostęp (proces ten nazywany jest reifikacja). W powyższych przypadkach funkcje są następujące:

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 
} 

Funkcja nazywana jest kontynuacją i jest podawana jako argument do własnej argumentacji. Przesunięcie jest podpis:

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

Kontynuacja będzie (A => B) funkcja i kto pisze kod wewnątrz shift zdecyduje, co zrobić (lub nie robić) z nim. Naprawdę masz poczucie, co może zrobić, jeśli po prostu go zwrócisz. Wynik reset jest wtedy reified obliczeń sam:

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 
     } 

myślę aspekt reifikacja jest bardzo ważnym aspektem zrozumienia Scala rozdzielany kontynuacje.

Z perspektywy typu, jeśli funkcja k ma typ (A => B), wówczas shift ma typ A@cpsParam[B,C]. Typ C jest ściśle określony przez to, co wybrałeś, aby powrócić do wnętrza shift. Wyrażenie zwracające typ oznaczony cpsParam lub cps zostało zakwalifikowane jako zanieczyszczone w papierze EPFL. Jest to przeciwieństwo wyrażenia pure, które nie ma typów z adnotacjami cps.

Zanieczyszczone obliczenia są przekształcane w obiekty Shift[A, B, C] (obecnie nazywane ControlContext[A, B, C] w bibliotece standardowej). Obiekty Shift rozszerzają monadę kontynuacji. Ich formalne wdrożenie znajduje się w EPFL paper, sekcja 3.1 strona 4. Metoda map łączy czyste obliczenia z obiektem Shift. Metoda flatMap łączy nieczyste obliczenia z obiektem Shift.

Wtyczka kontynuacji wykonuje transformację kodu zgodnie z konturem podanym w sekcji 3.4 EPLF paper. Zasadniczo, shift są przekształcane w obiekty Shift. Czyste wyrażenia występujące po połączeniu są łączone z mapami, a nieczyste są łączone z płaskimi mapami (zobacz więcej reguł rysunek 4).Na koniec, gdy wszystko zostanie przekonwertowane do zamykającego resetu, jeśli wszystko zostanie sprawdzone, typ końcowego obiektu Shift po wszystkich mapach i płaskich mapach powinien być Shift[A, A, C]. Funkcja reset potwierdza zawarty Shift i wywołuje funkcję z funkcją tożsamości jako argumentem.

Podsumowując, uważam, że dokument EPLF zawiera formalny opis tego, co się dzieje (sekcja 3.1 i 3.4 oraz rysunek 4). Samouczek, o którym wspomniałem, zawiera bardzo dobrze dobrane przykłady, które dają wspaniałe odczucie dla wytyczonych ścieżek.

Answer 2

Aby podać wikipedia:

rozdzielanego uzupełniające, sk kontynuacji lub częściową kontynuację, jest „plaster” w jest ramka kontynuacja który został reified w funkcji.

Scala składnia to:

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

Ramka kontynuacja powyżej jest wszystko, co będzie realizowane poshift aż do końca bloku ograniczonej przez reset. Obejmuje to wywołanie funkcji g, ponieważ będzie ona wywoływana tylko jako po przy ocenie shift, plus cały kod w B.

Funkcja g nie jest wymagana - można zamiast tego wywołać metodę lub całkowicie zignorować wynik shift. Pokazuję to tylko po to, aby wyjaśnić, że wywołanie shift zwraca wartość, która może być użyta.

Innymi słowy, że rama kontynuacją będzie następująca funkcja:

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

I całe ciało odblokowanie staje się w ten sposób:

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

Należy zauważyć, że ostatnie oświadczenie w B musi mieć typ Y. Wynik obliczeń jest wynikiem zawartości bloku shift, tak jak w przypadku powyższego tłumaczenia.

Jeśli chcesz uzyskać większą precyzję, check the paper opisuje delimitowane kontynuacje w Scali. Dokładne typy można znaleźć na stronie API documentation.