Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Оператор управления потоком в функциональном программировании
Control flow operator in functional programming
В языке программирования Scheme в качестве оператора управления потоком используется вызов процедуры с текущим продолжением, сокращенно call/cc. Он был принят несколькими другими языками программирования. Принимая функцию f в качестве единственного аргумента, (call/cc f) в выражении применяется к текущему продолжению этого выражения. Например, ((call/cc f) e2) эквивалентно применению f к текущему продолжению выражения. Текущее продолжение получается заменой (call/cc f) на переменную c, связанную с лямбда-абстракцией, таким образом, текущее продолжение будет (lambda (c) (c e2)). Применение функции f к нему дает конечный результат (f (lambda (c) (c e2))). В качестве дополнительного примера, в выражении (e1 (call/cc f)), продолжение для подвыражения (call/cc f) равно (lambda (c) (e1 c)), поэтому всё выражение эквивалентно (f (lambda (c) (e1 c))). Другими словами, он делает "снимок" текущего контекста управления или состояния программы как объекта и применяет к нему f. Объект продолжения является значением первого класса и представлен в виде функции, а применение функции – его единственная операция. Когда объект продолжения применяется к аргументу, существующее продолжение удаляется и на его место восстанавливается примененное продолжение, так что выполнение программы продолжится с точки, в которой продолжение было захвачено, а аргумент продолжения становится "возвращаемым значением" вызова call/cc. Продолжения, созданные с помощью call/cc, могут быть вызваны несколько раз, и даже вне динамической области применения call/cc. В информатике, представление неявного состояния программы в виде объекта называется реификацией. (Scheme синтаксически не различает применение продолжений и функций.) С помощью call/cc можно реализовать различные сложные операторы управления из других языков всего за несколько строк кода, например, оператор amb Маккарти для недетерминированного выбора, отслеживание в стиле Prolog, корутины в стиле Simula 67 и их обобщения, генераторы в стиле Icon, или движки и потоки, или даже малоизвестный COMEFROM.
In the Scheme computer programming language, the procedure call with current continuation, abbreviated call/cc, is used as a control flow operator. It has been adopted by several other programming languages. Taking a function f as its only argument, (call/cc f) within an expression is applied to the current continuation of the expression. For example ((call/cc f) e2) is equivalent to applying f to the current continuation of the expression. The current continuation is given by replacing (call/cc f) by a variable c bound by a lambda abstraction, so the current continuation is (lambda (c) (c e2)). Applying the function f to it gives the final result (f (lambda (c) (c e2))). As a complementary example, in an expression (e1 (call/cc f)), the continuation for the sub expression (call/cc f) is (lambda (c) (e1 c)), so the whole expression is equivalent to (f (lambda (c) (e1 c))). In other words it takes a "snapshot" of the current control context or control state of the program as an object and applies f to it. The continuation object is a first class value and is represented as a function, with function application as its only operation. When a continuation object is applied to an argument, the existing continuation is eliminated and the applied continuation is restored in its place, so that the program flow will continue at the point at which the continuation was captured and the argument of the continuation then becomes the "return value" of the call/cc invocation. Continuations created with call/cc may be called more than once, and even from outside the dynamic extent of the call/cc application. In computer science, making this type of implicit program state visible as an object is termed reification. (Scheme does not syntactically distinguish between applying continuations or functions.) With call/cc a variety of complex control operators can be implemented from other languages via a few lines of code, e. g., McCarthy's amb operator for nondeterministic choice, Prolog style backtracking, Simula 67 style coroutines and generalizations thereof, Icon style generators, or engines and threads or even the obscure COMEFROM.
Критика
Олег Киселев, автор реализации ограниченных продолжений для OCaml и разработчик интерфейса прикладного программирования (API) для манипулирования ограниченным стеком с целью реализации операторов управления, выступает за использование ограниченных продолжений вместо полных стековых продолжений, с которыми работает call/cc: "Использование call/cc в качестве базовой управляющей конструкции, на основе которой должны реализовываться все остальные средства управления, оказывается неудачным решением. Производительность, утечки памяти и ресурсов, простота реализации, удобство использования и понятность рассуждений – все говорит против call/cc."
Oleg Kiselyov, author of a delimited continuation implementation for OCaml, and designer of an application programming interface (API) for delimited stack manipulation to implement control operators, advocates the use of delimited continuations instead of the full stack continuations that call/cc manipulates: "Offering call/cc as a core control feature in terms of which all other control facilities should be implemented turns out a bad idea. Performance, memory and resource leaks, ease of implementation, ease of use, ease of reasoning all argue against call/cc."
Отношение к неконструктивной логике
Корреспонденция Карри-Ховарда между доказательствами и программами связывает call/cc с законом Пирса, который расширяет интуиционистскую логику до неконструктивной, классической логики: ((α → β) → α) → α. Здесь ((α → β) → α) является типом функции f, которая может либо непосредственно возвращать значение типа α, либо применить аргумент к продолжению типа (α → β). Поскольку существующий контекст удаляется при применении продолжения, тип β никогда не используется и может считаться ⊥, пустым типом. Принцип устранения двойного отрицания ((α → ⊥) → ⊥) → α сопоставим с вариантом call/cc, который ожидает, что его аргумент f всегда будет вычислять текущее продолжение, не возвращая значение обычным образом. Встраивания классической логики в интуиционистскую логику связаны с преобразованием в стиле передачи продолжения.
The Curry–Howard correspondence between proofs and programs relates call/cc to Peirce's law, which extends intuitionistic logic to non constructive, classical logic: ((α → β) → α) → α. Here, ((α → β) → α) is the type of the function f, which can either return a value of type α directly or apply an argument to the continuation of type (α → β). Since the existing context is deleted when the continuation is applied, the type β is never used and may be taken to be ⊥, the empty type. The principle of double negation elimination ((α → ⊥) → ⊥) → α is comparable to a variant of call cc which expects its argument f to always evaluate the current continuation without normally returning a value. Embeddings of classical logic into intuitionistic logic are related to continuation passing style translation.