Pourquoi les programmes fonctionnels ont-ils une corrélation entre le succès de la compilation et l'exactitude?

Je me dirige vers la programmation fonctionnelle depuis 4 ans maintenant, depuis que j'ai commencé à travailler avec LINQ. Récemment, j'ai écrit du code C # purement fonctionnel et j'ai remarqué, de première main, ce que j'ai lu sur les programmes fonctionnels - une fois qu'ils compilent, ils ont tendance à être corrects.

J'ai essayé de mettre un doigt sur pourquoi c'est le cas mais je n'y suis pas parvenu.

Une supposition est qu'en appliquant des principes OO, vous avez une "couche d'abstraction" qui n'est pas présente dans les programmes fonctionnels et cette couche d'abstraction permet aux contrats entre les objets d'être corrects tandis que l'implémentation est incorrecte.

Quelqu'un a-t-il pensé à cela et a-t-il trouvé la raison abstraite sous-jacente de la corrélation entre le succès de la compilation et l'exactitude du programme dans la programmation fonctionnelle?

Je peux écrire cette réponse comme quelqu'un qui prouve beaucoup de choses, donc pour moi l'exactitude n'est pas seulement ce qui fonctionne, mais ce qui fonctionne et est facile à prouver.

À bien des égards, la programmation fonctionnelle est plus restrictive que la programmation impérative. Après tout, rien ne vous empêche de ne jamais muter une variable en C! En effet, la plupart des fonctionnalités des langages FP sont simples à aborder en termes de quelques fonctionnalités de base. Tout se résume à peu près aux lambdas, à l'application de fonction et à la correspondance de modèles!

Cependant, puisque nous avons payé le joueur de pipeau à l'avance, nous avons beaucoup moins à gérer et nous avons beaucoup moins d'options sur la façon dont les choses peuvent mal tourner. Si vous êtes un fan de 1984, la liberté est en effet de l'esclavage! En utilisant 101 astuces différentes pour un programme, nous devons raisonner comme si n'importe laquelle de ces 101 choses pouvait arriver! C'est vraiment difficile à faire car il s'avère :)

Si vous commencez avec des ciseaux de sécurité au lieu d'une épée, courir est modérément moins dangereux.

Maintenant, nous examinons votre question: comment tout cela s'inscrit-il dans le "ça compile et fonctionne!" phénomènes. Je pense qu'une grande partie de cela est la même raison pour laquelle il est facile de prouver le code! Après tout, lorsque vous écrivez un logiciel, vous construisez une preuve informelle qu'il est correct. Pour cette raison, ce qui est couvert par vos preuves naturelles à la main et la propre notion de correction (typechecking) des compilateurs est beaucoup.

Lorsque vous ajoutez des fonctionnalités et des interactions complexes entre elles, ce qui n'est pas vérifié par le système de type augmente. Cependant, votre capacité à construire des preuves informelles ne semble pas s'améliorer! Cela signifie qu'il y a plus de choses qui peuvent passer à travers votre inspection initiale et qui doivent être capturées plus tard.

la raison abstraite sous-jacente de la corrélation entre le succès de la compilation et l'exactitude du programme en programmation fonctionnelle?

État mutable.

Les compilateurs vérifient les choses statiquement. Ils s'assurent que votre programme est bien formé et le système de type fournit un mécanisme pour essayer de s'assurer que le bon type de valeurs est autorisé au bon type d'endroits. Le système de types essaie également de garantir que le bon type de sémantique est autorisé dans le bon type d'emplacements.

Dès que votre programme introduit l'état, cette dernière contrainte devient moins utile. Non seulement vous devez vous soucier des bonnes valeurs aux bons endroits, mais vous devez également tenir compte du fait que cette valeur change à des points arbitraires de votre programme. Vous devez tenir compte de la sémantique de votre code changeant à côté de cet état.

Si vous faites bien la programmation fonctionnelle, il n'y a pas (ou très peu) d'état mutable.

Il y a cependant un débat sur la causalité ici - si les programmes sans état fonctionnent plus fréquemment après la compilation parce que le compilateur peut détecter plus de bogues ou si les programmes sans état fonctionnent plus souvent après la compilation parce que ce style de programmation produit moins de bogues.

C'est probablement un mélange des deux dans mon expérience.

Pour le dire simplement, les restrictions signifient qu'il y a moins de façons correctes de rassembler les choses, et les fonctions de première classe facilitent la factorisation de choses comme les structures de boucle. Prenez la boucle de cette réponse , par exemple:

for (Iterator<String> iterator = list.iterator(); iterator.hasNext();) {
    String string = iterator.next();
    if (string.isEmpty()) {
        iterator.remove();
    }
}

Il se trouve que c'est le seul moyen impératif et sûr de Java pour supprimer un élément d'une collection pendant que vous l'itérez. Il existe de nombreuses façons qui semblent très proches, mais qui sont erronées. Les personnes qui ne connaissent pas cette méthode passent parfois par des moyens compliqués pour éviter le problème, comme une itération à travers une copie à la place.

Ce n'est pas très difficile de rendre ce générique, donc cela fonctionnera sur plus que des collections de Strings, mais sans fonctions de première classe, vous ne pouvez pas remplacer le prédicat (la condition à l'intérieur du if), donc ce code a tendance à être copié et collé et légèrement modifié.

Combinez des fonctions de première classe qui vous donnent la possibilité de passer le prédicat en tant que paramètre, avec la restriction de l'immuabilité qui le rend très ennuyeux si vous ne le faites pas, et vous obtenez de simples blocs de construction comme filter, comme dans ce code Scala cela fait la même chose:

list filter (!_.isEmpty)

Pensez maintenant à ce que le système de type vérifie pour vous, au moment de la compilation dans le cas de Scala, mais ces vérifications sont également effectuées par les systèmes de type dynamiques la première fois que vous l'exécutez:

• listdoit être une sorte de type qui prend en charge la filterméthode, à savoir une collection.
• Les éléments de listdoivent avoir une isEmptyméthode qui renvoie un booléen.
• La sortie sera une collection (potentiellement) plus petite avec le même type d'éléments.

Une fois que ces choses ont été vérifiées, quelles sont les autres façons pour le programmeur de bousiller? J'ai oublié accidentellement !, ce qui a provoqué une défaillance de cas de test extrêmement évidente. C'est à peu près la seule erreur disponible à faire, et je ne l'ai fait que parce que je traduisais directement à partir du code qui a testé la condition inverse.

Ce modèle se répète encore et encore. Les fonctions de première classe vous permettent de refaçonner les choses en petits utilitaires réutilisables avec une sémantique précise, des restrictions comme l'immuabilité vous donnent l'impulsion pour le faire, et la vérification du type des paramètres de ces utilitaires laisse peu de place pour les visser.

Bien sûr, tout cela dépend du programmeur sachant que la fonction de simplification comme filterexiste déjà, et capable de la trouver, ou de reconnaître l'avantage d'en créer une vous-même. Essayez de l'implémenter vous-même partout en utilisant uniquement la récursivité de la queue, et vous êtes de retour dans le même bateau de complexité que la version impérative, pire encore. Ce n'est pas parce que vous pouvez l' écrire très simplement que la version simple est évidente.

Je ne pense pas qu'il existe une corrélation significative entre la compilation de la programmation fonctionnelle et l'exactitude de l'exécution. Il peut y avoir une certaine corrélation entre la compilation typée statiquement et l'exactitude de l'exécution, car au moins vous pouvez avoir les bons types, si vous ne diffusez pas.

L'aspect du langage de programmation qui peut en quelque sorte corréler la compilation réussie avec l'exactitude du type d'exécution, comme vous le décrivez, est le typage statique, et même alors, seulement si vous n'affaiblissez pas le vérificateur de type avec des transtypages qui ne peuvent être affirmés qu'au moment de l'exécution (dans les environnements avec valeurs ou emplacements fortement typés, par exemple Java ou .Net) ou pas du tout (dans les environnements où les informations de type sont perdues ou avec un typage faible, par exemple C et C ++).

Cependant, la programmation fonctionnelle en soi peut aider d'autres façons, comme éviter les données partagées et l'état mutable.

Ensemble, les deux aspects peuvent avoir une corrélation significative dans l'exactitude, mais vous devez être conscient que l'absence d'erreurs de compilation et d'exécution ne dit rien, à proprement parler, sur l'exactitude au sens large, comme dans le programme fait ce qu'il est censé faire et échoue rapidement sur entrée non valide ou échec d'exécution incontrôlable. Pour cela, vous avez besoin de règles métier, d'exigences, de cas d'utilisation, d'assertions, de tests unitaires, de tests d'intégration, etc. En fin de compte, du moins à mon avis, ils offrent beaucoup plus de confiance que la programmation fonctionnelle, la saisie statique ou les deux.

Explication pour les managers:

Un programme fonctionnel est comme une grande machine où tout est connecté, tubes, câbles. [Une voiture]

Un programme procédural est comme un bâtiment avec des pièces contenant une petite machine, stockant des produits partiels dans des bacs, obtenant des produits partiels d'ailleurs. [Une usine]

Ainsi, lorsque la machine fonctionnelle s'emboîte déjà: elle est appelée à produire quelque chose. Si un complexe procédural s'exécute, vous pourriez avoir supervisé des effets spécifiques, introduit le chaos, pas garanti le fonctionnement. Même si vous avez une liste de contrôle de tout ce qui est correctement intégré, il y a tellement d'états, de situations possibles (produits partiels qui traînent, seaux débordants, manquants), que les garanties sont difficiles à donner.

Mais sérieusement, le code procédural ne spécifie pas la sémantique du résultat souhaité autant que le code fonctionnel. Les programmeurs procéduraux peuvent plus facilement échapper au code et aux données circonstanciels et introduire plusieurs façons de faire une chose (certaines imparfaites). Généralement, des données superflues sont créées. Les programmeurs fonctionnels peuvent prendre plus de temps lorsque le problème devient plus complexe?

Un langage fonctionnel typé fort peut toujours améliorer l'analyse des données et des flux. Avec un langage procédural, l'objectif d'un programme doit souvent être défini en dehors du programme, comme une analyse formelle de l'exactitude.