Lazi

Les types

Résumé

Nous expliquons pourquoi la définition de Lazi nécessite d'utiliser des types et classes évolués. Nous faisons un point rapide sur la notion de type dans les divers domaines. Nous expliquons pourquoi il existe une grande diversité de notions d'objets en informatique et comment il est possible de les unifier. Enfin nous montrons ce qui est déjà réalisé en Lazi du point de vue des types.

Pourquoi la définition de Lazi nécessite les types et classes

lazi.1.0 est une fondation mathématique définie formellement en lazi.0.1. Définir une fondation mathématique nécessite de définir des structures et processus (comme le processus de vérifier si une preuve est valide). C'est donc très proche d'un programme informatique et comme tout programme un peu évolué nous avons besoin de la notion d'objet. En fait, en lazi, une mathématique est un type.

La notion de type dans les divers domaines

Que ce soit dans la vie courante, en informatique ou en mathématique nous avons besoin de classer les différentes choses qui nous entoure. Appelons ce classement le "typage". Par exemple en langage courant nous aurons le type "chaise", en mathématique nous aurons le type "groupe abélien" (appelé "structure algébrique") et en informatique nous aurons la classe "chaise".

Dans tous les domaines nous avons besoin de reconnaître si quelque chose est d'un certain type, mais il existe ici une différence importante entre l'informatique traditionnelle et le reste : si notre univers était comme notre informatique traditionnelle, chaque objet aurait une étiquette avec son type écrit dessus. En effet, en langage courant et en mathématique on détermine le type d'une chose par le teste de propriétés sur la chose (c'est pourquoi les structures algébriques comprennent des axiomes).

La notion de type et classe en informatique traditionnelle

En informatique la notion de type a plusieurs fonctions :

  • se procurer des informations sur une donnée (par exemple pour savoir quelle fonction de sérialisation lui appliquer)
  • vérifier qu'une entité a les propriétés attendues (par exemple on déclare que la fonction de sérialisation retourne un type "chaîne de caractères" et le compilateur vérifie cette propriété).
Les langages informatiques diffèrent dans le fonctionnement du typage par :
  • un langage spécifique d'expression des types
  • une manière différente d'exprimer les caractéristiques d'un type
  • une manière différente d'exprimer les relations entre les types (l'héritage)
Dans tous les cas le compilateur du langage implémente en dur la notion de type.

Que faudrait-il pour unifier la notion de type ?

L'expression des propriétés :

La fonction de vérification des propriétés (que l'on retrouve en mathématique par les axiomes des structures) peut être d'une complexité sans limite. C'est pourquoi, tant que l'on n'utilisera pas des expressions mathématiques, on sera voué à de perpétuelles évolutions de langage. Pour arriver à utiliser des expressions mathématiques il faut renoncer à ce que la vérification des contraintes par le compilateur soit sans échec. Cela peut sembler une limitation, mais en fait en élargissant et en mathématisant l'expression des contraintes cela offre la liberté de rester confiné dans les systèmes d'expressions traditionnelles (logiquement mais aussi syntaxiquement) tout en permettant d'aider le compilateur en fournissant des morceaux de preuves pour qu'il puisse vérifier des contraintes plus sophistiquées.

L'expression des types :

Bien que l'on retrouve dans le typage les mêmes besoins que dans la manipulation des données (assignation, fonction, vérification de contraintes) les langages informatiques traditionnels possèdent chacun un langage spécifique pour l'expression des types. Par exemple si on veut donner un nom à un type, on n'utilisera pas la même syntaxe que pour donner un nom à un nombre ("type List3D a = [(a,a,a)]" et "x=2" en Hakell).

On voit donc qu'un langage informatique traditionnel fournit en fait deux langages : un pour les données et un pour les types. Haskell va même jusqu'à commencer un troisième niveau avec les kinds.
relecture : j'en suis là
Pour unifier l'expression des types il est nécessaire d'unifier le langage de typage et le langage sur les données, et donc de voir les types comme des données. Pour cela il est nécessaire de renoncer à ce que toute donnée possède un type unique (sinon on a une boucle infinie puisque les types sont des données). Ce renoncement peut paraître une contrainte, mais cela n'empêche pas d'exiger que pour certain bloc de code que les types soit déclarés.

L'expression du contenu et des relations entre les types :

En informatique traditionnelle chaque compilateur/interpréteur implémente en dur un fonctionnement. Si on utilise la vision mathématique des structures il apparaît que la complexité des relations entre les types est sans limite. Par exemple on peut vouloir y ajouter des lois, voir une mathématique. C'est pourquoi une unification des types doit se passer d'une implémentation fixée du contenu et des relations entre types, et donc aussi une implémentation fixée par le compilateur. Cela nécessite un niveau supplémentaire d'abstraction. Remarquons que le chemin vers cette abstraction est déjà entamé par Haskell avec les monades, par exemple les exceptions sont implémentées par une librairie en Haskell et par le compilateur en C++).

L'implémentation en dur permet la rapidité de compilation et l'optimisation du code. Comment traduire rapidement le source en code optimisé sans implémentation en dur des types ?

Pour cela le code source n'est plus la représentation de l'exécutable mais un code interprété qui produit lui-même l'exécutable. Ce code peut faire appel à des librairies de manière à accélérer certaine tâches. L'ensemble des librairies disponibles n'est pas fixé car c'est la vérification des contraintes mathématiques qui fourni la validité de celles-ci. Il n'y a plus alors de compilateur opaque fournissant une interface fixée, mais un compilateur ouvert, régi par des lois et extensible.

Remarquons que cela n'augmente pas outre mesure la complexité de la production de code, par exemple pour écrire du source en C++ il suffit d'entourer le code source de balises indiquant que l'on veut transformer du source C++ en programme.

Les types utilisés dans la définition de la fondation mathématique Lazi

Tout le système de typage est défini en lazi (principalement dans 03-types.def.lazi), les seuls éléments intégrés dans l'interpréteur sont optionnels : des notations et des optimisations de calcul.

Un exemple simple

La définition du type uniDictT :


/*
Type des dictionnaires, t est le type des valeurs.
*/
$Def uniDictT =
  $O($O[t])[
    domain = $F i → isDict i ∧b 
      // les valeurs doivent avoir le type demandé
      ∀l x/dictValues i; x ∈t t
    ,
    equal = $F i,j →
      wordListEqual ( dictEntries i , dictEntries j ) ∧b 
      listAnd ( dictValues \ dict2Map (t .o'equal) i j )
  ,
    object = $F i → dictMap (t .o'object) i
  ,V
    map = $F i,f → dictMap f i
  ,
    fold = $F i,f,r → listFold ($F r2,$T[k,v] → f r2 v) r i
  ]

L'assignation du type au nom "uniDictT" se fait comme pour tout autre assignation : par $Def.
Voyons ce que signifie "$O" :

Pour cela voyons d'abord les dictionnaires ($D) :
Un dictionnaire est une liste de paire (mot,valeur). C'est donc une manière standard de stocker des informations quelconques. Nous avons une syntaxe simplifiant l'écriture des dictionnaires, par exemple
$D[ values = srT, x = wordT, d = deductionT .o'addGVar x ]
attribue au mot "values" la valeur srT etc.
Comme un dictionnaire est une simple liste, il n'est pas possible dans un dictionnaire de faire référence à la valeur d'une autre entrée, par exemple dans $D[ a = 1, b = a + 2 ], b ne vaut pas 1 + 2 et en fait n'a pas de sens.
Un objet peut faire référence à lui-même et à d'autre objets, pour cela un objet est une fonction qui prend en argument un objet et retourne un dictionnaire. Voir le code source 02-tools-2.def.lazi section "Structure Objet" pour la définition des objets.
Voyons ce que signifie "$O($O[t])" :
uniDictT est un objet qui prend en référence un objet contenant la clé "t", "t" devient alors accessible dans la définition de l'objet. Ici t est le type des valeurs du dictionnaire. On aurait pu définir directement
$Def uniDictT = $F t → $O[ ... ]
mais ce mode de définition pose un problème : dans ce cas uniDictT n'est pas un type mais une fonction retournant un type. Le passage de paramètre par objet nous permet un fonctionnement plus générique pour manipuler les types.
Voyons ce que signifie "domain = ... " :
Le système de typage en Lazi est comme celui en mathématique ou en langage courant : il ne requiert pas que chaque donnée soit d'un certain type prédéfini. C'est au type de vérifier si une donnée est de ce type, et c'est le rôle de la fonction domain. Ici elle véfifie que l'instance présumée "i" est un dictionnaire et que chaque valeur est de type t (la notation "∀l" est une boucle "for" sur la liste). La fonction "domain" n'est appelée que quand cela est nécessaire, c'est à dire que l'on peut très bien manipuler des instances sans d'abord vérifier le domaine car on peut être déjà assuré de leurs appartenance.
Voyons ce que signifie "equal = ... " :
C'est une fonction d'égalité entre deux instances. Bien qu'en théorie pas totalement indispensable, tout type lazi possède une fonction égalité car l'égalité est une relation très importante.
Voyons ce que signifie "object = ... " :
Quasi systématiquement une instance représente quelque chose, autrement dit c'est en général l'objet de l'instance que de représenter quelque chose. Par exemple l'objet d'une preuve est de prouver quelque chose donc son objet est l'énoncé déduit, l'objet d'une représentation de formule est une formule. Ici l'objet d'une instance de uniDictT est le dictionnaire des objets des valeurs.
Dans certains cas il n'y a pas d'autre objet que de représenter la chose elle même, par exemple pour wordT on aura
object = $F i -> i
Les entrée map et fold correspondent à des fonctions spécifiques aux type. Elles prennent en premier argument l'instance du type. C'est un comportement systématique qui est utile dans les surcharges.

L'utilisation du type uniDictT :


t2 = uniDictT ∪od $D[ t = formulaT ]


$D[ t = formulaT ] est un dictionnaire permetant de passer l'argument "t" qui est le type en paramètre.
∪od permet d'unir un objet et un dictionnaire.

Un exemple de typage dynamique

Cet exemple illustre les particularités dynamiques des types Lazi. Ces aspects dynamiques sont nécessaires pour définir simplement la fondation lazi.

Ici nous définissons dynDictT qui contrairement à uniDictT attribut un type qui peut être différent pour chaque entrée du dictionnaire. Les types des entrées sont déterminés par une fonction (dtf, qui prend en argument une instance de dynDictT) car ils peuvent dépendre des valeurs du dictionnaire :


$Def dynDictT = 
  $O($O[dtf])[
    domain = $F i →
      isDict i ∧b
      wordListEqual ( dictEntries (dtf i) , dictEntries i ) ∧b
      listAnd \ dictValues \ dict2Map isInstance i \ dtf i
  ,
    equal = $F i,j → listAnd \ dictValues \ dict2Map apply ( dict2Map ( $F t → t .o'equal ) (dtf i) i ) j
  ,
    object = $F i → dict2Map ( $F t,v → t .o'object v ) (dtf i) i
  ,
    // Notons que f a pour premier argument le type de la valeur.
    map = $F i,f → dict2Map ( $F t,v → f t v ) (dtf i) i
  ,
    // Notons que f a pour premier argument le type de la valeur.
    fold = $F i,f,r → listFold ($F r2,$T[k,v] → f ((dtf i) .o k) r2 v) r i
  ]

Nous ne documenterons que sa particularité : la fonction "domain" :

On vérifie que i est un dictionnaire, puis qu'il y a égalité entre les entrée de l'instance et du dictionnaire des types "dtf i", puis que les valeurs du dictionnaire ont le bon type.

L'utilisation du type dynDictT :


dynDictT ∪o 
    $O($O[deductionT])[
      formulaT = deductionT .o'formulaT
    ,
      dtf = $F $D[vj] → $D[ 
        dom = formulaT, 
        tr = formulaT, 
        // La variable doit ne pas déjà être utilisée.
        vj = wordChoosedT ∪od $D[ filter = listHasNotWord \  deductionT .o'gvarList ],
        proof = deductionT .o'addGVar vj, 
        j = anythingT 
      ]
    ]

L'objet fournissant la fonction dtf prend lui-même un paramètre "deductionT". On définit dans cet objet "formulaT" par confort car on a besoin plusieurs fois de la valeur. dtf prend en argument l'instance ($D[vj]) pour n'utiliser que la valeur de la clé "vj", elle retourne le dictionnaire des types, on voit que le type pour la clé "proof" utilise la valeur vj.
Remarquons que le type pour l'entrée j est particulier puisque anythingT est vérifié pour toute chose.

Un exemple d'héritage

Comme les types sont des objets (au sens lazi), que les objets sont fait pour avoir des références à d'autres objets, il n'y a pas de mécanisme particulier pour l'héritage, l'union d'objet suffit, par exemple :


$Def eDeductionT = 
  $Let parent = dynPairT ∪o $O($O[deductionT])[
      eventT = deductionT .o'eventT,
      t1 = eventT,
      t2f = $F ev → eventT .o'object ev
    ]
  ,
  parent ∪o
  $O($O[deductionT,eventT,map])[
      // Pour obtenir l'objet de la déduction, on traduit la sous-déduction. Cela implique que l'on puisse traduire les événements sans ordre. debug! : adapter le code et la doc à cette contrainte.
      object = $F $T[ev, d] → deductionT .o'object \ eventT .o'translateThis ev d 
    ,
      mapFormulas = $F i,f → map i $F t,j → t .o'mapFormulas j f 
    ,
      mapDeductions = $F i@$T[ev, d],f → 
        $T[ eventT .o'mapDeductions ev f, f (eventT .o'object ev) d ]
    ,
      // Traduit tous les événements de l'instance, suivant le critère p. Voir http://url.bobu.eu/g3H
      translateEvents =  $F i@$T[ev, d],p → eventT .o'translate ev p d
  ]

Le type eDeductionT a pour type parent le type défini localement par "$Let parent = ...". Le type "parent" est uni à la partie spécifique d'eDeductionT par
parent ∪o $O($O[deductionT,eventT,map])[ ... ]
On remarque que eDeductionT utilise trois paramètres : deductionT, eventT et map.

Un exemple de définition de fonction virtuelle


translate = callVirtual 'translate
    $F i@$T[tn,j],p  → 
        if(p i; 
           translate (getType tn .o'translateThis j) p;  
           mapDeductions i $F deductionT,k → deductionT .o'translate k p) 

Dans cet exemple repris de l'intérieur de la définition d'un type, on définit une fonction virtuelle : si la fonction n'est pas définie par l'objet enfant alors la fonction "$F i@$T[tn,j],p → ..." est retournée.

Un système de fonction virtuelle pure existe aussi.

La vérification des contraintes

Un grand atout des système de typage est d'éviter les bugs par vérification du compilateur.
Cette partie n'est pas encore implémentée en Lazi. Elle sera basée sur des expressions mathématiques, des preuves (la pluspart du temps automatiquement générées). Il sera donc possible d'exprimer toutes formes de contraintes.