Études-Mathématique/unionT et fonction de mapping

From Lazi wiki
Jump to: navigation, search

Question

Si on veut créer une fonction de mapping pour un unionT:

  • il serait pratique que le type constituant n'ait pas à connaître le nom de son type, et que la construction $T[nom du type, valeur mappée] soit faite par l'unionT pour la partie création de la paire.
  • il serait pratique de pouvoir définir un comportement par défaut, peut être la fonction identité.

Comment implémenter cette fonctionnalité ?

Étude

Principe d'ouverture

Il ne faut pas ajouter des présupposés artificiels, comme par exemple supposer qu'une type est un constituant d'une union alors qu'il peut ne pas l'être.

Mais il y a des cas où le type doit posséder des connaissances sur l'unionT parent:

  • Pour les traductions des déductions, la fonction de traduction d'une déduction peut en retourner une autre.
  • La fonction formWordT .o'replaceTypedWords doit retourner une formule, s'il n'y a pas eu de remplacement alors il faut construire la formule à partir du mot.

On peut donc diviser les types en deux catégories:

  • les constituants : ils doivent avoir des informations sur une union qui les contient.
  • les a-constituants  : ils peuvent être utilisés normalement sans être un constituant.

Réponse

unionT ajoute des informations dans les types constituants:

  • l'unionT parent
  • le nom du type pour l'unionT
  • des fonctions utilitaires

Pour les types constituants on peut prévoir des fonctions relatives à l'unionT.