Bonjour,
Je suis en train de garnir la bibliothèque standard de Typer pour faciliter l'écriture de programmes en Typer. En particulier hier, je voulais ajouter Eq_trans, un lemme qui exprime la transitivité de l'égalité. Voici la déclaration.
Eq_trans : (x : ?t) ≡> (y : ?t) ≡> (z : ?t) ≡> Eq x y -> Eq y z -> Eq x z; Eq_trans p q = Eq_cast (f := lambda yz -> Eq x yz) (p := q) p;
Rien de surprenant, mais Typer l'a rejeté avec Error:(SEXP) Unrecognized lambda argument. Ok. J'ai décidé d'écrire un test pour l'élaborateur. Dans mon test, la définition était acceptée. J'ai fini par découvrir que le problème est que la définition originale était trop tôt dans pervasives.typer, en particulier avant le macro multiarg_lambda.
Pourtant je n'utilise pas de lambda multiarguments directement. C'est l'élaborateur qui décide de l'émettre en désugarant le =. Ça implique qu'il y a une dépendance des pervasives vers le compileur, i.e. le compilateur s'attend à ce que ce module non seulement définisse multiarg_lambda (en fait lambda_->_, lambda_=>_ et lambda_≡>_), mais aussi lui donne une sémantique bien précise qui conserve le sens d'une définition lors du désugaring.
J'ai considéré modifier l'élaboration de = pour générer une cascade de lambda, mais ça ne règle pas le problème. Avec ce changement, le support pour multiarg_lambda est maintenant dupliqué dans l'élaborateur et dans les pervasives.
Une alternative serait de ne pas supporter ce lambda dans le compilateur, mais d'avoir un macro =, définit après multiarg_lambda, qui accepte la forme sugarée avec les arguments à gauche du =. C'est-à-dire que le compilateur n'a aucune connaissance des lambda multiarguments. Le défaut de cette approche est que le langage utilisé par les utilisateurs est de plus en plus différent de celui de l'élaborateur et ça peut avoir un impact négatif sur la qualité des messages d'erreur.
Qu'est-ce que vous en pensez? Simon
Afficher les réponses par date
Pourtant je n'utilise pas de lambda multiarguments directement. C'est l'élaborateur qui décide de l'émettre en désugarant le =. Ça implique qu'il y a une dépendance des pervasives vers le compileur, i.e. le compilateur s'attend à ce que ce module non seulement définisse multiarg_lambda (en fait lambda_->_, lambda_=>_ et lambda_≡>_), mais aussi lui donne une sémantique bien précise qui conserve le sens d'une définition lors du désugaring.
Plus ou moins. En fait, l'idée c'est que le `=` devrait lui-aussi être définit par macro-expansion mais que ce n'est actuellement pas le cas.
J'ai considéré modifier l'élaboration de = pour générer une cascade de lambda,
Tu peux trouver le code pour ça dans le revision history, avant que les macros comme `multiarg_lambda` ne fonctionnent ;-)
mais ça ne règle pas le problème. Avec ce changement, le support pour multiarg_lambda est maintenant dupliqué dans l'élaborateur et dans les pervasives.
Exactement, c'est pour ça que je l'ai enlevé du code OCaml quand j'ai mis le `multiarg_lambda`.
Une alternative serait de ne pas supporter ce lambda dans le compilateur, mais d'avoir un macro =, définit après multiarg_lambda, qui accepte la forme sugarée avec les arguments à gauche du =. C'est-à-dire que le compilateur n'a aucune connaissance des lambda multiarguments.
En fait, le sugaring du `=` est déjà pas mal générique:
x <foo> = <bar>
devient
x = lambda <foo> -> <bar>
Sans trop regarder ce qu'est <foo>.
Le problème est plus fondamental: c'est un problème de bootstrap, et il faut simplement être conscient que le langage disponible dans `btl` n'est pas le même au début qu'à la fin et donc que l'ordre est important.
Le défaut de cette approche est que le langage utilisé par les utilisateurs est de plus en plus différent de celui de l'élaborateur et ça peut avoir un impact négatif sur la qualité des messages d'erreur.
C'est effectivement un problème, mais c'est un problème inhérent à l'usage de métaprogrammation et donc mon plan est plutôt de travailler à résoudre le problème qu'à l'éviter (i.e. trouver des méthodes qui permettent de garder des messages d'erreurs en terme du code source).
Stefan