Lazi

Quelle est la structure du système de vérification des types ?

Contexte

À partir des objectifs visés, il est nécessaire d'avoir déjà une vision globale du fonctionnement de la vérification des types.

Question

Quelle est la structure du système de vérification des types ?

Étude

Qu'est-ce qu'une déclaration de type ?

Actuellement le code source contient des événements "$Def" et "$Nota".

On peut voir la déclaration d'un type comme une déduction spéciale qui prend en paramètre une phrase à démontrer.

Les déclarations de types sont séparées et constituent une preuve à vérifier, dans la mathématique modifiées par les événements "$Def" et "$Nota".

Le code source comme objet mathématique

La déclaration d'un type est une formule qu'il faut démontrée, il faut donc que le code source soit lu pour être introduit en tant qu'une chose en argument d'une fonction.

Il faut donc une nouvelle fonction de lazi-translate, qui lit des fichiers sources pour les transformer en un argument d'une fonction lazi. C'est l'interprétation de cette fonction avec cet argument qui constitue la vérification des types.

Utilisation des types précédents

Le système traditionnel de vérification des types utilise les types des éléments (variables, fonctions etc) rencontrés dans une procédure pour vérifier le type.

Ce fonctionnement peut être aussi utile avec Lazi: cela consiste ici à utiliser les vérités déjà démontrées pour construire la preuve de la vérité à prouver.

Réponse

Voir l'étude.