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