Le compilateur pour le type dépendant est-il beaucoup plus difficile qu'un interprète?

J'ai appris quelque chose sur l'implémentation de types dépendants, comme ce tutoriel , mais la plupart d'entre eux implémentent des interprètes. Ma question est, il semble que l'implémentation d'un compilateur pour le type dépendant soit beaucoup plus difficile qu'un compilateur, car vous pouvez vraiment évaluer les arguments de type dépendant pour la vérification de type.

Donc

• Mon impression naïve est-elle juste?
• Si c'est le cas, des exemples / ressources sur l'implémentation d'un langage à vérification statique prenant en charge le type dépendant

C'est une question intéressante! Comme le suggère la réponse d'Anthony, on peut utiliser les approches habituelles pour compiler un langage fonctionnel non dépendant, à condition d'avoir déjà un interprète pour évaluer les termes pour la vérification de type .

C'est l'approche adoptée par Edwin Brady. Maintenant, c'est conceptuellement plus simple, mais cela perd les avantages de vitesse de la compilation lors de la vérification de type. Ce problème a été résolu de plusieurs manières.

Tout d'abord, on peut implémenter une machine virtuelle qui compile les termes en octet-code à la volée pour effectuer le contrôle de conversion. C'est l'idée derrière vm_computemise en œuvre dans Coq par Benjamin Gregoire . Apparemment, il y a aussi cette thèse de Dirk Kleeblatt sur ce sujet précis, mais en bas du code machine réel plutôt que d'une machine virtuelle.

Deuxièmement, on peut générer du code dans un langage plus conventionnel qui, lors de l'exécution, vérifie toutes les conversions nécessaires pour vérifier par type un programme typé de manière dépendante. Cela signifie que nous pouvons utiliser Haskell, par exemple, pour effectuer une vérification de type d'un module Agda. Le code peut être compilé et exécuté, et s'il accepte, alors le code dans le langage de type dépendant peut être supposé être bien typé (à l'exception des erreurs d'implémentation et de compilation). J'ai d'abord entendu cette approche suggérée par Mathieu Boesflug .

$^*$

La thèse de doctorat d' Edwin Brady explique comment construire un compilateur pour un langage de programmation typé de manière dépendante. Je ne suis pas un expert, mais je dirais que ce n'est pas extrêmement difficile que d'implémenter un compilateur de type System F. Beaucoup de principes sont assez similaires et certains sont les mêmes (par exemple, compilation de supercombinateurs.) La thèse couvre de nombreuses autres préoccupations.