Quelqu'un pourrait-il me donner plus d'informations sur le module de première classe dans Coq ? Je sais que le module dans Coq n'est pas une première classe. J'aimerais en connaître la raison et savoir si, à l'avenir, les modules de Coq pourront être de première classe.
Merci beaucoup.
Je ne suis pas certain, mais d'après ce que j'ai compris, elle provient essentiellement de deux points :
Le Coq est conservateur. Parce que certaines de ses principales applications sont dans la vérification, Coq se limite principalement à des constructions dont la sémantique est raisonnablement bien comprise.
Dans le cadre des types de dépendance, les modules de première classe sont plutôt subtils et ne sont pas entièrement compris. En particulier, quelle part du comportement de calcul/réduction des définitions souhaitez-vous voir visible en dehors d'un module ? Si rien n'est visible, alors cela est déjà disponible, sous forme de types d'enregistrement. Mais si une partie ou la totalité du comportement de réduction est visible, alors il est difficile de quantifier exactement la part qui l'est, et il est donc assez difficile d'analyser la sémantique des modules résultants.
Je ne suis pas un expert de la littérature pertinente, je peux donc me tromper sur deux points, mais j'ai l'impression que c'est la situation de base.
Prograide est une communauté de développeurs qui cherche à élargir la connaissance de la programmation au-delà de l'anglais.
Pour cela nous avons les plus grands doutes résolus en français et vous pouvez aussi poser vos propres questions ou résoudre celles des autres.
