CPS на языке карри

Question

Как CPS в таких языках с карри, как лямбда-исчисление или Ocaml, имеет смысл? Технически все функции имеют один аргумент. Допустим, у нас есть версия дополнения CPS на одном из таких языков:

cps-add k n m = k ((+) n m)

И мы называем это как

(cps-add random-continuation 1 2)

Это то же самое, что и:

(((cps-add random-continuation) 1) 2)

Я уже вижу два вызова, которые не являются хвостовыми вызовами, и в действительности это сложное вложенное выражение, (cps-add random-continuation) возвращает значение, а именно функцию, которая использует число, а затем возвращает функцию, которая использует другое число, а затем доставляет сумму обоих к этому random-continuation. Но мы не можем обойти это возвращаемое значение, просто переведя его снова в CPS, потому что мы можем дать каждой функции только один аргумент. Нам нужно как минимум два, чтобы освободить место для продолжения и «фактического» аргумента.

Или я что-то упустил полностью?

Answer 1

Поскольку вы пометили это с помощью Haskell, я отвечу по этому поводу: в Haskell эквивалент преобразования CPS работает в монаде Cont, которая преобразует значение x в более высокое значение. Функция заказа, которая принимает один аргумент и применяет его к x.

Итак, для начала вот 1 + 2 в обычном Haskell: (1 + 2) А вот в монаде продолжения:

contAdd x y = do x' <- x
                 y' <- y
                 return $ x' + y'

... не очень информативно. Чтобы увидеть, что происходит, давайте разберем монаду. Сначала удалите запись do:

contAdd x y = x >>= (\x' -> y >>= (\y' -> return $ x' + y'))

Функция return выводит значение в монаду и в этом случае реализуется как \x k -> k x, или с использованием секции инфиксного оператора как \x -> ($ x).

contAdd x y = x >>= (\x' -> y >>= (\y' -> ($ x' + y')))

Оператор (>>=) (читай «связать») объединяет вычисления в монаде и в этом случае реализуется как \m f k -> m (\x -> f x k). Изменение функции связывания на префикс формы и подстановку в лямбду, а также некоторые переименования для ясности:

contAdd x y = (\m1 f1 k1 -> m1 (\a1 -> f1 a1 k1)) x (\x' -> (\m2 f2 k2 -> m2 (\a2 -> f2 a2 k2)) y (\y' -> ($ x' + y')))

Сокращение некоторых функций приложения:

contAdd x y = (\k1 -> x (\a1 -> (\x' -> (\k2 -> y (\a2 -> (\y' -> ($ x' + y')) a2 k2))) a1 k1))

contAdd x y = (\k1 -> x (\a1 -> y (\a2 -> ($ a1 + a2) k1)))

И немного финальной перестановки и переименования:

contAdd x y = \k -> x (\x' -> y (\y' -> k $ x' + y'))

Другими словами: аргументы функции были изменены с чисел на функции, которые принимают число и возвращают конечный результат всего выражения, как и следовало ожидать.

Редактировать : Комментатор указывает, что contAdd сам по-прежнему принимает два аргумента в стиле карри. Это разумно, потому что оно не использует продолжение напрямую, но не обязательно. Чтобы сделать иначе, вам нужно сначала разбить функцию на части между аргументами:

contAdd x = x >>= (\x' -> return (\y -> y >>= (\y' -> return $ x' + y')))

А затем используйте это так:

foo = do f <- contAdd (return 1)
         r <- f (return 2)
         return r

Обратите внимание, что это действительно ничем не отличается от более ранней версии; это просто упаковывает результат каждого частичного применения как продолжение, а не только конечный результат. Поскольку функции являются первоклассными значениями, нет существенной разницы между выражением CPS, содержащим число, и выражением, содержащим функцию.

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

---

Добавление: вы можете заметить, что конечное выражение выглядит очень похоже на версию с моносами без десагаров. Это не совпадение, так как внутренняя вложенность монадических выражений, которая позволяет им изменять структуру вычислений на основе предыдущих значений, тесно связана со стилем прохождения продолжения; в обоих случаях вы в некотором смысле утвердили понятие причинности.

Answer 2

Краткий ответ: конечно, это имеет смысл, вы можете применить CPS-преобразование напрямую, у вас будет много ошибок, потому что каждый аргумент будет иметь, как вы заметили, свое собственное присоединенное продолжение

В вашем примере я буду считать, что существует +(x,y) неиспользуемый примитив, и что вы спрашиваете, что означает перевод

let add x y = +(x,y)

(Это add точно соответствует оператору OCaml (+))

add синтаксически эквивалентно

let add = fun x -> (fun y -> +(x, y))

Итак, вы применяете преобразование CPS¹ и получаете

let add_cps = fun x kx -> kx (fun y ky -> ky +(x,y))

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

¹: Я написал « a CPS-преобразование», потому что не существует «одного истинного CPS-преобразования». Были разработаны различные переводы, производящие более или менее связанный с продолжением мусор. Формальные переводы CPS обычно определяются непосредственно в лямбда-исчислении, поэтому я полагаю, что вы имеете в виду менее формальное, более ручное преобразование CPS.

Хорошие свойства CPS (как стиль , которые учитывает программа, а не конкретное преобразование в этот стиль) заключаются в том, что порядок вычисления является полностью явным и что все вызовы являются хвостовыми вызовами. Пока вы уважаете их, вы относительно свободны в том, что вы можете сделать. Таким образом, особенно хорошо обрабатывается функция curryfied.

Примечание: Ваша версия (cps-add k 1 2) также может считаться хвостовой рекурсивной, если вы предполагаете, что компилятор обнаруживает и оптимизирует, что cps-add на самом деле всегда принимает 3 аргумента и не создает промежуточных замыканий. Это может показаться надуманным, но это то же самое предположение, которое мы используем при рассуждении о хвостовых вызовах в программах, не относящихся к CPS, на этих языках.

Answer 3

Да, технически все функции можно разложить на функции одним методом, однако, когда вы хотите использовать CPS, единственное, что вы делаете, это говорите, что в определенной точке вычисления запустите метод продолжения.

Используя ваш пример, давайте посмотрим.Чтобы немного упростить ситуацию, давайте разберем cps-add в его обычной форме, где это функция, принимающая только один аргумент.

(cps-add k) -> n -> m = k ((+)nm)

Обратите внимание на то, что продолжение, k, не оценивается (может ли это быть для вас путаницей?).

Здесь у нас есть метод cps-addk, который получает функцию в качестве аргумента, а затем возвращает функцию, которая принимает другой аргумент, n.

((cps-add k) n) -> m = k ((+) nm)

Теперь у нас есть функция, которая принимает аргумент, м.

Итак, я предполагаю, что я пытаюсь указать, что карри не мешает программированию в стиле CPS.Надеюсь, это поможет.