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
Afficher les réponses par date
Ça c’est pile dans mes cordes. Utiliser un calculus bien défini, le modifier et prouver des propriétés … miam miam ;-)
Je suis motivé pour participer.
Vincent
On Apr 16, 2016, at 11:40 AM, Stefan Monnier monnier@iro.umontreal.ca wrote:
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
Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer
Ça c’est pile dans mes cordes. Utiliser un calculus bien défini, le modifier et prouver des propriétés … miam miam ;-)
C'est bien à peu près ça.
Idéalement il faudrait aussi quelques analyses de performance, soit avec de vrai benchmarks, soit avec des arguments "analytiques/symboliques".
Je suis motivé pour participer.
Tu peux commencer par lire "A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi", http://www-users.cs.umn.edu/~gopalan/papers/suspension-calculus.pdf
Cet article couvre les 2 "concurrents" principaux (le système principal présenté et le λσ). Il y manque par contre une version limitée antérieure du "Suspension Calculus", mais si non ça couvre assez bien le sujet.
Stefan