Продолжения
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). Учебник, о котором я упоминаю, содержит очень удачно выбранные примеры, которые дают отличное ощущение продолжения с разделителями.