Pourquoi récursif `let` rend l’espace effcient?

J’ai trouvé cette déclaration en étudiant la Programmation Réactive Fonctionnelle, à partir de “Brancher une fuite d’espace avec une flèche” de Hai Liu et Paul Hudak (page 5):

Suppose we wish to define a function that repeats its argument indefinitely: repeat x = x : repeat x or, in lambdas: repeat = λx → x : repeat x This requires O(n) space. But we can achieve O(1) space by writing instead: repeat = λx → let xs = x : xs in xs 

La différence semble minime, mais elle incite énormément à l’efficacité de l’espace. Pourquoi et comment ça se passe? La meilleure conjecture que j’ai faite est de les évaluer à la main:

  r = \x -> x: rx r 3 -> 3: r 3 -> 3: 3: 3: ........ -> [3,3,3,......] 

Comme ci-dessus, nous devrons créer de nouveaux thunks infinis pour ces récursions. Ensuite, j’essaie d’évaluer le second:

  r = \x -> let xs = x:xs in xs r 3 -> let xs = 3:xs in xs -> xs, according to the definition above: -> 3:xs, where xs = 3:xs -> 3:xs:xs, where xs = 3:xs 

Dans la deuxième forme, le xs apparaît et peut être partagé entre chaque endroit où il se produit, donc je suppose que c’est la raison pour laquelle nous ne pouvons exiger que des espaces O(1) plutôt que O(n) . Mais je ne sais pas si j’ai raison ou pas.

BTW: Le mot clé “shared” provient de la même page de l’article 4:

Le problème ici est que les règles d’évaluation standard des besoins par appel ne peuvent pas reconnaître que la fonction:

 f = λdt → integralC (1 + dt) (f dt) 

est le même que:

 f = λdt → let x = integralC (1 + dt) x in x 

La première définition entraîne la répétition du travail dans l’appel récursif à f, alors que dans le second cas, le calcul est partagé.

C’est plus facile à comprendre avec des images:

  • La première version

     repeat x = x : repeat x 

    crée une chaîne de (:) constructeurs se terminant par un thunk qui se remplacera par plus de constructeurs à la demande. Ainsi, O (n) espace.

    une chaîne

  • La deuxième version

     repeat x = let xs = x : xs in xs 

    utilise let pour “lier le noeud”, en créant un seul constructeur (:) qui se réfère à lui-même.

    une boucle

En d’autres termes, les variables sont partagées, mais les applications de fonction ne le sont pas. Dans

 repeat x = x : repeat x 

c’est une coïncidence (du sharepoint vue du langage) que l’appel (co) récursif à répéter est avec le même argument. Ainsi, sans optimisation supplémentaire (appelée transformation des arguments statiques), la fonction sera appelée à plusieurs resockets.

Mais quand tu écris

 repeat x = let xs = x : xs in xs 

il n’y a pas d’appel de fonction récursif. Vous prenez un x et construisez une valeur cyclique xs utilisant. Tout partage est explicite.

Si vous voulez le comprendre de manière plus formelle, vous devez vous familiariser avec la sémantique de l’évaluation paresseuse, telle que La sémantique naturelle pour l’évaluation paresseuse .

Votre intuition à propos du partage de xs est correcte. Pour réitérer l’exemple de l’auteur en termes de répétition, au lieu d’intégrale, lorsque vous écrivez:

 repeat x = x : repeat x 

le langage ne reconnaît pas que la repeat x à droite est identique à la valeur produite par l’expression x : repeat x . Alors que si vous écrivez

 repeat x = let xs = x : xs in xs 

vous créez explicitement une structure qui, lorsqu’elle est évaluée, ressemble à ceci:

 {hd: x, tl:|} ^ | \________/