• [^] # Re: Structures non mutables performantes

    Posté par . En réponse à la dépêche Sortie de GHC 8.2.1. Évalué à 3.

    J'ai voulu cependant introduire un peu le concept et fournir une bonne ressource car je trouve que on néglige trop souvent les structures de donnée dans l'apprentissage de l'informatique, et on néglige encore plus les structures non mutables qui offrent des propriétés très intéressantes.

    C'est dommage que les structures persistantes soient négligées : la persistance, c'est le bien ! :-)

    Dans leur ouvrage Apprendre à programmer avec OCaml, Sylvain Cochon et Jean-Christophe Filliâtre consacrent un paragraphe sur l'utilité et les avantages de la persistance :

    Les intérêts pratiques de la persistance sont multiples. De manière immédiate, on comprend qu'elle facilite la lecture du code et sa correction. En effet, on peut alors raisonner sur les valeurs manipulées par le programme en termes « mathématiques », puisqu'elles sont immuables, de manière équationnelle et sans même se soucier de l'ordre d'évaluation. Ainsi est-il facile de se persuader de la correction de la fonction append précédente une fois qu'on a énoncé ce qu'elle est censé faire (i.e append l1 l2 construit la liste formée des éléments de l1 suivis des éléments de l2) : une simple récurrence sur la structure de l1 suffit. Avec des listes modifiables en place et une fonction append allant modifier le dernier pointeur de l1 pour le faire pointer sur l2, l'argument de correction est nettement plus difficile. L'exemple est encore plus flagrant avec le renversement d'une liste. La correction d'un programme n'est pas un aspect négligeable et doit toujours l'emporter sur son efficacité : qui se soucie en effet d'un programme rapide mais incorrect ?

    Le code de la fonction append en question est :

    let rec append l1 l2 = match l1 with
     | [] -> l2
     | x :: xs -> x :: append xs l2

    et effectivement un simple raisonnement par récurrence sur la structure de l1 suffit à prouver sa correction. On peut même facilement formaliser un tel résultat dans un assistant de preuve comme Coq pour certifier le code. Là où avec des structures impératives se sera une toute autre paire de manches.

    Ils continuent en prenant un exemple de problématiques de backtracking : parcourir un labyrinthe pour trouver une sortie. La position dans le labyrinthe est modélise par un état e dans un type de donnés persistants. On suppose qu'on a une fonction is_exit qui prend un état et renvoie un booléen pour savoir si on est à une sortie. On a également une fonction possible_moves qui renvoie la liste de tous les déplacements possibles à partir d'un état donné et une fonction move pour effectuer un tel déplacement. La recherche d'une sortie s'écrit alors trivialement à l'aide de deux fonctions mutuellement récursives :

    let rec find e =
     is_exit e || try_move (possible_moves e)
    and try_move e = function
     | [] -> false
     | d :: r -> find (move d e) || try_move e r

    Avec des structures impératives il faudrait, après chaque déplacement, annuler celui-ci avant d'en faire un autre : ce genre de code est un vrai nid à bugs.

    let rec find () =
     is_exit () || try_move (possible_moves ())
    and try_move = function
     | [] -> false
     | d :: r -> (move d; find ()) || (undo_move d; try_move r)

    ici il faudrait s'assurer que la fonction undo_move annule bien correctement le déplacement d effectué via l'appel à move d. Non seulement cela complique le code, mais en plus cela ouvre la porte à des erreurs potentielles.

    Dans le même ordre d'idées, on peut prendre le cas de la mise à jour d'une base de données. Avec un structure de donnés modifiables, on aurait un code du style :

    try
     (* effectuer l'opération de mise à jour *)
    with e ->
     (* rétablir la base dans un état cohérent *)
     (* traiter ensuite l'erreur *)

    Avec un structure persistante, c'est plus simple et moins propice aux bugs.

    (* on stocke la base dans une référence *)
    let bd = ref base_initale
    try
     bd := (* opération de mise à jour de !bd *)
    with e ->
     (* traitement de l'erreur *)

    Ici la mise à jour construit une nouvelle base qui est ensuite affectée à l'ancienne via une opération atomique qui ne peut échouer. Si il y a une erreur lors de l'opération de mise à jour alors l'ancienne base n'a pas été modifiée et il n'est pas nécessaire de la remettre dans un état cohérent avant de traiter l'erreur proprement dite.

    Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.