En réalité, j'ai mal nommé mes modules : dans tous les cas on a un AST, c'est juste la structure de données pour le représenter qui change. L'encodage de Boeham-Berarducci permet de les représenter dans un langage qui ne possède pas de types inductifs.
Sinon, la différence de performance semble également dépendre de la complexité des fonctions d'interprétations impliquées. Dans les tests précédents les fonctions étaient simples : l'identité pour les litéraux et l'addition pour les nœuds. En prenant la fonction de pretty printing cela change un peu la donne :
Et encore, ici il s'agit d'une structure simple : une seule opération binaire. Sur des langages plus riches, si les transformations sur l'arbre sont un peu plus complexes qu'une simple addition, il se peut bien que cette représentation soit plus performante comme le disait Perthmâd pour l'usage qui en est fait dans Coq.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: C'est bien la peine !
Posté par kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1.
En réalité, j'ai mal nommé mes modules : dans tous les cas on a un AST, c'est juste la structure de données pour le représenter qui change. L'encodage de Boeham-Berarducci permet de les représenter dans un langage qui ne possède pas de types inductifs.
Sinon, la différence de performance semble également dépendre de la complexité des fonctions d'interprétations impliquées. Dans les tests précédents les fonctions étaient simples : l'identité pour les litéraux et l'addition pour les nœuds. En prenant la fonction de pretty printing cela change un peu la donne :
Là l'arbre a environ 8 millions de nœuds. Pour des arbres parfaits de 2000 à 500_000 nœuds, cela donne :
Et encore, ici il s'agit d'une structure simple : une seule opération binaire. Sur des langages plus riches, si les transformations sur l'arbre sont un peu plus complexes qu'une simple addition, il se peut bien que cette représentation soit plus performante comme le disait Perthmâd pour l'usage qui en est fait dans Coq.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.