Existe-t-il une définition canonique de la fonction «pure»?

9

StackOverflow m'a pointé ici, donc la question pourrait être un peu en termes simples.

Wikipedia définit les fonctions pures comme

En programmation informatique, une fonction peut être décrite comme une fonction pure si ces deux déclarations sur la fonction sont valables:

  1. La fonction évalue toujours la même valeur de résultat pour les mêmes valeurs d'argument. La valeur de résultat de la fonction ne peut dépendre d'aucune information ou état caché susceptible de changer au cours de l'exécution du programme ou entre différentes exécutions du programme, ni de toute entrée externe provenant de périphériques d'E / S.
  2. L'évaluation du résultat ne provoque aucun effet secondaire ou sortie sémantiquement observable, comme une mutation d'objets mutables ou une sortie vers des dispositifs d'E / S.

Cependant, il ne semble pas citer de sources - il est donc difficile de dire s'il s'agit d'une définition acceptée ou qui l'a définie de cette façon.

Quand je regarde ce que font les langages quand ils incluent une syntaxe / annotation pour les fonctions "pures", il y a pas mal d'approches différentes:

  1. En D, la seule limitation est la non-mutation de l'état global. Les fonctions "pures" peuvent muter ses arguments.
  2. Dans GCC, il existe deux types de "pur": pure(pas d'effets secondaires, mais peut lire l'état global) et const(strictement pur selon la définition de wikipedia).
  3. En C # , il est défini comme "ne fait aucun changement d'état visible" (quel qu'il soit).
  4. Haskell suit la définition de Wikipedia.

Ma question est donc la suivante: existe-t-il une définition canonique de la fonction pure?
Et s'il y en a, quelle est sa source?

terminology functional-programming semantics Andrey Shchekin
la source
Perspective historique connexe , bien que personne ne semble donner de réponses définitives ou d'origine.
Guildenstern
1
Cela ne vaut pas une réponse mais voici ma définition: si x = y (par sa définition) alors fx = fy est vrai et f ne provoque aucun changement d'état mesurable de manière externe (c'est-à-dire que tout changement d'état est interne à x, y, et f). Haskell en profite. Il implémente l'évaluation paresseuse en mutant les thunks et en les remplaçant par des fonctions qui retournent le résultat immédiatement. C'est-à-dire que si vous évaluez (fx) cela peut réellement changer f et x sous le capot mais vous ne pouvez jamais le dire.
Jake

Réponses:

3

Comme indiqué dans cet article Imperative Functional Programming , (1993) par Peyton-Jones et Wadler (parmi le groupe de chercheurs qui a créé Haskell):

Nous nous concentrons sur des solutions purement fonctionnelles, qui excluent les effets secondaires, pour deux raisons. Premièrement, l'absence d'effets secondaires permet une utilisation illimitée du raisonnement équationnel et de la transformation des programmes ...

l'accent est mis sur l'absence d'effets secondaires pour permettre les transformations de programme (c'est-à-dire les optimisations du compilateur).

Quels sont les effets secondaires? Cet article pointe à son tour vers la programmation fonctionnelle et impérative (1986) de Gifford et Lucassen, qui mentionne quatre types de classes d'effets : Pure, Function, Observer et Procedure. Ainsi, le terme «fonction pure» dérive de cet article.

  • un PURE est référentiellement transparent: il ne provoque pas d'effets secondaires, sa valeur n'est pas affectée par les effets secondaires et il renvoie la même valeur chaque fois qu'il est évalué.

Notez, cependant, que Peyton-Jones et Wadler ont mentionné des lacunes dans cette approche. Il convient de noter, disent-ils, que le langage de programmation Clean utilise des types linéaires pour introduire les effets secondaires de manière sûre (c'est-à-dire sans danger pour le compilateur). Fondamentalement, il enfile le monde en tant que variable dans toutes les fonctions liées aux E / S, y compris le point d'entrée principal .

Avec cela, il est possible d'avoir un langage fonctionnel pur interagissant avec le monde et ayant des effets secondaires (E / S, OS, système de fenêtrage, etc.), contredisant partiellement votre définition wikipedia. On peut en fait dire que Haskell a Clean comme l'un de ses influenceurs; bien qu'il s'écarte des types linéaires et utilise une autre construction de niveau type (monades) pour garantir la linéarité, c'est-à-dire une référence unique à tout moment.

carlosayam
la source
"Fondamentalement, il enfile le monde comme une variable ...". Voulez-vous vraiment dire "fils". Y a-t-il un compte informel de cela sur le web?
babou
J'ai utilisé le «filetage» comme métaphore. Cela signifie que vous devez passer la variable World d'une fonction à une autre. Et le typage linéaire signifie qu'une telle variable World n'est pas utilisée plus d'une fois. Cela implique, par exemple, que pour ouvrir un fichier à l'intérieur d'une fonction, vous voudriez (f_handle, world2) = fopen file_name, world(pseudocode) et qu'un prochain appel devra utiliser world2. En substance, les programmes sont perçus comme fonctionnant sur l' Univers dans son ensemble. Autrement dit, il n'y a pas d'effets secondaires lorsque vous
opérez
Threading the World, comme vous le dites, semble être la manière standard (si je me souviens bien) de gérer l'environnement dans la sémantique dénotationnelle. Le point clé doit donc être la linéarité. Mais alors, la sémantique dénotationnelle (DS) est censée être purement fonctionnelle, sans aucune contrainte de linéarité. Je suppose que DS est une abstraction mathématique et n'a aucun scrupule à jongler avec de nombreux mondes. L'informatique est physique et la linéarité permet l'évolution du monde, mais un seul monde peut exister à la fois (ce qui séquentielle probablement l'évaluation). Quelle est la sémantique de 2 programmes Clean exécutés simultanément :-)?
babou
Le document Gifford et Lucassen est-il accessible sur le Web?
babou
J'ai eu accès à l'Uni.
carlosayam
-1

La définition de Wikipédia est canonique. Les deux exigences cruciales sont:

  • La valeur de retour et le comportement de la fonction sont une fonction déterministe des arguments qui ont été explicitement passés à la fonction.

  • Une invocation de la fonction n'a pas d'effets secondaires observables.

À strictement parler, D et gcc ne devraient pas utiliser le mot «pur» comme ils le font; c'est un abus de terminologie standard.

DW
la source