Maintenant, je pense que tout cela n'invalide en rien ma conclusion, qui est qu'il faut faire attention avec certaines supposition et que on peut se planter facilement.
En Coq t'aurais pas eu ce problème ! :-P Son système de type, qui est le plus riche que l'on puisse conférer au lambda-calcul, n'autorise pas de telles ambiguïtés.
Sinon pour gérer le maximum, et encoder des preuves sur ce dernier via des termes, avec les GADT il y a un bon exemple dans cette leçon sur les GADT dans le cours de programmation fonctionnelle avancée de Jeremy Yallop et Leo White. Cela rejoint ta question sur les GADT et type families dans mon journal sur la méthode tagless-final.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mode pinaillage :-P
Posté par kantien . En réponse au journal Cohérence des fonctions de tri. Évalué à 3.
En Coq t'aurais pas eu ce problème ! :-P Son système de type, qui est le plus riche que l'on puisse conférer au lambda-calcul, n'autorise pas de telles ambiguïtés.
Sinon pour gérer le maximum, et encoder des preuves sur ce dernier via des termes, avec les GADT il y a un bon exemple dans cette leçon sur les GADT dans le cours de programmation fonctionnelle avancée de Jeremy Yallop et Leo White. Cela rejoint ta question sur les GADT et type families dans mon journal sur la méthode tagless-final.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.