En programmation fonctionnelle, comment parvient-on à la modularité grâce aux lois mathématiques?

J'ai lu dans cette question que les programmeurs fonctionnels ont tendance à utiliser des preuves mathématiques pour s'assurer que leur programme fonctionne correctement. Cela semble beaucoup plus facile et plus rapide que les tests unitaires, mais venant d'un arrière-plan OOP / Unit Testing, je ne l'ai jamais vu faire.

Pouvez-vous me l'expliquer et me donner un exemple?

Une preuve est beaucoup plus difficile dans le monde OOP en raison des effets secondaires, de l'héritage illimité et du fait d' nullêtre membre de tout type. La plupart des preuves reposent sur un principe d'induction pour montrer que vous avez couvert toutes les possibilités, et ces 3 éléments rendent cela plus difficile à prouver.

Disons que nous implémentons des arbres binaires qui contiennent des valeurs entières (dans un souci de simplification de la syntaxe, je n'y apporterai pas de programmation générique, bien que cela ne changera rien.) Dans ML standard, je définirais cela comme ce:

datatype tree = Empty | Node of (tree * int * tree)

Cela introduit un nouveau type appelé treedont les valeurs peuvent se présenter dans exactement deux variétés (ou classes, à ne pas confondre avec le concept OOP d'une classe) - une Emptyvaleur qui ne contient aucune information et des Nodevaleurs qui portent un triplet dont le premier et le dernier les éléments sont trees et dont l'élément central est un int. L'approximation la plus proche de cette déclaration dans la POO ressemblerait à ceci:

public class Tree {
    private Tree() {} // Prevent external subclassing

    public static final class Empty extends Tree {}

    public static final class Node extends Tree {
        public final Tree leftChild;
        public final int value;
        public final Tree rightChild;

        public Node(Tree leftChild, int value, Tree rightChild) {
            this.leftChild = leftChild;
            this.value = value;
            this.rightChild = rightChild;
        }
    }
}

Avec la mise en garde que les variables de type Tree ne peuvent jamais l'être null.

Écrivons maintenant une fonction pour calculer la hauteur (ou la profondeur) de l'arbre, et supposons que nous avons accès à une maxfonction qui renvoie le plus grand de deux nombres:

fun height(Empty) =
        0
 |  height(Node (leftChild, value, rightChild)) =
        1 + max( height(leftChild), height(rightChild) )

Nous avons défini la heightfonction par cas - il y a une définition pour les Emptyarbres et une définition pour les Nodearbres. Le compilateur sait combien de classes d'arbres existent et émettrait un avertissement si vous ne définissiez pas les deux cas. L'expression Node (leftChild, value, rightChild)de la signature de la fonction lie les valeurs du 3-tuple aux variables leftChild, valueet rightChildrespectivement afin que nous puissions faire référence dans la définition de la fonction. Cela revient à déclarer des variables locales comme celle-ci dans un langage OOP:

Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();

Comment prouver que nous avons mis en œuvre heightcorrectement? Nous pouvons utiliser l' induction structurelle , qui consiste à: 1. prouver que heightc'est correct dans le ou les cas de base de notre treetype ( Empty) 2. en supposant que les appels récursifs à heightsont corrects, prouver que heightc'est correct pour le cas non-base (s ) (lorsque l'arbre est en fait un Node).

Pour l'étape 1, nous pouvons voir que la fonction retourne toujours 0 lorsque l'argument est un Emptyarbre. Ceci est correct par définition de la hauteur d'un arbre.

Pour l'étape 2, la fonction revient 1 + max( height(leftChild), height(rightChild) ). En supposant que les appels récursifs retournent vraiment la taille des enfants, nous pouvons voir que cela est également correct.

Et cela complète la preuve. Les étapes 1 et 2 combinées épuisent toutes les possibilités. Notez, cependant, que nous n'avons pas de mutation, pas de null et qu'il existe exactement deux variétés d'arbres. Supprimez ces trois conditions et la preuve devient rapidement plus compliquée, voire impossible.

EDIT: Puisque cette réponse a atteint le sommet, je voudrais ajouter un exemple moins trivial d'une preuve et couvrir l'induction structurelle un peu plus en profondeur. Ci-dessus, nous avons prouvé que si heightretourne , sa valeur de retour est correcte. Cependant, nous n'avons pas prouvé qu'il renvoie toujours une valeur. Nous pouvons également utiliser l'induction structurelle pour le prouver (ou toute autre propriété). Encore une fois, à l'étape 2, nous sommes autorisés à supposer que la propriété détient des appels récursifs tant que les appels récursifs fonctionnent tous sur un enfant direct du arbre.

Une fonction peut ne pas retourner une valeur dans deux situations: si elle lève une exception et si elle boucle pour toujours. Prouvons d'abord que si aucune exception n'est levée, la fonction se termine:

1. Prouver que (si aucune exception n'est levée) la fonction se termine pour les cas de base ( Empty). Puisque nous renvoyons inconditionnellement 0, il se termine.

2. Prouver que la fonction se termine dans les cas non-base ( Node). Il y a trois appels de fonction ici: +, maxet height. Nous le savons +et nous nous maxterminons parce qu'ils font partie de la bibliothèque standard du langage et ils sont définis de cette façon. Comme mentionné précédemment, nous sommes autorisés à supposer que la propriété que nous essayons de prouver est vraie sur les appels récursifs tant qu'ils opèrent sur des sous-arbres immédiats, donc les appels se heightterminent également.

Cela conclut la preuve. Notez que vous ne pourrez pas prouver la terminaison avec un test unitaire. Il ne reste plus qu'à montrer que heightcela ne lève pas d'exceptions.

1. Prouvez que heightcela ne lève pas d'exceptions sur le cas de base ( Empty). Renvoyer 0 ne peut pas lever d'exception, nous avons donc terminé.
2. Prouvez que heightcela ne lève pas d'exception sur le cas non-base ( Node). Supposons encore une fois que nous connaissons +et maxne lançons pas d'exceptions. Et l'induction structurelle nous permet de supposer que les appels récursifs ne lanceront pas non plus (car ils opèrent sur les enfants immédiats de l'arbre). Mais attendez! Cette fonction est récursive, mais pas récursive de queue . On pourrait faire sauter la pile! Notre tentative de preuve a révélé un bogue. Nous pouvons le corriger en changeant heightpour être récursif de queue .

J'espère que cela montre que les preuves ne doivent pas être effrayantes ou compliquées. En fait, chaque fois que vous écrivez du code, vous avez construit de manière informelle une preuve dans votre tête (sinon, vous ne seriez pas convaincu que vous venez d'implémenter la fonction.) En évitant la mutation nulle, inutile et l'héritage illimité, vous pouvez prouver que votre intuition est corriger assez facilement. Ces restrictions ne sont pas aussi sévères que vous pourriez le penser:

• null est un défaut de langage et le supprimer est inconditionnellement bon.
• La mutation est parfois inévitable et nécessaire, mais elle est nécessaire beaucoup moins souvent que vous ne le pensez - en particulier lorsque vous avez des structures de données persistantes.
• Quant à avoir un nombre fini de classes (au sens fonctionnel) / sous-classes (au sens de la POO) vs un nombre illimité d'entre elles, c'est un sujet trop grand pour une seule réponse . Qu'il suffise de dire qu'il y a un compromis de conception là-bas - prouvabilité de l'exactitude vs flexibilité de l'extension.

1. Il est beaucoup plus facile de raisonner sur le code lorsque tout est immuable . Par conséquent, les boucles sont le plus souvent écrites sous forme de récursivité. En général, il est plus facile de vérifier l'exactitude d'une solution récursive. Souvent, une telle solution se lira également de manière très similaire à une définition mathématique du problème.

   Cependant, dans la plupart des cas, il y a très peu de motivation pour effectuer une véritable preuve formelle d'exactitude. Les preuves sont difficiles, prennent beaucoup de temps (humain) et ont un faible retour sur investissement.

2. Certains langages fonctionnels (en particulier de la famille ML) ont des systèmes de type extrêmement expressifs qui peuvent faire des garanties beaucoup plus complètes qu'un système de type C (mais certaines idées comme les génériques sont également devenues courantes dans les langages traditionnels). Lorsqu'un programme réussit une vérification de type, il s'agit d'une sorte de preuve automatisée. Dans certains cas, cela pourra détecter certaines erreurs (par exemple, oublier le cas de base dans une récursivité, ou oublier de gérer certains cas dans une correspondance de modèle).

   D'autre part, ces systèmes de type doivent être maintenus très limités afin de les garder décidables . Donc, dans un sens, nous gagnons des garanties statiques en abandonnant la flexibilité - et ces restrictions sont une raison pour laquelle des articles universitaires compliqués du type « Une solution monadique à un problème résolu, en Haskell » existent.

   J'apprécie à la fois les langues très libérales et les langues très restreintes, et les deux ont leurs difficultés respectives. Mais ce n'est pas le cas que l'on serait «mieux», chacun est juste plus pratique pour un type de tâche différent.

Il faut ensuite souligner que les preuves et les tests unitaires ne sont pas interchangeables. Ils nous permettent tous les deux de mettre des limites à l'exactitude du programme:

• Les tests mettent une limite supérieure à l'exactitude: si un test échoue, le programme est incorrect, si aucun test échoue, nous sommes certains que le programme gérera les cas testés, mais il peut toujours y avoir des bogues non découverts.

  int factorial(int n) {
    if (n <= 1) return 1;
    if (n == 2) return 2;
    if (n == 3) return 6;
    return -1;
  }
  
  assert(factorial(0) == 1);
  assert(factorial(1) == 1);
  assert(factorial(3) == 6);
  // oops, we forgot to test that it handles n > 3…
  

• Les preuves mettent une limite inférieure à l'exactitude: il peut être impossible de prouver certaines propriétés. Par exemple, il peut être facile de prouver qu'une fonction renvoie toujours un nombre (c'est ce que font les systèmes de types). Mais il peut être impossible de prouver que le nombre sera toujours < 10.

  int factorial(int n) {
    return n;  // FIXME this is just a placeholder to make it compile
  }
  
  // type system says this will be OK…
  

Un mot d'avertissement peut être de mise ici:

Bien qu'il soit généralement vrai ce que les autres écrivent ici - en bref, que les systèmes de type avancés, l'immuabilité et la transparence référentielle contribuent beaucoup à l'exactitude - il n'est pas vrai que les tests ne sont pas effectués dans le monde fonctionnel. Au contraire !

En effet, nous avons des outils comme Quickcheck, qui génèrent des cas de test automatiquement et de manière aléatoire. Vous énoncez simplement les lois auxquelles une fonction doit obéir, puis la vérification rapide vérifie ces lois pour des centaines de cas de test aléatoires.

Vous voyez, c'est un niveau un peu plus élevé que les contrôles d'égalité triviaux sur une poignée de cas de test.

Voici un exemple d'une implémentation d'une arborescence AVL:

--- A generator for arbitrary Trees with integer keys and string values
aTree = arbitrary :: Gen (Tree Int String)


--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (\t -> 
             forAll arbitrary (\k ->
               forAll arbitrary (\v ->
                lookup (insert t k v) k == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (\t ->
            not (null t) ==> forAll (elements (keys t)) (\k ->
                lookup (delete t k) k == Nothing))

La deuxième loi (ou propriété) peut être lue comme suit: Pour tous les arbres arbitraires t, la règle suivante est valable: si elle tn'est pas vide, alors pour toutes les clés kde cet arbre, elle contiendra la recherche kdans l'arbre qui résulte de la suppression. kà partir de t, le résultat sera Nothing(ce qui indique: introuvable).

Cela vérifie la fonctionnalité appropriée pour la suppression d'une clé existante. Quelles lois devraient régir la suppression d'une clé inexistante? Nous voulons certainement que l'arbre résultant soit le même que celui dont nous avons supprimé. On peut l'exprimer facilement:

p_delete_nonexistant = forAll aTree (\t ->
                          forAll arbitrary (\k -> 
                              k `notElem` keys t ==> delete t k == t))

De cette façon, les tests sont vraiment amusants. De plus, une fois que vous apprenez à lire les propriétés de contrôle rapide, elles servent de spécification testable par machine .

Je ne comprends pas exactement ce que signifie la réponse liée par «parvenir à la modularité grâce aux lois mathématiques», mais je pense avoir une idée de ce que l'on entend.

Découvrez Functor :

La classe Functor est définie comme ceci:

 class Functor f where
   fmap :: (a -> b) -> f a -> f b

Il ne vient pas avec des cas de test, mais plutôt avec quelques lois qui doivent être satisfaites.

Toutes les instances de Functor doivent obéir:

 fmap id = id
 fmap (p . q) = (fmap p) . (fmap q)

Supposons maintenant que vous implémentiez Functor( source ):

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

Le problème est de vérifier que votre implémentation respecte les lois. Comment procédez-vous?

Une approche consiste à écrire des cas de test. La limite fondamentale de cette approche est que vous vérifiez le comportement dans un nombre fini de cas (bonne chance en testant de manière exhaustive une fonction avec 8 paramètres!), Et donc passer des tests ne peut garantir rien d'autre que leur réussite.

Une autre approche consiste à utiliser un raisonnement mathématique, c'est-à-dire une preuve, basé sur la définition réelle (plutôt que sur le comportement dans un nombre limité de cas). L'idée ici est qu'une preuve mathématique peut être plus efficace; cependant, cela dépend de l'adaptabilité de votre programme à la preuve mathématique.

Je ne peux pas vous guider à travers une preuve formelle réelle que l' Functorinstance ci-dessus satisfait aux lois, mais je vais essayer de donner un aperçu de ce à quoi pourrait ressembler la preuve:

1. fmap id = id
   • si nous avons Nothing
     • fmap id Nothing= Nothingpar la partie 1 de la mise en œuvre
     • id Nothing= Nothingpar la définition deid
   • si nous avons Just x
     • fmap id (Just x)= Just (id x)= Just xpar la partie 2 de la mise en œuvre, puis par la définition deid
2. fmap (p . q) = (fmap p) . (fmap q)
   • si nous avons Nothing
     • fmap (p . q) Nothing= Nothingpar la partie 1
     • (fmap p) . (fmap q) $ Nothing= (fmap p) $ Nothing= Nothingpar deux applications de la partie 1
   • si nous avons Just x
     • fmap (p . q) (Just x)= Just ((p . q) x)= Just (p (q x))par la partie 2, puis par la définition de.
     • (fmap p) . (fmap q) $ (Just x)= (fmap p) $ (Just (q x))= Just (p (q x))par deux applications de la deuxième partie

"Méfiez-vous des bogues dans le code ci-dessus; je l'ai seulement prouvé correct, pas essayé." - Donald Knuth

Dans un monde parfait, les programmeurs sont parfaits et ne font pas d'erreurs, donc il n'y a pas de bugs.

Dans un monde parfait, les informaticiens et les mathématiciens sont également parfaits et ne font pas non plus d'erreurs.

Mais nous ne vivons pas dans un monde parfait. Nous ne pouvons donc pas compter sur les programmeurs pour ne faire aucune erreur. Mais nous ne pouvons pas supposer que tout informaticien qui fournit une preuve mathématique qu'un programme est correct n'a fait aucune erreur dans cette preuve. Je ne ferais donc pas attention à quiconque essaie de prouver que son code fonctionne. Écrivez des tests unitaires et montrez-moi que le code se comporte conformément aux spécifications. Rien d'autre ne me convaincra de rien.