Формальное определение продолжений Scala - PullRequest
7 голосов
/ 13 января 2012

Есть несколько вопросов о том, что такое продолжение Scala ( здесь и здесь ).Но ответы только пытаются объяснить это.Итак, в этом вопросе я прошу формальное определение того, что представляют собой продолжения (разделенные Скалой).Мне не нужен пример (хотя это может помочь), и я прошу о простой и понятной, насколько это возможно, формализации, возможно, даже игнорируя типизацию, если это помогает.

Формализация должна охватывать синтаксис (не в грамматическом смысле, носкорее как f is a function and c is a foo) и семантика (что будет результатом вычисления).

Ответы [ 3 ]

3 голосов
/ 15 апреля 2013
Продолжения

Scala с разделителями , реализованные в плагине продолжения, представляют собой адаптацию операторов управления shift и reset , введенных Danvy и Filinski . См. Их Абстрактное управление и Представление контроля: исследование трансформации CPS документы с 1990 и 1992 года. В контексте типизированного языка, работа EPFL Команда расширяет работу Асаи . См. Статьи за 2007 год здесь .

Это должно быть много формализма! Я взглянул на них, и, к сожалению, они требуют беглости в записи лямбда-исчисления.

С другой стороны, я обнаружил следующее Программирование с помощью Shift и Reset учебник , и мне кажется, что у меня действительно был прорыв в понимании, когда я начал переводить примеры в Scala и когда я попал в раздел "2.6 Как извлечь продолжения с разделителями" .

Оператор reset разделяет часть программы. shift используется в месте, где присутствует значение (включая, возможно, Единицу). Вы можете думать об этом как о дыре. Давайте представим это с ◉.

Итак, давайте посмотрим на следующие выражения:

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

Что делает shift, это превращает программу внутри сброса в функцию, к которой вы можете получить доступ (этот процесс называется реификацией). В вышеприведенных случаях используются следующие функции:

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 является то, что само вычисление reified:

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
         }

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

С точки зрения типа, если функция k имеет тип (A => B), тогда shift имеет тип A@cpsParam[B,C]. Тип C определяется исключительно тем, что вы выбрали для возврата внутри shift. Выражение, возвращающее тип, помеченный cpsParam или cps, квалифицируется как примесный в документе EPFL. Это в отличие от выражения pure , которое не имеет cps-аннотированных типов.

Нечистые вычисления преобразуются в Shift[A, B, C] объекты (теперь они называются ControlContext[A, B, C] в стандартной библиотеке). Объекты Shift расширяют монаду продолжения. Их формальная реализация приведена в документе EPFL paper , раздел 3.1, стр. 4. Метод map объединяет чистые вычисления с объектом Shift. Метод flatMap объединяет нечистые вычисления с объектом Shift.

Плагин продолжения выполняет преобразование кода, следуя схеме, приведенной в разделе 3.4 документа EPLF . По сути, shift превращаются в Shift объектов. Чистые выражения, возникающие после объединения с картами, нечистые - с flatMaps (см. Больше правил на рисунке 4) Наконец, после того, как все было преобразовано до полного сброса, при проверке всех типов тип конечного объекта Shift после всех карт и flatMaps должен быть Shift[A, A, C]. Функция reset устанавливает значение Shift и вызывает функцию с тождественной функцией в качестве аргумента.

В заключение, я думаю, что документ EPLF содержит формальное описание того, что происходит (разделы 3.1 и 3.4 и рисунок 4). Учебник, о котором я упоминаю, содержит очень удачно выбранные примеры, которые дают отличное ощущение продолжения с разделителями.

3 голосов
/ 13 января 2012

Процитировать википедию :

продолжение с разделителем, составное продолжение или частичное продолжение - это «фрагмент» кадра продолжения, который был преобразован в функцию.

Синтаксис Scala для этого:

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

A кадр продолжения выше - это все, что будет выполнено после shift до конца блока, ограниченного reset.Это включает в себя вызов функции g, поскольку она будет вызываться только после оценки shift, плюс весь код в B.

Функция g не требуется- вместо этого можно вызывать метод или полностью игнорировать результат shift.Я просто показываю, что вызов shift возвращает значение, которое можно использовать.

Другими словами, этот кадр продолжения становится следующей функцией:

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

Иполное тело сброса становится таким:

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

Обратите внимание, что последний оператор в B должен иметь тип Y.Результат вычисления является результатом содержимого блока shift, как это было бы с этим переводом выше.

Если вы хотите большей точности, проверьте бумагу , которая описывает разделительпродолжения в Scala.Точные типы можно найти в документации API .

0 голосов
/ 23 сентября 2018

Продолжения позволяют вам захватывать код после смены (но внутри сброса) и применять его следующим образом:

  import scala.util.continuations._
  def main(args: Array[String]): Unit = {
    reset {
      shift { continue: (Int => Int) =>
        val result: Int = continue(continue(continue(7)))
        println("result: " + result) // result: 10
      } + 1
    }
  }

В этом случае код вне нашей смены (но внутри нашего сброса) равен +1, поэтому каждый раз, когда вы вызываете continue, применяется {_ + 1}. Таким образом, результат continue(continue(continue(7))) равен 7 + 1 + 1 + 1 или 10.

Вот еще пример кода, взятого из здесь :

  import scala.util.continuations._
  import java.util.{Timer,TimerTask}

  def main(args: Array[String]): Unit = {
    val timer = new Timer()
    type ContinuationInputType = Unit
    def sleep(delay: Int) = shift { continue: (ContinuationInputType => Unit) =>
      timer.schedule(new TimerTask {
        val nothing: ContinuationInputType = ()
        def run() = continue(nothing) // in a real program, we'd execute our continuation on a thread pool
      }, delay)
    }
    reset {
      println("look, Ma ...")
      sleep(1000)
      println(" no threads!")
    }
  }

В приведенном выше коде код, следующий за сменой, но внутри сброса, равен println(" no threads!"). Таким образом, если мы заменим это:

def run() = continue(nothing)

с этим:

def run() = continue(continue(continue(nothing)))

Мы получаем этот вывод:

look, Ma ...
 no threads!
 no threads!
 no threads!

вместо этого вывода:

look, Ma ...
 no threads!

Таким образом, наш код после этого изменения в основном эквивалентен:

  import java.util.{Timer,TimerTask}
  def main(args: Array[String]): Unit = {
    println("look, Ma ...")
    timer.schedule(new TimerTask {
      def run() = {
        println(" no threads!")
        println(" no threads!")
        println(" no threads!")
      }
    }, 1000)
  }

Вы можете поиграть с кодом здесь .

Обратите внимание, что весь код перед нашим вызовом continue выполняется только один раз, и весь код между окончанием нашей смены и концом нашего сброса выполняется столько раз, сколько вызывается continue. Если наше продолжение никогда не вызывается, то код между концом нашей смены и концом нашего сброса никогда не выполняется. Таким образом, продолжение в Scala - это лямбда, которая фиксирует весь код между концом смены и окончанием сброса этого сдвига.

Также обратите внимание, что если наше продолжение выполняется в пуле потоков, остальная часть кода (весь код между концом сдвига и концом сброса) выполняется в потоке, предоставленном нам этим пулом потоков. Таким образом, если наше продолжение будет выполняться в потоке # 1 пула потоков, println(" no threads!") будет выполняться в потоке # 1 пула потоков, а println("look, Ma ...") будет работать в основном потоке. Из-за этого функция продолжения может использоваться для реализации фасада поверх асинхронного ввода-вывода, чтобы он выглядел как блокирующий ввод-вывод.

...