Lazi

Quels sont les extensions nécessaires à la vérification des types ?

Contexte

La vérification des types nécessitent:

  • de pouvoir exprimer des propriétés sur des choses,
  • de pouvoir généralement démontrer ces propriété,
  • de lire du code source pour intégrer les événements et vérifier les déductions.

Question

Quels extensions a-t-on besoin pour réaliser tout cela ?

Étude

Pour voir le code source en tant qu'une chose mathématique

Il faut une extension "definition" pour voir les définitions comme des événements.

Il faut que la représentation du code source soit relativement fidèle. On peut se passer de la représentation des fonctions pour l'instant, mais on a besoin d'extensions pour:

  • représenter les fonctions (extension de type "notation")
  • peut être pour représenter "$Let" (extension de type "notation")
  • pour représenter les mots

Pour l'expression des propriétés

Voir des cas d'études.

On voit que l'on a besoin d'une grande expressivité, celle classique avec les quantificateurs, implications etc.

Donc on a besoin des extensions aux minimum:

  • forAll
  • imply
  • and

Et tant qu'à faire il me semble bien d'ajouter:

  • exists
  • or

Pour démontrer ces propriétés

L'extension "proveType"

Elle prend une phrase mathématique et cherche à la prouver. Elle permet d'avoir un message suffisament clair en cas d'erreur. Elle peut utiliser des vérités d'autres déclarations de types. Il faut donc qu'il soit possible de stocker ces vérités.
Probablement qu'il faut stocker ces vérités à part. Pour stocker des vérités dans la mathématique, il faut que ce soit un événement.

Réponse

Il y a besoin d'un bon nombre d'extension, voir l'étude.