Bonjour les amis,
Pour faire la vérification et l'inférence des types, il faut implémenter l'opération de substitution d'une variable par une expression.
Cette opération devrait être faite de manière paresseuse, principalement de manière à pouvoir combiner plusieurs substitutions (de sorte à ne faire qu'une traversée de l'expression (où le cas Var coûtera O(N)) plutôt que de faire N traversée (où le cas Var ne coûte que O(1))).
Cela se fait normalement par l'intermédiaire des noeuds "Susp".
Je regardait donc comment étendre subst.ml pour ça. En gros j'ai trouvé deux approches, une (le suspension-calculus) semble efficace mais un peu compliquée/inélégante/nonintuitive et l'autre (le λσ calculus of explicit substitutions) semble élégante et intuitive mais moins efficace.
En essayant de bien comprendre comment fonctionne le suspension-calculus, j'ai trouvé une autre solution, une sorte de restriction du λσ qui reste élégante et intuitive mais qui correspond en fait de manière assez proche à certaines versions du suspension calculus.
Je compte écrire un petit papier là-dessus, et pour pas perdre trop de temps là dessus, j'aimerais l'envoyer tout soudain (e.g. fin du mois).
Qui de vous serait intéressé à participer à cet article?
Stefan