La page "Advanced Scheme: Some Naughty Bits" indique:
Les continuations sont une puissante structure de contrôle-flux à partir de laquelle presque toute autre structure de contrôle-flux [...] peut être dérivée.
Je pensais que Scheme call/cc
, étant lié (*) à l'opérateur J de Peter Landin, pourrait être utilisé pour implémenter n'importe quelle structure de flux de contrôle connue?
Avec "structure de flux de contrôle", je pense spécifiquement à la description de Wikipédia , par exemple les exceptions, les coroutines, les fils verts, etc.
Plus précisément, existe-t-il des exemples de structures de flux de contrôle qui ne peuvent pas être implémentées à l'aide call/cc
?
(*) Je n'ai pas pu déterrer de papier établissant qu'il call/cc
est aussi puissant que l'opérateur J. Un article de Felleisen (que je n'ai pas lu et qui a certes du mal à le comprendre) étudie cela et semble conclure que même s'ils appartiennent à différentes classes de complexité, ils sont formellement équivalents.
(Notez également que j'ai mis à jour la question sur la base des commentaires ci-dessous)
Mise à jour
Sur la base de l'excellente réponse de @Neel ci-dessous, j'ai regardé des sites commentant des suites délimitées et non délimitées , et il semble en effet que call/cc
, étant non délimité, ce n'est pas suffisant. Pendant ce temps, des suites délimitées de première classe (comme shift/reset
) peuvent être utilisées, semble-t-il, pour exprimer toute structure de flux de contrôle.
call/cc
ne peuvent pas exprimer d'exceptions en l'absence d'État . (Comme le souligne Thielecke, des exceptions peuvent être implémentées en passant autour de deux continuations, une pour le programme et l'autre pour le gestionnaire d'exceptions, mais cela nécessite plus que justecall/cc
.)amb
opérateur-, etc.Réponses:
Dans cette réponse, je considérerai "expressible" comme "macro-expressible" au sens de Felleisen 1991, On The Expressive Power of Programming Languages . (Intuitivement, une fonction de langage est macro-exprimable si vous pouvez la définir comme une transformation source locale, sans utiliser une transformation de programme entier.)
Avec cette définition, la réponse est non : le contrôle délimité n'est pas macro-expressible dans le lambda-calcul + appel / cc. Pour exprimer des opérateurs de contrôle délimités à l'aide de call / cc. Afin d'implémenter les délimiteurs de contrôle (la partie réinitialisation de shift / reset), vous avez besoin d'un état pour simuler les marques de continuation, essentiellement pour coder une pile pour simuler les durées de vie dynamiques des marques de continuation.
Cependant, le contrôle délimité est un effet universel, dans le sens suivant. Dans sa thèse de doctorat , Andrzej Filinski a montré que tout effet secondaire exprimable est codable en utilisant soit des continuations délimitées, soit un appel / cc et une seule cellule d'état. En gros, un "effet secondaire exprimable" est tout effet dont le type monadique peut être défini en termes de types de langage de programmation.
Étonnamment, cette idée semble assez intéressante dans la pratique. Au cours de la dernière décennie, Gordon Plotkin et John Power ont défendu l'idée de prendre une sémantique algébrique des théories des effets : l'idée est que vous spécifiez les opérations d'effets secondaires qui vous intéressent et les équations que vous attendez qu'elles satisfassent, puis vous pouvez génériquement obtenir une sémantique en prenant la monade libre sur cette théorie.
Matija Pretnar et Andrej Bauer ont adopté cette approche mathématique, puis l'ont implémentée dans leur langage Eff pour inventer une nouvelle construction de langage appelée "gestionnaires d'effets": vous pouvez écrire du code qui utilise un ensemble de fonctionnalités impératives, puis donner aux fonctionnalités impératives une sémantique en écrivant un ensemble de gestionnaires qui expliquent comment implémenter chaque opération efficace.
la source