Re: Structures non mutables performantes

Heureux de voir que j'avais bien compris le principe des shared_ptr. Je suppose qu'en C++ la nécessité de recourir au weak_ptr doit venir du côté mutuellement récursif des deux type 'a t et 'a data.

Note, si mon benchmark n'est pas faux (j'ai des doutes quand je manipule des effets de bords de ce type), alors :

• modifier un vecteur non mutable (i.e.: créer une copie) c'est super rapide sur des petits vecteurs, mais cela devient linéairement lent avec la taille du vecteur qui augmente
• modifier un vecteur avec ta technique c'est en O(1)
• modifier un vecteur "vraiment" mutable vue de l’extérieur est un poil plus rapide.

Je suis étonné qu'une copie complète soit plus rapide sur de petits vecteurs, j'aurais parié le contraire (je suis surtout étonné par l'écart de temps : 4 ms vs 30 ms). En revanche, le coût constant si on n'enchaîne que des update est bien conforme à mes attentes. Néanmoins, le code de ta fonction update est « erroné », en OCaml c'est celui-ci :

let set pa i v =
 let a = reroot pa in
 let old = a.(i) in
 a.(i) <- v;
 let res = ref (Arr a) in
 pa := Diff (i, old, res);
 res

Il faut d'abord se rebaser sur le « véritable » vecteur représentant ton tableau, faire une mise à jour à l'index, construire une référence sur le vecteur mis à jour et modifier l'ancien tableau persistant pour le voir comme un Diff du nouveau, puis enfin retourner le nouveau tableau. Ceci dit, cela ne doit pas changer les invariants de la structure par rapport à ton code. Chaque tableau persistant est, dans le fond, une classe d'équivalence¹ au sein du type 'a data puis ton code et celui en OCaml ne renvoie simplement pas le même élément de la classe en question.

Merci pour la discussion, je me suis amusé.

À mon tour de te remercier pour ta très intéressante dépêche. La partie sur l'introduction du typage linéaire (dont je suivrai l'évolution avec intérêt) m'a enfin décidé à acheter certains ouvrages de Jean-Yves Girard² : j'y pensais depuis longtemps mais je repoussais toujours l'achat (sans raison aucune à vrai dire). Je me suis acheté la transcription de ses cours de Logique, Le Point Aveugle en deux tomes, ainsi que son dernier livre Le Fantôme de la transparence. Si les deux premiers livres sont très techniques et théoriques, le dernier est, quant à lui, un ouvrage plus grand publique de « vulgarisation ». J'attends toujours la livraison de ses cours, mais j'ai en revanche reçu ce matin Le Fantôme de la transparence dans lequel je peux lire, à mon grand plaisir, en conclusion de sa préface de présentation :

Le principal bénéficiaire de cette visite non guidée aura été l'auteur, tout surpris d'y trouver matière à de futurs développements techniques. Et de découvrir la surprenante adéquation du kantisme — au sens large — à la logique contemporaine. Ce qui n'est pas très étonnant après tout : que veut dire « raison pure », sinon logique ?

Le graissage est bien entendu de moi :-). La chose m'étonne moins : étudiant, je m'étais inscrit au master Logique Mathématique et Fondements de l'Informatique parce que j'étais déjà kantien et que je voulais approfondir mes connaissances en logique. Puis lorsque Jean-Louis Krivine m'enseigna la lambda-calcul typé, le système F et la correspondance de Curry-Howard, ma première réaction fût : c'est comme la théorie kantienne des catégories dans la Critique de la Raison Pure³ ! ;-) Pour Kant (pour faire court et en employant des termes actuels), le type du rapport de cause à effet c'est la forme des jugements hypothétiques, forme qui est le type des fonctions en programmation fonctionnelle. \o/

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