D IAGRAMMES E. T OURATIER Étude du typage dans le système de calcul scientifique Aldor Diagrammes, tome 42 (1999), p. 3-113 © Université Paris 7, UER math., 1999, tous droits réservés. L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright. Article numérisé dans le cadre du programme Numérisation de documents anciens mathématiques http://www.numdam.org/ DIAGRAMMES VOLUME 42 ,1999 ETUDE DU TYPAGE DANS LE SYSTEME DE CALCUL SCIENTIFIQUE ALDOR w E. Touratier Introduction Apparu vers le milieu des années 70, le langage de calcul formel Axiom [13], initialement Scratchpad, faisait montre de caractéristiques peu communes dans l'univers des langages de calcul formel, comparativement aux langages contemporains ou ultérieurs tels Reduce, Macsyma, Mathematica, Maple, Magma, Mupad. Aldor est le successeur direct du langage Axiom. Comme tous les langages de calcul formel, il autorise la manipulation des objets de base du calcul mathématique : entiers, flottants, booléens, chaînes de caractères, etc., en programmation impérative ou fonctionnelle. n : Integer := 2 est une affectation de variable, n : Integer == 2 est une définition de constante, carre(n : Integer) : Integer == n*n est une définition de fonction, (*> Thèse de Mathématiques et Informatique, préparée et soutenue à lTJniversité de Limoges (U.F.R. des Sciences - L.A.C.O.). c a r r e ( 2 ) est une application de fonction. On dispose également en Aldor des types de "l'algèbre" : Monoid, Ring, F i e l d , etc., et : R : Ring == Integer ou R : Field == Float sont des expressions licites dans le langage. On définit de même des fonctions : Polynôme(R : Ring) : Ring == ... ce qui permet de construire le nouveau type Polynôme ( I n t e g e r ) . Si l'on peut dire que 2 est de type I n t e g e r ou que JC2+JC + 1 est de type Polynôme ( I n t e g e r ) , on peut aussi dire en Aldor que Integer et Polynôme ( I n t e g e r ) ne sont pas des types atomiques et qu'en plus ils ont euxmêmes un type. Il n'y a pas de différence fondamentale entre 2 , I n t e g e r et Polynôme(Integer) . Le trait le plus typique de ce langage réside donc dans son système de types, d'une très grande richesse expressive. Il hérite des travaux menés sur les spécifications algébriques [9] dont il reprend les concepts. Notre étude portera donc sur le système de types d'Aldor [19]. On abordera l'aspect standard du typage d'Aldor en tant que langage fonctionnel, avec les notions de typage par déclaration ou par inférence, de constructeur de types de fonctions -» ou de types de uplets (.,...,.), etc. On verra que pour expliquer le typage de certaines expressions du langage, appelées domaines et catégories, on a besoin de l'approche du typage par les "types abstraits algébriques". Ceci nous permettra de justifier d'une part l'existence de catégories pour typer les domaines et d'autre part le fait que les catégories typent d'autres catégories, par une relation de satisfaction entre types que l'on définira. Pour cette étude du système de types, on préférera aux spécifications algébriques la théorie des esquisses. Développée depuis 1968 par Ehresmann [8], la théorie des esquisses peut s'utiliser pour formaliser aussi bien la logique classique [10, 11] que des problèmes plus circonscrits de l'informatique [2]. A la lumière de travaux précédents [6, 7, 17], les esquisses et leurs généralisations se sont révélées être un bon formalisme pour l'étude des langages informatiques. L'objectif poursuivi dans ce travail est unique : déterminer une esquisse associée au langage de calcul formel Aldor. Celle-ci devra traduire la syntaxe du langage ainsi que toutes les caractéristiques de son système de types : construction, relation de satisfaction dont l'héritage n'est qu'un cas particulier, etc. Dans une première partie, on traitera de manière générale du typage dans les langages informatiques. Puis on mettra en évidence l'originalité du typage d'Aldor tout en essayant de donner les raisons pour lesquelles ce choix aurait été opéré par les concepteurs du langage. Ceci sera fait de manière informelle, repris par la suite à l'aide des procédés de construction de la théorie des esquisses. Après avoir rappelé les notions essentielles de la théorie des esquisses, on pourra débuter la construction de l'esquisse associée à Aldor proprement dite. Elle repose sur la structure de catégorie cartésienne fermée, base de tous les langages fonctionnels. Une fois posée la structure de base du langage, on définira précisément ce qu'est le type d'une expression Aldor, selon sa nature et sa présentation. Il sera ensuite possible de donner toutes les règles de satisfaction de types, relation qui nous permettra de justifier tous les mécanismes de typage d'Aldor. On verra en conclusion que la notion de typage est insuffisante pour exprimer la validité d'une expression dans le langage Aldor et qu'il faut y ajouter la notion de nature. On pourra consulter ce document totalement ou partiellement selon ses centres d'intérêt en se référant au plan suivant : • Chapitres 1 et 2 : le typage en général et celui d'Aldor en particulier, • Chapitre 3 : rappels sur la théorie des esquisses, • Chapitres 4, 5 et 6 : construction de l'esquisse depuis l'application de fonction jusqu'à l'inférence de types, • Chapitre 7 : retour sur quelques propriétés du typage à la lumière du point précédent. Chapitre 1 Typage Le typage dans les langages de programmation a été introduit à l'origine pour répondre à des besoins de vérification dans la formation des termes: il fallait au moins s'assurer que le profil des opérateurs était respecté. Mais le typage aide aussi à la compréhension des programmes. Un langage de programmation est en effet un outil qui permet de produire un programme en langage machine (ce qu'on appelle également le "code-objet") à partir d'un programme "code source", assorti d'un ensemble de commentaires écrits par et pour le programmeur. Lorsque ces commentaires ne sont pas traités par la machine, on parle de langage de bas niveau et dans ce cas la compilation d'un programme source consiste à étudier la partie écrite en code et à "oublier" les commentaires. Dans un langage dit de haut niveau, une partie des commentaires peut être vérifiée par la machine et c'est précisément cette partie que l'on désigne par le terme typage. Dans cette classe de langages de haut niveau, on peut encore distinguer les langages selon la richesse de leur système de types. 1.1 Les langages fonctionnels Pour la plupart des langages fonctionnels, comme CAML par exemple, un système de t y p e s est une classe de formules d'un certain langage, ces formules étant destinées à exprimer des propriétés des termes du langage de programmation. Les systèmes de types sont en général constitués de types 1.1. Les langages fonctionnels atomiques (nat, bool, string . . . ) , de règles de formation des types et de règles de typage des expressions. Les règles de formation vont servir à introduire des connecteurs de types ; la plupart des langages typés disposent des constructeurs produit ou somme de types et du connecteur —K Pour former les types du système de types, on considère les termes du premier ordre sur la signature formée des constructeurs et des constantes de types. Exemple 1 : Le système de types de CAML [18] CAML dispose de constructeurs de types binaires (—>•,*), unaires ( l i s t ) , ainsi que de constantes de types (ou types atomiques : b o o l , n a t , . . . ) , de vaxiables de types et de deux classes de types : • les types de base ( i n t , bool, s t r i n g , . . . ) , • les types composés, La production grammaticale qui les définit est la suivante : Type := BasicType | Type -* Type | Type * Type Dans ce langage, les constructeurs de valeurs et les constructeurs de types ne sont pas dénotés de la même manière. Les termes définissant les expressions à évaluer et ceux définissant les types ne sont donc pas construits sur la même signature : • c'est le constructeur "," qui sert à construire les uplets de valeurs et "*" les uplets ou produits de types ; • les listes de valeurs sont construites par "[ ]" tandis que le type "liste sur un type variable a" s'écrit ' a l i s t ; • la valeur "( )" est de type u n i t . 1.1. Les langages fonctionnels Les règles de typage, souvent présentées sous la forme de règles d'inférence logiques utilisant le symbole h, vont comprendre les déclarations de constantes typées (true est de type bool d'où la règle h t r u e : bool) et permettre d'inférer les jugements de la forme C hM :r où C est un contexte (ensemble fini de déclarations de variables), M un terme du langage de programmation et r un type, c'est-à-dire un terme du "langage de typage". Ces règles de typage peuvent être utilisées pour vérifier un type (lorsque C, M et r sont connus) ou pour une synthèse de type (lorsque r est inconnu) comme c'est le cas en CAML. Synthèse de types en CAML : Au problème "Comment trouver le type le plus général pour une expression du langage ?", CAML et les langages de cette famille répondent en utilisant un algorithme basé sur un procédé d'unification "destructive" sur les termes du premier ordre que sont les types. Un nouvel ensemble de règles d'inférences est écrit (par rapport à celles qui définissent ce qu'est un type), que l'on peut voir comme un algorithme puisqu'il admet exactement une conclusion pour chaque construction syntaxique. Pour une expression donnée du langage CAML, la déduction de type pour cette expression utilise exactement une règle par sous-expression. Ainsi la déduction est structurée selon le même schéma que celui de l'expression, ce qui permet par là-même de reconstruire une expression à partir de son arbre de déduction de type. Remarque : Le type i n t -> i n t est le type exprimant qu'un terme du langage de programmation de ce type est une fonction des entiers naturels vers les entiers naturels. Le fait de pouvoir écrire des types comme (int —• i n t ) —ï ( i n t -» i n t ) nous fait parfois parler de langages d'"ordre supérieur". Cette notion peut se formaliser en se donnant une fonction ord associant à tout type atomique un entier (ex : ord(int) = 1), prolongée par ord(ri -> r 2 ) = max(ord(ri) + l,ord(r 2 )). 1.2. Les langages algébriques - LPG 10 Exemple 2 : Les types du système F Le système F de Girard [14] est un système de types dits de second ordre (cette notion d'ordre n'étant pas à assimiler à la précédente), avec le Àcalcul comme modèle de langage de programmation. Pour former les types,on considère les formules écrites sur un ensemble infini dénombrable de variables (dites variables de type : X, Y,...), le connecteur —• et le quantificateur V. On définit sur cet ensemble de formules une notion de substitution, puis de a- équivalence (par induction et en utilisant la substitution : t\ = £2 si t X) -> X} (type produit de A et B) List(Y) = VX {(Y,X -+ X),X -» X} (type des listes d'objets de type Y) Un terme du À-calcul de type Id sera par exemple M = Àxx, un À-terme booléen M = XxXyx ou M = XxXyy. Remarque : Il est possible de "décoder" les types du système F dans la théorie des esquisses, ou plutôt des trames qui sont une généralisation de la notion d'esquisse. A partir du type List(Y) par exemple, on obtient une trame d'ordre 2 [5, 1]. 1.2 Les langages algébriques - LPG Si les langages fonctionnels déterminent la construction de types à partir d'opérations sur des types déjà définis, par somme ou produit par exemple, les langages algébriques relient la notion de type (de données) à celle de classe de modèles d'une théorie algébrique. A titre d'exemple, on écrit en LPG [3] des spécifications algébriques et on s'intéresse à la classe des modèles d'une telle spécification. Une propriété 1.3. Exemple du langage Haskell 11 LPG est une spécification particulière, définissant une classe de modèles, et on peut déclarer dans LPG qu'un type, ou type abstrait algébrique, est un modèle d'une propriété. Exemple : Soient la propriété property Ensemble sorts E end Ensemble et le type abstrait type Naturel s o r t s nat constructors zéro : -> nat suce : nat -> nat operators + : ( n a t , n a t ) -> nat v a r i a b l e s i , j : nat équations 1 : zéro + j ==> j 2 : s u c c ( i ) + j ==> succ(i+j) end Naturel On spécifie que Naturel est modèle de Ensemble par la déclaration : models Naturel : Ensemble [nat] On fait ainsi correspondre aux sortes et opérateurs de la propriété les sortes et opérateur d'un type : ici ce sont seulement les sortes nat et E qui sont en correspondance. 1.3 Exemple du langage Haskell Haskell [12] est un langage fonctionnel qui permet de définir des types abstraits algébriques et des classes de types. 1.3. Exemple du langage Haskell ^ 12 Types et valeurs d'expressions ne sont pas confondus mais la notion de g e n r e permet de caractériser les types. Les valeurs de types sont construites à partir de constructeurs de types et les expressions de types sont caractérisées par un g e n r e pour assurer leur validité. On peut ainsi les classer avec les deux seules formes qui peuvent être prises : • Le symbole * représente le genre de tous les constructeurs de types 0-aires. • Si ki et k2 sont des genres, alors fci —• k2 est le genre des types qui prennent un type de genre k\ et retournent un type de genre k2. On détermine alors le genre des expressions de types : • Les variables de types ont leur genre inféré par le contexte dans lequel elles apparaissent. • Les constructeurs constants I n t , F l o a t , Char, . . . sont de genre *. • Le constructeur —y a pour genre * - > * - * * . • Les constructeurs de uplets de types ( ) , ( ) , ( , ) , ( , , ) , pour 0, 1, 2 ou 3 éléments, ont pour genre * , * - > * , * - > * — > • * , * — > • * — > . * — > * . La construction d'un type abstrait en Haskell peut se faire en utilisant une déclaration newtype à partir d'un type existant. Exemple : Piles définies par les listes module S t a c k (StkType, p u s h , p o p , empty) where newtype StkType a = S t k [ a ] push x (Stk s ) = Stk (x : s ) pop ( S t k (x : s ) ) = S t k s empty = S t k [ ] Dans le noyau Prélude de Haskell, on a par exemple les types abstraits I n t e g e r , F l o a t et la classe prédéfinie de types Num, dont I n t e g e r et F l o a t sont des instances selon la terminologie Haskell. Ils sont par ailleurs instances de la classe Eq définie par : 1.4. Quelques spécificités d'Aldor 13 c l a s s Eq a where ( = = ) , ( / = ) : : a -» a -> Bool x/ = y = not (x = = y) Une déclaration i n s t a n c e stipule qu'un type est une instance d'une classe. On notera que les types Haskell sont structurés par un ordre de généralisation : on dit qu'un type 7\ est plus général qu'un type T2 (en faisant appel à une notion de substitution) et le type le plus général que l'on peut associer à une expression est appelé son type principal. 1.4 Quelques spécificités d'Aldor Aldor est un langage basé sur l'évaluation d'expressions. On verra ultérieurement quelles sont les règles à respecter pour former les expressions, ie la syntaxe du langage. Chaque expression du langage est évaluée et cette exécution produit un ensemble de valeurs. Les valeurs calculées peuvent ensuite être sauvées dans des variables ou des constantes identifiées (un identificateur n'étant qu'une chaîne de caractères, exception faite des mots réservés du langage tels with, add, i f , t h e n , e l s e , r e p e a t . . . , utilisé pour nommer des variables ou des constantes par une affectation := ou une définition = = ) . Définir une variable ou une constante consiste à associer une expression, un identificateur et éventuellement un type. Définir une paire (nom, valeur) revient alors à apparier les noms de variables et les valeurs affectées, et un ensemble de paires (nom, valeur) constitue un environnement. L'approche choisie par les concepteurs est celle de "types sur les variables et constantes" : les types sont associés aux variables et constantes soit par des déclarations, soit inférés de l'expression qui les définit, et il n'est pas possible, à partir d'une seule valeur, de retrouver son type. Les types étant décrits par les mêmes formules que les expressions évaluées par le langage, on parle de types comme valeurs de première classe. On pourra en particulier les passer en arguments de fonctions si leurs types (de ces types) sont adéquats ou encore les affecter à des variables. 1.4. Quelques spécificités d'Aldor 14 Cette spécificité a des conséquences très particulières, que l'on se propose de présenter de suite. Chapitre 2 Les types d'Aldor On s'intéresse dans ce chapitre aux pures notions de typage : association d'un type à une expression et sa vérification dans le monde des types. D'autres notions viendront s'y greffer en fin de document, notamment celle de nature. 2.1 Expressions d'Aldor et types Les expressions d'Aldor sont des termes sur une signature donnée E . Notons EXPR l'ensemble des termes du premier ordre sur E. Les termes décrivant les types d'Aldor sont produits à partir d'une signature E j . On note TYPE l'ensemble de ces termes. L'affirmation Aldor est un langage typé signifie que l'on définit ainsi une application type : EXPR -+ TYPE telle que chaque expression a exactement un type. La seule trace visible de cette application en Aldor réside dans l'affichage en mode interactif : un type est proposé après chaque évaluation. C'est en général le type de l'expression évaluée. 15 2.2. Fonctions et objets de base 16 Exemple 1: f : Integer -> I n t e g e r == (x: I n t e g e r ) : I n t e g e r +-> x + 1 est une définition de fonction et type(f) = I n t e g e r -> Integer, où le type est construit à partir du terme type I n t e g e r et du constructeur de type —>. La première conséquence de la sentence u Tous les termes Aldor sont des valeurs de premier ordre" s'applique aux termes décrivant les types : TYPE C EXPR. Pour la plupart des langages de calcul on ne peut comparer les termes sur E et les termes sur E^. Comme on a vu que la prescription d'un type est permise pour tous les éléments de EXPR, la question du typage des types sera alors à étudier. 2.2 Fonctions et objets de base Si FONC désigne l'ensemble des fonctions alors EXPR = FONC II OBJU TYPE (réunion disjointe) avec OBJ l'ensemble des objets de base (ni fonctions ni types). La fonction type de EXPR vers TYPE est donc à définir à la fois sur FONC, OBJ et TYPE. Un type étant qu'une expression, une fonction peut produire un type : on appelle constructeur de t y p e toute fonction Aldor retournant un type (—>-, Tuple, Cross, etc pour les prédéfinies, et toutes les fonctions définies par l'utilisateur). Dans l'exemple 1, le constructeur —• est un élément de FONC et est aussi un élément de Ex puisqu'il retourne le type I n t e g e r —»• Integer une fois appliqué aux deux types I n t e g e r , I n t e g e r , mais il n'est pas dans TYPE puisque FONC D TYPE = 0 . 2.3. Satisfaction de types 2.3 17 Satisfaction de types La quasi-totalité des langages fonctionnels mettent en oeuvre une vérification de types pour l'application : si / est une fonction de type A —• B où A et B sont des types alors f(x) est une expression valide si et seulement si le type de x est exactement A. Cette vérification est sensiblement différente en Aldor. On a d'une part : f(x) est une expression valide si le type de x satisfait le type A, et d'autre part cette condition concernant uniquement le typage s'accompagne en fait d'une deuxième condition . Celle-ci ne concerne pas uniquement le typage, elle fait aussi intervenir le corps de la définition. On y reviendra dans le dernier chapitre de ce travail. On ne s'intéresse pour le moment qu'aux seuls types. Le langage Aldor définit une relation de satisfaction sur les types et, si l'on sait que toute expression a exactement un type, celui-ci peut en satisfaire plusieurs autres. Cette relation de satisfaction sera décrite dans ce document par le formalisme des esquisses, au cours du chapitre 4. Exemple 2 : Le type ( I n t e g e r , I n t e g e r ) des couples d'entiers satisfait le type Tuple(Integer) des uplets d'entier. Cette satisfaction est "automatique" en Aldor (6.4.3). 2.4 Types-domaines et types des domaines Les types des fonctions et des objets de base sont appelés parfois typesdomaines en Aldor, ou le plus souvent domaines. Si DOM désigne l'ensemble de tous les domaines alors DOM C TYPE. Exemple 3 : Integer and I n t e g e r -» I n t e g e r sont des domaines. Pour en faire une présentation simple, complétée dans le paragraphe suivant, on peut considérer le domaine des entiers comme la définition des opérateurs accessibles sur les entiers. 2.5. Types-catégories et types des catégories 18 Pour répondre maintenant à la question "Quel est le type d'un domaine ?", on pourrait introduire un unique type noté Type. Ce type existe en Aldor et il s'agit d'un domaine, mais ce seul typage par Type est insuffisant pour exprimer toute la richesse du système de types d'Aldor. La raison principale est la suivante : puisque TYPE Ç EXPR, un domaine peut être argument d'une fonction dans un contexte d'application. Si le type de tout domaine est Type, on ne peut définir des fonctions que sous la forme : <7(T:Type):B==... Cette fonction g prend un domaine en argument. Il est de fait impossible de placer des restrictions sur les domaines acceptables par la fonction g comme arguments, en termes d'opérateurs disponibles par exemple. Si g est par exemple une fonction de tri d'éléments, qui à partir d'une séquence retourne la séquence triée, le domaine de ces éléments doit fournir un opérateur de comparaison, ce que l'on aimerait signifier dans le typage. Ce concept de type unique pour tous les domaines n'est pas satisfaisant. En réalité tout domaine a un type qui satisfait Type sans être nécessairement Type. Ce peut être un type-catégorie. 2.5 Types-catégories et types des catégories 2.5.1 Catégories comme types de domaines Un type-catégorie ou catégorie est destiné à apporter des restrictions sur les domaines possibles dans un contexte de typage donné. La conception d'un domaine en Aldor est celle du typage dans les langages algébriques : c'est un type abstrait de données (ADT). Il est constitué d'un type exporté (noté % dans la définition du domaine et qui prend ensuite le nom du domaine une fois exporté), et d'une collection d'opérations exportées, ce qui détermine une signature hétérogène sous-jacente au domaine. Exemple 4 : un domaine des À-termes Lambda-termes :with{ vax : Variable —• %; — Variable e s t un domaine préalablement d é f i n i 2.5. Types-catégories et types des catégories 19 abs : (Variable, %) ->• %; apply : (%, %) -»•%;} == add { var (x:Variable) : % — x prétend % abs (x:Variable, M:%) — ... } Le domaine Lambda-termes est un ADT sur la signature multi-sortes . La notion de catégorie s'appuie sur celle de signature au sens où l'on reprend les symboles fonctionnels de la signature, munis de leur profil. S'y ajoutent des constructions particulières, en termes d'héritage par exemple, non détaillées ici mais dans le chapitre 7. Exemple 5 : Une catégorie identifiée (ie à laquelle on a associé un identificateur) de termes Termes == with { var : Variable -> %; } — Toute v a r i a b l e e s t un terme La catégorie Termes est relative à la signature multi-sortes ^termes = < {Variable, %}, {var} > . si l'on définit une fonction modele(D : Termes ) : Type ==... alors cette fonction modèle accepte comme arguments toutes les expressions D vérifiant la condition désormais habituelle : le type de D satisfait la catégorie Termes. Ainsi Lambda-termes est un argument valide pour modèle, son type étant la catégorie non identifiée (ou anonyme) with{ var : Variable -» %; abs : (Variable, %) -» %; apply : (%, %) -» %; } Il y a une inclusion de signatures entre cette catégorie et Termes, ce qui constitue un des cas de satisfaction de types, donc cette catégorie anonyme satisfait la catégorie Termes. 2.6. Domaines et catégories comme types 20 Pour des domaines très usités, on a par exemple : • I n t e g e r de type la catégorie Join(IntegerNumberSystem, Steppable) with { i n t e g e r . . . } ; • I n t e g e r -» I n t e g e r de type la catégorie with. 2.5.2 Types des catégories Si CAT est l'ensemble des catégories d'Aldor alors CATC TYPE et elles ont elles-mêmes un type. Ce pourrait être là encore un type unique, noté Category. Ce type existe en Aldor et c'est un domaine, mais pour de semblables raisons ce n'est pas le type unique des catégories, il n'est qu'un type satisfait par tous les types des catégories. Dans ce langage, les catégories sont typées par d'autres catégories ou par le domaine Category. Une catégorie peut être utilisée comme type d'une autre si une relation d'héritage est satisfaite, par exemple si elle fournit suffisamment d'opérations ou constantes exportées. Exemple 6 : Les catégories Group et Monoid sont de type Category, et Group hérite de Monoid puisque : • Monoid : Category == BasicType with {1 : % ; * : . . . } • Group : Category « Monoid with {inv : % —ï % ; . . . } Toutes ces notions seront définies ultérieurement. 2.6 Domaines et catégories comme types Il est maintenant possible de typer toute expression Aldor par un domaine ou une catégorie. TYPE = CAT U DOM. 2.6. Domaines et catégories comme types 21 Les deux domaines Type et Category ont une fonction privilégiée dans le typage: type : FONC^ DOM\{Type, Category} type : OBJ-ï DOM\{Type,Category} type : DOM-* CATU {Type} type : CAT-> CATU {Type, Category} Il n'est alors pas nécessaire d'introduire de nouveaux types puisque les catégories typent les catégories. Avec ce système de types, une expression E est : • une fonction ou un objet de base si le type de E est un domaine différent de Type et Category ; • une catégorie si le type de E est Category ; • un domaine ou une catégorie sinon, i.e. si le type de E est Type ou une catégorie. Cette dernière ambiguité peut être levée si nécessaire (application de fonction par exemple), en faisant alors référence à la notion de nature et non plus de typage. Ceci sera abordé en 5.1.4 et repris en 7.2. On notera tout de même l'ambiguité que ce choix introduit en Aldor. Type pouvant être le type d'une catégorie, alors on obtient un cas de satisfaction immédiat : Type satisfait Category puisque tout type de catégorie satisfait Category (ce sera défini en termes d'esquisses). Mais Type peut aussi être le type d'un domaine. On se trouve donc dans la situation où le type d'un domaine satisfait Category, ce qui peut troubler l'utilisateur a priori, mais la deuxième condition de vérification de type que l'on introduira au dernier chapitre assure la validité des expressions que l'on forme. 22 2.7. Présentation graphique 2.7 Présentation graphique Les différents ensembles et applications introduits dans ce chapitre se présentent ainsi : FONC DOM CAT Chapitre 3 Esquisses Le schéma précédent (fin du chapitre 2) liait des ensembles (EXPR, TYPE, ...) par le moyen d'applications dont certaines étaient des injections. Ce dessin (?2 ne fait que refléter, en termes ensemblistes, une structure que l'on aurait pu décrire de manière plus formelle par le graphe Gi suivant : constitué uniquement d'objets et de flèches au sens le plus strict. Gi et G2 ont la même structure au sens où l'on peut envoyer G\ sur G2 par une famille d'applications, objets sur ensembles et flèches sur applications, ici : • A sur EXPR # B sur TYPE # C sur FONC • etc 23 24 en respectant domaine et codomaine de chacune des flèches. On connaît d'autres propriétés sur ces ensembles qui ne sont pas exprimées dans (?2, par exemple le fait que EXPR est la somme des ensembles FONC, OBJ, TYPE et TYPE la somme de DOM et CAT. Par contre ceci peut se faire explicitement à partir de Gi en décrétant que certains cônes ont un statut particulier, auquel cas on ne considère plus seulement G\ mais G\ et un ensemble de cônes distingués issus de G\ : + B E Dans le cas présent, les deux cônes distingués sont des cônes inductifs. Ce graphe Gf avec cônes distingués doit encore pouvoir s'envoyer sur G2 (on n'a rajouté ni objet ni flèche) avec la même famille d'applications que précédemment. On doit préciser cette fois que l'image de A doit être la réunion disjointe des ensembles images de C, D, B, idem pour l'image de B, ce qui est vérifié par notre famille d'applications, telle qu'elle avait été définie. La donnée ainsi constituée est celle d'une esquisse (Gf), d'un foncteur (la famille d'applications vérifiant une bonne propriété) caractérisant un modèle ensembliste, toutes notions que l'on définit dans ce chapitre. Remarque : Dans G\, on peut déjà nommer les objets EXPR, TYPE, FONC, OBJ, DOM, CAT, tout ceci étant purement syntaxique et ne présageant en rien des modèles que l'on va considérer. 3.1. Graphes à composition 3.1 25 Graphes à composition La notion de graphe est essentielle dans le formalisme que l'on a choisi pour exprimer la théorie des esquisses. Il s'agit en effet d'un formalisme graphique, où le graphe à composition est la base du discours. Définition 3.1.1 Un graphe orienté consiste en la donnée d'une classe d'objets OBJ, d'une classe de flèches FL et des opérations dom : FL —> OBJ (sélection des domaines) codom : FL —> OBJ (sélection des codomaines) telles que : • pour A -> B dans FL, dorn(f) = A et codom(f) = B Exemple : Sous forme graphique : J- -O» ou plus classiquement : OBJ = FL = {A,B,C} {AÂB,BAB,CAA} dorn(f) = A, dom(g) = codom(g) = B,... Définition 3.1.2 Un graphe à composition (fort) consiste en la donnée d'un graphe orienté et des opérations : selid : OBJ —• FL (sélection des identités) comp : FL • FL -)• FL (composition) telles que : 3.1. Graphes à composition 26 • FL + FLÇ {(g, f) e FLxFL: codom(f) = dom(g)}, FL • FL est appelé l'ensemble des couples de flèches composables, V(g,f) G FL*FL,comp :(g,f)*+gof pour reprendre la notation habituelle des composées. • Axiome de position : V5 G OBJ, dom(selid(B)) = B = codom(selid(B)), dont o selid = codorn o selid = soit encore Idosj (fonction identité sur la classe OBJ) • Axiome d'unitarité : pour tout objet B, la flèche selid(B), notée parfois ids est une identité : VA -4 B, V5 ^C,idBof = f et # o zrfB = p Exemple de graphe à composition : Sous forme graphique ou plus classiquement : cornp(j, h) = j o /i = / Nota On ne représentera pas toujours les flèches identités. 3.2. Catégories 3.2 27 Catégories Définition 3.2.1 Une catégorie consiste en la donnée d'une classe d'objets OBJ, d'une classe de flèches FL et des opérations : dorn : FL -> OBJ (sélection des domaines) codom : FL —• OBJ (sélection des codomaines) selid : OBJ —» FL (sélection des identités) cornp : FL • FL —> FL (composition) telles que : • pour A -¥ B dans FL, dom(f) = A et codorn(f) = B • FL*FL= {(g, f) eFLx V(s,/) e FL• FL,cornp FL: codom(f) = dom(g)}, :(gJ)*-*gof • Axiome d'associativité : VA4B,VBAC,VCAD,ho(gof) = (hog)of • Axiome de position : pour tout objet B, on a une flèche selid(B) notée icfe dans FL dom(idB) = B et codom(idB) = B • Axiome d'unitarité : pour tout objet B, la flèche ids est une identité VA -4 £ , V £ I>C,idBof = f et £ o ttfe = # Autrement dit une catégorie est un graphe à composition fort, avec une composition associative et une composabilité maximale. Exemple : La catégorie Ens des ensembles avec comme objets tous les ensembles et comme flèches toutes les applications. 3.3. Fondeurs 3.3 28 Foncteurs Définition 3.3.1 Soient G = (OBJG, FLG, FLG * FLG, domG,...) et G' = {OBJQI , FLQ> , FLGi -kFljQi, dornGi,...) deux graphes à composition forts, un homomorphisme entre G et G' est un triplet H = (OBJ(H), FL(H),H* H) où: OBJ {H) : OBJG -»• OBJG. FL(H) : FLG -»• FLG> H*H : FLG*FLG -+ FLG. * FLG* sont des applications telles que : • V/ e FLG, domG,(FL{H)(f)) codomG.(FL{H)(f)) = = OBJ{H)(domG(f)) OBJ(H)(codomG(f)) soit encore l'égalité fonctionnelle o FL(H) = OBJ(H) o codomG ou la notation simplifiée V/ € F-^G, dom(H(f)) codom(H(f)) • H* H(g,f) H(dom(f)) H{codom(f)) = (H(g), H(f)) en notation simplifiée • FL(H)(selid) = Graphiquement : = = selid(OBJ(H)) 3.4. Cônes 29 OBJ(H) OBJG OBJG. domp \codomG FLG + Pi dafriG> j codomnf FL(H) compçm H H FLG• FLG * > FLG, *FL G / Pi,P2,qi,<]2 sont les projections, avec les conditions de commutation suivantes sur les diagrammes FL(H\ FL{H\ FL(H\ ?i Vï qi compG H*H H*H H*H OBJ(H) OBJ(H\ FL(H) domA domGt FL(H) codovriQ codomG* FL{H) compQt idp OBJ{H) Un homomorphisme entre graphes à composition est appelé un foncteur. 3.4 Cônes Définition 3.4.1 Soit I un graphe à composition. 3.4. Cônes 30 On appelle cône projectif type de base I le graphe Cp obtenu en ajoutant à I un objet (le sommet) et des flèches (les génératrices) en même nombre que les objets de I, chacune ayant pour domaine le sommet du cône et pour codomaine un objet de la base I : avec une condition de commutation pour chaque flèche de I. 7Tj = j O 7T/ KK — k O 7T J Définition 3.4.2 Soit I un graphe à composition. On appelle cône inductif type de base I le graphe Ci obtenu en ajoutant à I un objet (le sommet) et des flèches (les génératrices) en même nombre que les objets de I, ayant pour domaine un objet de la base I et pour codomaine le sommet du cône : 3.4. Cônes 31 avec là aussi une condition de commutation pour chaque flèche de I : ai = cri o % • B K M- C J k 7TJ 7T/V- Fi: <7j H* a 6 r H-* s t H» b v H- Remarque : En parlant de cône, on confondra souvent le foncteur et son image dans un graphe. 3.5 Esquisses Définition 3.5.1 Une esquisse E consiste en la donnée d'un graphe à composition G (le support de E), d'un ensemble V de cônes projectifs dans G et 33 3.5. Esquisses d'un ensemble I de cônes inductifs dans G. Ces cônes sont appelés cônes distingués dans E. Exemple : Une esquisse E\ des ensembles munis d'une loi binaire ; Ex = (G,V,I) avec : 0 H> E2 Fpl : l 1 \-> Ei . 2 H> TTI !-» pi 7r2 *-* P2 ^ 7> = {Fpl}, J = 0 Exemple : Une esquisse 2¾ d e s ensembles munis d'une loi binaire et d'une loi 0-aire (une constante) ; E2 = (G,V,Z) avec : Fp2 : 0 H-> £ 0 (base vide !) 7> = {Fpl,JF>2}, X = 0 34 3.6. Limites projectives et inductives 3.6 Limites projectives et inductives On va donner à certains cônes un statut particulier, celui d'être une limite projective ou inductive. On n'exprimera pas ces propriétés d'algèbre universelle sur les foncteurs eux-mêmes, ce qui nous amènerait à définir d'autres objets de la théorie des catégories, mais sur leurs images dans un graphe. Définition 3.6.1 Soient C une catégorie et Cp (respectivement Ci) un cône projectif (respectivement inductif) type de base I, soit F un foncteur de Cp (respectivement Ci) vers C. F = (OBJ(F), FL(F),F* F) est un cône limite projective si : pour tout autre cône G de même base I dans le graphe sous-jacent à C, il existe une unique flèche dans C de OBJ(G)(0) vers OBJ(F)(0) qui réalise les conditions de commutation pour chacune des arêtes des cônes. Supposons [ ( OBJ(F){0) OBJ(F)(I) OBJ(F)(J) OBJ(G)(0) OBJ(G)(I) ' OBJ{G)(J) D B C A FL(F)(j) = e B C FL(F)(TT/) FL(F)(ITJ) = = b c FL(G)(j) = e FL(G)(7T/) = boa FL(G)(nj) = d 3.7. Modèle 35 Alors il existe une unique flèche de domaine D et codomaine A, notons la fact(bo a,d), qui réalise : { b o fact(b o a, d) = boa co fact(bo a,d) = d Certains cônes limite projective sont appelés également cônes produit, ou produits, et parfois identifiés au seul sommet image s'il n'y a pas ambiguité. Le cas inductif s'obtient en inversant les flèches et un cône limite inductive s'appelle parfois un cône somme ou une somme ; la flèche analogue à fact y est notée cofact. Exemple : Le produit cartésien de deux ensembles muni de ses deux projections est un cône limite projective dans la catégorie Eus des ensembles. La réunion disjointe joue le rôle de la limite inductive. Cas particulier : Cônes limites projectives de base vide La propriété générale devient excessivement simple lorsque les cônes considérés sont de base vide. Ainsi un cône limite projective de base vide vers un graphe G sélectionne un objet du graphe, noté 1 de coutume, vérifiant : VA € OBJG, ^WA E FLG,dom(\A) = A,codom(XA) = 1 On appelle souvent 1 l'objet t e r m i n a l et une flèche de 1 vers un autre objet est appelée une constante. 3.7 Modèle Définition 3.7.1 Soit E = (G,V,X) une esquisse. Un modèle de E dans une catégorie C consiste en la donnée d'un foncteur F de G vers C tel que : • l'image par F de tout cône projectif distingué dans E est un cône limite projective dans C ; • l'image par F de tout cône inductif distingué dans E est un cône limite inductive dans C. 3.8. Catégorie cartésienne et cartésienne fermée Exemple : 36 Un modèle ensembliste d'une esquisse E Ens où les cônes distingués dans E sont envoyés dans Ens sur des cônes limites comme suit : EQ {0} Théorème 3.7.1 Les modèles d'une esquisse E dans une catégorie C forment une catégorie, que Von notera le plus souvent Mod(E,C), dont les objets sont les modèles de E dans C et les flèches les transformations naturelles entre les modèles. 3.8 Catégorie cartésienne et cartésienne fermée Définition 3.8.1 C est une catégorie cartésienne si : 1. C est une catégorie 3.8. Catégorie cartésienne et cartésienne fermée 37 2. il existe un objet 1, appelé objet terminal, tel que, pour tout objet A, FLA,I contient un seul élément noté A^ 3. pour tous objets A et B, il existe un objet A x B et deux flèches pflB : A x B -» A et p^B : A x B -> B, tels que, pour tout objet C et toutes flèches C —y A, C A B, il existe une unique flèche fact(f,g) : C -¥ Ax B telle que : pïB o fact(f, g) = f { PÏ o fact(f,g) B = 9 AxB En d'autres termes, une catégorie cartésienne est une catégorie qui contient tous les produits finis. Exemple : La catégorie Ens des ensembles munie du produit cartésien. Exemple : Considérons toutes les formules du premier ordre du calcul des propositions, on obtient une catégorie Prop ayant comme objets les propositions et comme flèches les dérivations. Par exemple, soient P et Q deux propositions, si P H Q, alors il existe une flèche dans Prop de domaine P et codomaine Q. En outre, la catégorie Prop est une catégorie cartésienne puisque, dès lors que l'on a deux objets P et Q, on a l'objet P A Q, et les deux flèches déduites des règles PAQ h P, PAQ h Q sont les deux flèches de projection. Définition 3.8.2 C est une catégorie cartésienne fermée si : 1. C est une catégorie cartésienne 3.9. 38 Catégorie-type 2. pour tous objets A et B, il existe un objet BA et une flèche appAyB • BA x A - • B, appelée application, tels que, pour tout objet C et toute flèche / : C x A -* 5 , il existe une unique flèche À/ : C —• Z?A appelée la curryfiée de / , telle que : ap/>A,£ o fact(\foprojuproj2) = / fîA x appA7B fact(. CxA Exemple : La catégorie Ens des ensemble est une catégorie cartésienne fermée. Pour tous objets A et S de .Ens, on a l'objet Hom(A, B) ensemble des applications de A vers B qui joue le rôle de l'objet exponentiel BA et la flèche d'application qui, à une application f de A vers B et un élément a de A associe l'élément f(a) de B. Exemple : La catégorie Prop est une catégorie cartésienne fermée. Pour tous objets P et Q, on a un objet exponentiel P =>• Q et une flèche d'application associée déduite de la règle (P =» Q) A P h Q. 3•9 Cat égor ie-ty p e Définition 3.9.1 Soit U : C -» C' un foncteur entre deux catégories. 3.9. Catégorie-type 39 Soient C un objet de C, C' un objet de C' et e une flèche de C' vers U(C). On dit que e présente C comme un objet libre engendré par C' relativement à U si, pour tout objet D de C, pour toute flèche / de C' vers U(D), il existe une et une seule flèche h : C -¥ D dans C telle que U(h)os = f. (on a noté U(h) pour FL(U)(h).) ^D U(C) c U(h) : U{D) V/ Exemple : Soient E une signature unisorte et X un ensemble, l'algèbre 2E[X] des termes du premier ordre sur E et à variables dans X est engendrée librement par X. Ici c'est la catégorie des ensembles qui joue le rôle de C', et la catégorie des E-algèbres le rôle de C. On peut également appliquer la définition précédente avec C la catégorie des catégories cartésiennes fermées à limites projectives et inductives, et C' la catégorie des esquisses. Une esquisse engendre librement une catégorie cartésienne fermée à limites et U est un foncteur d'oubli qui permet de "voir" une catégorie comme une esquisse. C'est un théorème dû à C. Ehresmann [8] : Théorème 3.9.1 Toute esquisse engendre librement une catégorie cartésienne fermée à limites projectives et inductives, unique à isomorphisme près. Définition 3.9.2 La catégorie cartésienne fermée à limites engendrée librement par une esquisse E = (G,V,I) est appelée catégorie-type de E. 3.9. Catégorie-type 40 Pratiquement, on considère le graphe G sous-jacent à E, auquel on ajoute toutes les composées de flèches consécutives dans G, les limites projectives et inductives, les objets exponentiels, les flèches d'application et de curryfication ainsi que toutes les flèches de factorisation (cas inductif et projectif) des cônes distingués dans E. Les cônes distingués dans E deviennent ainsi des cônes limites dans la catégorie-type de E. Exemple : Une approche ultra-simplifiée des entiers naturels La catégorie type de l'esquisse E du 3.7 permet, en rajoutant seulement les factorisations et de la composition pour ce qui nous intéresse, d'atteindre les termes k(e, / ) , k(f, k{e, / ) ) , . . . *(*,/)) k o fact(e, f) Ainsi un entier naturel peut être vu classiquement comme un élément de l'ensemble N dans un modèle de l'esquisse E, ou plus syntaxiquement comme une flèche de EQ vers E\ dans l'esquisse E ou dans sa catégorie type. Ce point de vue "syntaxique" est celui de toute la théorie des esquisses. Chapitre 4 Une interprétation d'Aldor en termes d'esquisses Aldor étant un langage typé de calcul formel, basé sur l'interprétation d'expressions, on se retrouve dans un univers comprenant des classes : classe des types, classe des fonctions, ..., et plus généralement classe des expressions, entre lesquelles on met en évidence des liens, par les notions d'héritage ou de typage par exemple. Une des questions qui se posent est alors de savoir s'il est possible de structurer 1'"univers" que compose le langage Aldor, en utilisant la structure essentielle de catégorie entre autres. Pour cela, on va déterminer une esquisse associée au langage Aldor. Ce sera pour nous une esquisse "généralisée", au sens où on permet la construction d'objets exponentiels dans l'esquisse. Elle est destinée à exprimer aussi bien la syntaxe du langage que les propriétés qui lui sont associées (soustypage, héritage, . . . ) . On notera cette esquisse E Aldor, et la catégorie cartésienne fermée à limites qu'elle engendre librement (cf 3.9) sera notée C Aldor- On décrit T^Aidor par étapes, en traduisant systématiquement le fonctionnement d'Aldor en termes d'esquisses. L'objectif ultime est de retrouver le langage Aldor comme modèle de cette esquisse, en considérant en particulier des modèles ensemblistes pour lesquels les objets de 'EAldor sont interprétés respectivement en la classe des fonctions d'Aldor, la classe des types d'Aldor, etc. 41 4.1. Structure de catégorie 4.1 42 Structure de catégorie Proposition 4.1.1 "E Aldor contient une esquisse des catégories. Pour esquisser Aldor en conservant notre point de vue qui est de décrire au moins le typage du langage, on va poser les premiers objets de cette esquisse ainsi que les premières flèches, en tout premier lieu l'objet des types d'Aldor, que l'on note TYPE. Une possibilité qu'offre Aldor pour agir sur les types consiste à utiliser les fonctions. Celles-ci permettent en effet, à partir d'un objet d'un certain type, de déterminer un objet d'un type éventuellement différent par application de ladite fonction. On peut donc les caractériser par un type "source" et un type "but", ce qui se représente, en notant FONC l'objet des fonctions : TYPE ^f^^FONC but Définition 4.1.1 Deux fonctions en Aldor sont composables dès lors que la source de l'une et le but de l'autre coïncident : si source(f) = t\, but(f) = ti, si source(g) = u\, but(g) = tz2 et si u\ = t2} alors la composée compose(g,f), notée g f est une fonction de source t\ et de but U2, ce que l'on peut représenter graphiquement : Si l'on considère les couples de fonctions composables, dont l'objet est noté FONCComp dans T&Aidor, on obtient le graphe à composition suivant sous-jacent à l&Aidor -" ^^ TYPE ^zf^î^FONC but g/7?/.^fep •rnmPM^FONCComp " droite^ 4.1. Structure de catégorie 43 but o droite = source o gauche où le cône projectif ci-dessous est distingué dans "EAldor FONCComp -'FONC La fonction obtenue par composabilité doit respecter les équations suivantes, inscrites dans l&Aidor '- i source o compose but o compose = = source o droite but o gauche La composition est associative, ce que l'on traduit en introduisant l'objet F0NCComp2 des triples de fonctions composables, sommet d'un cône projectif distingué de E Aldor ' FONCÇomp2 gauchie miïieu FONC *cèv soura TYPE FONC but source b TYPE FONC 4.2. Fonctions, items et types i 44 source o gauche source o milieu = = but o milieu but o droite plus un certain nombre de flèches et d'équations pour exprimer les "projections" partielles et l'égalité des compositions selon le parenthésage. Toutes ces propriétés font de "EtAldor en particulier une esquisse des catégories. l 4.2 Fonctions, items et types 4.2.1 Fonctions et items Outre les fonctions, Aldor manipule des objets de base, domaines et catégories, toutes données que l'on désigne sous le vocable "items". Donc, si OBJ désigne l'objet des objets de base d'Aldor, DOM l'objet des domaines et CAT l'objet des catégories d'Aldor, OBJ et ce cône inductif est distingué dans EtAidor (donc cône limite inductive dans C Aldor)' On introduit maintenant l'objet des expressions d'Aldor : EXPR 'x FONC 1 ITEM On ne fait pas figurer dans le graphe sous-jacent à E^/dor les flèches identités ni la flèche selid de l'esquisse des catégories. 4.2. Fonctions, items et types 45 ce dernier cône faisant partie des cônes projectifs distingués dans EiAidorIl existe une systématique de traduction en Aldor , non automatique cependant, d'un item vers une fonction : l'item est x : T = = E et la fonction x : () -> T = = () : T+->E, la propriété de comparaison étant x() = x. FONC ^ ITEM source o ij = ( ) o ÀJTSM où ( ) est le "type vide". On utilisera ici ce type comme une donnée, il est en fait produit par un constructeur de types, ce qui sera justifié dans la section à suivre. La flèche XITEM est l'unique flèche de ITEM vers 1 (objet terminal dans la catégorie C ^ o r ) . 4.2.2 Types et items Les types d'Aldor ne pouvant être que des domaines ou des catégories, on distingue dans ÏÏAidor un nouveau cône inductif : TYPE Cette construction est dans C Aldor un cône limite inductive et la propriété universelle de cette limite a pour conséquence : it = cofact(id, ic) DOM CAT " \ / TYPE 4.2. Fonctions, items et types 46 f it o tc = ic \ it o td = id Exemple : Etant donné Integer un domaine des entiers en Aldor, on peut le considérer dans C Aldor comme : • effectivement un domaine, soit une flèche de 1 vers DOM : Integer 1 ^DOM C'est ce qu'il est naturellement. • un type, soit une flèche de 1 vers TYPE, en le composant : Integer 1 ^ DOM td ^ TYPE • un item, soit une flèche de 1 vers ITEM : Integer ^ DOM f- ^ — - ITEM selon l'utilisation. En particulier, si l'on désire typer un objet de base d'Aldor comme un entier, on se servira de la flèche de codomaine TYPE, par exemple pour réaliser la déclaration : x : Integer == 2 Pour passer ce domaine en argument d'une fonction, on pourra voir I n t e g e r comme une flèche de codomaine ITEM selon la déclaration de typage qui aura été inscrite dans l'écriture de la fonction appelante : f : Type-»Type == (x:Type):Type +-> E On peut alors envisager d'appliquer la fonction f à l'item I n t e g e r : f ( I n t e g e r ) . 47 4.2. Fonctions, items et types 4.2.3 Typage Le point de vue que l'on a adopté pour traduire Aldor, qui est un langage typé, impose de faire figurer dans EiAidor la notion de typage des fonctions par une flèche type de FONC verc TYPE : snn'çre TYPE FONC ainsi que celle de typage des items : TYPE t ^ZFONC V ITEM avec l'équation additionnelle : but o ij = type. 2 Exemples : • type(x) = Integer • type{f) = Type -> Type Ce typage des items a pour utilité particulière le typage des types : c'est la flèche type o it, de source TYPE et de but TYPE, qui détermine le type d'un type. 4.2.4 Satisfaction de types On sait que toute fonction et tout item ont un type unique. A ce type unique, on associe une famille de types constituée de tous les types qui le satisfont. Cette notion de satisfaction de types est à intégrer dans E Aldor • 2 On notera que type o if ^ type. 4.2. Fonctions, items et types 48 La relation de satisfaction sur les types se traduit ici comme un prédicat binaire, avec la propriété de transitivité (cf chapitre 7). On introduit l'objet SATISF, destiné à représenter les couples de types dont le premier satisfait le second. Exemple : Le type Category satisfait le type Type. Le prédicat binaire de la satisfaction de types se représente dans cette approche par une flèche satisf de source TYPE x TYPE et de but 1 + 1 (objet sommet d'un cône limite inductive dans CAidor) ' sntÀsf TYPExTYPE 1+ 1 ce qui permet de spécifier l'objet SATISF comme sommet d'un cône projectif distingué de EAidor : SATISF TYPExTYPE vrai \ /satisf 1+ 1 Une autre présentation en sera faite en 5.6, avec quelques exemples moins triviaux. 4.3. Structure de catégorie à composition faible 4.3 49 Structure de catégorie à composition faible La notion de composition abordée en début de chapitre (cf déf 4.1.1) n'est qu'une restriction de la composition en Aldor. Les fonctions sont en effet composables dès lors que le but de l'une satisfait la source de l'autre. Le cas où ces deux types sont identiques n'est donc qu'une situation bien particulière pour la composition en Aldor. L'objet des couples composables faiblement FONCCOMP de E*Aidor est donc sommet d'un cône projectif distingué, mais la base de ce cône n'est plus seulement celle qui avait été décrite précédemment pour FONCComp : FONCCOMP FONCxFONC y \ py 2 fact(but,sburcef \ ^source y TYPE \ FONC \but TYPE / TYPExTYPE 1+ 1 satisf Cette transformation s'applique de même à l'objet FONCCOMP2 pour lequel on "recopie" en deux exemplaires le cône projectif distingué précédent. On conserve une flèche de composition comp de FONCCOMP vers FONC associée à quelques équations assurant la cohérence de cette composition : étant données deux fonctions f et g composables faiblement, de composée g o f, on doit s'assurer que la source de g o f est la source de / et le but de g o f est le but de g. 4.3. Structure de catégorie à composition faible 50 Ceci peut s'exprimer plus simplement sans variables : { source o comp = but o comp = source o p2 o q but o p t o q En parallèle à la composition de fonctions, on se doit de traduire également l'application d'une fonction à un item . On introduit pour cela le nouvel objet de EAldor FONCITEMCOMP comme sommet d'un cône projectif distingué dans"EAldor' FONCITEMCOMP FONCxITEM FONC source TYPE ^vrai ITEM \type TYPE TYPExTYPE 1+1 satisf FONCITEMCOMP est en outre sommet d'un cône projectif distingué de même indexation que celui définissant FONCCOMP, on dispose donc d'une flèche de factorisation que l'on notera icf, de FONCITEMCOMP vers FONCCOMP. L'application d'une fonction à un item est ainsi traduite par la flèche comp o icj, qui retourne donc une fonction de source (). Plus précisément, on utilise une flèche itemcomp pour traduire le résultat de l'application d'une fonction à un item, la nature du résultat étant déterminée par l'analyse du corps de la fonction (cf. 7.2), et son type devant évidemment satisfaire le type-sortie de la fonction utilisée : 4.3. Structure de catégorie à composition faible 51 itemcomp FONCITEMCOMP — EXPR type v\ FONCxITEM FONC \but TYPE \vrai TYPE ITEM n TYPExTYPE 1+1 satisf satisf o fact(type o itemcomp, but o pi o q) = vrai o XFONCITEMCOMP Appliquer une fonction à un item est équivalent à composer ladite fonction avec ledit item transformé en fonction, puis à appliquer la fonction obtenue à l'item ( ) : itemcomp = itemcomp o fact^idx o XFONCITEMCOMP, fact(comp o icj, it o () o XFONCITEMCOMP)) Si / : A —> B est la fonction et x : C l'item, avec C satisfaisant A, l'item transformé en fonction est y :()—>- C, avec y() = x, et on exprime par cette équation que : (/y)() = /(») Remarque : EXPR étant sommet d'un cône inductif distingué de EAidor, on va utiliser quatre flèches toutes dénotées itemcomp, et la notion de nature en fin de document justifiera ce choix. 4.4. Structure de catégorie cartésienne FONCITEMCOM^^JtemromP 52 EXPR FONC OBJ DOM CAT L'esquisse EiAidor ainsi obtenue, et plus particulièrement la sous-esquisse traduisant l'aspect fonctionnel du langage, est une esquisse des catégories à composition faible. La partie de E Aldor s'articulant autour exprime l'aspect typé de ce langage. Une spécification plus détaillée de ce que sont les flèches de typage et la manière dont on peut les définir en fonction de flèches plus "élémentaires" seront envisageables à l'issue de ce chapitre, notamment en ce qui concerne le typage des catégories, des objets de base et des fonctions (voir chapitre 6). 4.4 Structure de catégorie cartésienne Cette section trouve son utilité dans le traitement des conversions automatiques (6.4.3) avec les fonctions prédéfinies Tuple, Cross, ( . . . , . . . ) , relatives aux uplets et aux produits de types. Tous les ingrédients présentés ici seraient nécessaires pour qui voudrait expliquer complètement dans E Aldor les régies de conversion automatique. Proposition 4.4.1 l&Aidor contient une esquisse des catégories cartésiennes. 4.4.1 Uplets de types L'enrichissement de la structure de catégorie à composition faible par l'ajout des produits nécessite au préalable de se donner les n-uplets de types (n G N). Les objets correspondants dans T&Aidor sont notés TYPEn. Les objets TYPEn sont des sommets de cônes projectifs distingués ayant pour arêtes n flèches 7rt-, 1 < i < n, de projection de TYPEn vers TYPE. 3 3 On devrait en toute rigueur y faire égalementfigurernflèchesde TYPEn vers FONC, chacune d'entre elles sélectionnant une identité, mais cesflèchesne sont pas réellement nécessaires à notre propos. 4.4. Structure de catégorie cartésienne 53 Dans CAidor^ on a de même les sommets TYPE x • • • x TYPE des cônes produits de n exemplaires de TYPE, isomorphes aux objets TYPEn par unicité de la limite projective. Plus particulièrement, TYPEi = TYPE et l'on notera ici TYPE0 pour 1, parmi ceux que l'on utilisera le plus fréquemment ;on note idj l'unique projection de TYPEi vers TYPE. TYPEQ FONC 4.4.2 Produits de deux types On introduit l'objet PRODTYPE dans E*Aidor pour représenter les produits de deux types, ou plus exactement les cônes produits de deux types. PRODTYPE est sommet d'un cône projectif distingué dans T&Aidor • PRODTYPE TYPE Z~ source ~ T ^ FONC but source o ni = 7r0 source o 7r2 = 7TQ Le constructeur de produits est symbolisé par la flèche prod de vers PRODTYPE : TYPEo _„™/ TYPE ^PRODTYPE ^ ° ^ ^ but F0NC TYPE2 4.4. Structure de catégorie 54 cartésienne D'un produit de deux types, on dispose des composantes de ce produit ainsi que de ce produit considéré comme un type simple, grâce aux trois projections : PRODTYPE TYPE2 TYPE ^^^FONC but 7C\ o prod = 7i"i 7T2 O prod = fl"2 Exemple Dans C Aldor, on a la situation suivante TYPE2 ^^^^BRODTYPE FONC sfsicType yc ^ - e r o ^ C A T BasicType 7To o prod o fact(ic o Group, ic o BasicType) est une flèche de 1 vers TYPE, c'est cette flèche qui "représente" le type noté (Group, BasicType) en Aldor, produit des deux types Group et BasicType Il est donc utilisable dans tout contexte de déclaration de type, par exemple : x : 4 (Group, BasicType) :=. . . 4 La définition de constantes n'obéit pas aux mêmes règles et leur utilisation est beaucoup plus problématique. 4.4. Structure de catégorie cartésienne 55 Il est toujours possible, à l'aide de "keyword arguments", de récupérer en Aldor les deux composantes d'un produit de types : (x : Group, y : BasicType) := ( F l o a t , Integer) L'appel de x (respectivement y) permet d'obtenir le type F l o a t (respectivement I n t e g e r ) , tout comme la flèche ni (respectivement n2) de E^/^ o r . Au produit est associée une factorisation (cf. chapitre 3) exprimée par une flèche factorise de PRODTYPE vers FONC. On ne détaille pas ici la propriété de factorisation ni les équations qui la traduisent dans l&Aidor dans le cas du produit de deux types. 4.4.3 Produit de "rien" Le cas du produit de "rien" nécessite un traitement particulier. C'est en effet un objet et non un cône non trivial, et cet objet est terminal dans toute catégorie cartésienne. On fait donc figurer dans EiAidor une flèche term de construction du produit de rien par sélection d'un type, ainsi qu'une flèche lambda qui exprime que de tout type A part une flèche ou plutôt une fonction A^ vers le type vide qui est terminal. On a de même une flèche nul qui envoie un type sur une configuration "type vide". lambda TYPEo TYPEX TYPE2 ^jpj^i^PRODTYPE nul TYPE ^^^^FONC On doit spécifier l'action de la flèche lambda par des équations supplémentaires : J source o idp o lambda 1 but o idp o lambda = = idx idx o term o nul 4.5. Structure de catégorie cartésienne fermée 56 En toute rigueur, on devrait spécifier également que la fonction sélectionnée par lambda est unique, ce qui nécessite quelques flèches et équations de plus (cf). On est maintenant en mesure de justifier l'utilisation que l'on faisait du type "vide" dans la définition des items au début de ce chapitre. La flèche ( ) : 1 -+TYPE utilisée, qui est en fait la composée :1 U DOM^TYPE, où le domaine () est une donnée de base d'Aldor, est en fait égale à id? o term, autrement dit la sélection du type produit de rien. 4.5 Structure de catégorie cartésienne fermée Cette section sera moins détaillée que la précédente puisqu'il n'existe pas en Aldor de formes prédéfinies relatives à la curryfication de fonctions, mais uniquement une forme syntaxique appropriée pour faciliter l'usage des fonctions curry fiées. Proposition 4.5.1 EAidor contient une esquisse des catégories cartésiennes fermées. 4.5.1 Exponentielle Disposant de deux types A et B en Aldor, on peut former le type A —> B par application de la fonction "—>", laquelle retourne im domaine Aldor qui est un type de fonctions. On exprime cette propriété dans EiAidor par l'ajout d'un constructeur mapping : TYPE0 TYPEX <*^^^^TYPE2 où la flèche mapping o (A, B) désigne l'objet "exponentielle de A et de 2?" au sens des catégories cartésiennes fermées. On identifie ensuite cet objet exponentiel au type produit par "—>" : 4.5. Structure de catégorie cartésienne fermée 57 idj o mapping = td o itemcomp o fact[id\ o XITEM, /act(—> O\[TEMI ^ITEM)) ° h °fl*o° prod avec TYPEo TYPEi mapping -*"^^TYPE2 prod ^ ^ PRODTYPE FONCITEMCOMP itemcomp DOM 4.5.2 Curryfication La possibilité qu'offre Aldor de curryfier toute fonction se traduit là aussi par la présence d'un constructeur de fonctions curry dans E^Aidor '> CUT7 ry FONCx idp TYPE ^Âûm:£^FONC but source o curry but o curry = ., = ., 4.5. Structure de catégorie cartésienne 4.5.3 fermée 58 Application L'aspect fonctionnel du langage Aldor s'exprime au niveau du type des fonctions, puisqu'à chaque objet exponentiel, qui est un type, on associe une fonction d'application. Cette fonction d'application, produite par un constructeur noté app dans E Aldor 5 doit en outre vérifier une équation de compatibilité avec la composition induite de E^Aidor • lambda TYPEo TYPEx TYPE2 app jprXi£^PRODTYPE nul 7TA \7T2 idp TYPE ^^"^FONC but On indique la relation entre application de fonction et existence d'une fonction d'application grâce à une équation supplémentaire, traduction au niveau esquisse de la propriété dernière du 3.8.2 : comp o fact{fuf2) = nF avec les objets et flèches suivants (FBIN désigne l'objet des fonctions d'arité 2): FBIN TYPE \ TYPE / TYPE2 \prod PRODTYPE ^12 = / a c i ( 7 r l 5 7 r 2 ) , 7T23 = / FONC but type ITEM c OBJ' DOM CAT TYPE De même que l'on a une flèche type de FONC vers TYPE, il y a également une flèche type de ITEM vers TYPE, ce qui permet ainsi de définir le type de toute expression Aldor. Le type d'une expression donnée n'est évidemment pas quelconque et la nature de l'expression détermine quels sont les catégories ou domaines utilisables pour typer cette expression. On différencie donc les types non 60 5.1. Rappels et hypothèses 61 plus seulement en catégories et domaines, qui est une différence de nature, mais également en fonction de leur utilité, autrement dit en fonction des expressions dont ils peuvent être types. On étudie dans ce chapitre la façon dont on détermine le type d'une expression identifiée, en supposant qu'une identification va de pair avec une déclaration de type. On donne en toute fin les premiers cas de satisfaction de types, ceux ne concernant que les expressions identifiées et typées par déclaration. 5.1.1 Types de première espèce Toute fonction et tout objet de base se typent par un domaine, lequel domaine ne peut être ni Type ni Category(2.6). * On parle alors de types de première espèce. Le type d'une fonction est toujours un domaine de la forme A —ï B, notons DOMF l'objet correspondant dans EiAidor aux types des fonctions. Le type d'un objet de base est un domaine qui n'est ni Type, ni Category, ni un type de fonction ; notons DOMO l'objet correspondant dans ^AidorOn note DOM1 l'objet des domaines qui sont distincts de Type, de Category et de tous les types qui sont satisfaits par Type et Category. Ainsi : DOMF A DOMO A type type FONC OBJ Les objets DOMl, DOMO et DOMF sont évidemment construits à partir de DOM, construction que l'on ne mentionne pas ici pour ne pas parasiter notre propos. On conserve juste une flèche z'i :DOMl-ïDOM. Bien souvent, les flèches type seront composées avec les flèches d'injection de DOMl, DOMO, DOMF vers DOM puis vers TYPE, mais on gardera les mêmes noms de flèches pour faciliter la compréhension. *Ni même Cross(Type), Tuple(Type), Cross(Category), Tuple(Category), et plus généralement les types qui sont satisfaits par Type et Category. 5.1. Rappels et hypothèses 5.1.2 62 Types de deuxième espèce Tous les domaines, y compris Type et Category, sont typables par les types dits de deuxième espèce que constituent les catégories et le domaine Type. On notera CAT1 l'objet de ces types de deuxième espèce. CAT1 type DOM DOMl type o ii = type Là encore CATl se détermine à partir de CAT, construction dont on ne garde comme trace que la flèche i\ : CAT-+CAT1, avec l'intention de représenter par CATl toutes les catégories ainsi que Type. Les catégories sont elles-mêmes typables, par une catégorie ou par le domaine Category ou par le domaine Type. Notons CAT2 l'objet qui a vocation, dans une interprétation ensembliste, à représenter l'ensemble des catégories et les domaines Category et Type. On peut bien entendu esquisser dans J^Aidor cette spécification de CAT2. CAT2 type CATl -CAT *i type o ii = type On a également CATl qui s'envoie dans CAT2 par ic12 : CATl -> CAT2. On utilise les types Type et Category comme de vrais domaines ou comme des types de domaines et de catégories, auquel cas on considère alors les flèches : 5.1. Rappels et hypothèses 63 CAT2 TYPE { td ° Type = td o Category = t lc o i[ o Type t\c o %2 o Category Les flèches Type et Category utilisées dans cette section le seront aux compositions avec les injections près. 5.1.3 Présentations de TYPE L'objet TYPE est donc présentable de deux manières : CAT te \ TYPE ty CAT2 5.1.4 DOM r Vu DOMl Nature d'une expression Une expression Aldor ne peut être que de nature : 1. fonction 2. objet de base 3. domaine 5.1. Rappels et hypothèses 64 4. catégorie et ceci de manière exclusive. On fait donc figurer dans Et Aldor un nouvel objet NAT ainsi qu'une nouvelle flèche nature : EXPR n ^ T NAT L'objet NAT se présente comme sommet d'un cône inductif distingué dans EtAidor et un certain nombre d'équations donnent la valeur de la composée avec nature pour des flèches de codomaine EXPR. On ne détaille pas ces éléments ici puisque seules des commutativités de diagrammes comportant l'objet NAT nous intéresseront par la suite. 5.1.5 Expressions identifiées Parmi les expressions, on distinguera celles qui sont identifiées et typées par déclaration des expressions anonymes, d'où l'ajout d'un cône inductif distingué dans E*Aidor ' EXPR (EXPRD EXPRA s> Les expressions identifiées et typées doivent être valides pour la déclaration, validité assurée par les cônes distingués suivants dans E ^ o r , pour ce qui concerne uniquement la vérification d'une satisfaction de types : EXPRD 65 5.1. Rappels et hypothèses EXPRD1 5.1. Rappels et hypothèses 66 EXPRD3 TYPExTYPE [vrai satisf 1+ 1 vrai o XTYPEXTYPE = satisf L'objet ID désigne la sorte des identificateurs d'Aldor, autrement dit toutes les chaînes de caratères à l'exception des quelques mots réservés du langage. Hypothèse principale : On ne s'intéresse pour le moment qu'à la partie des expressions qui sont identifiées et typées par déclaration. Le cas des expressions anonymes fait l'objet du chapitre 6. 67 5.2. Type cPun item Tout type déclaré pour un item est une expression valide ; tout type déclaré pour une fonction est l'application de la fonction -> à deux items qui sont des types. On ne cherchera donc à spécifier que la flèche type de EXPRD vers TYPE, via les flèches type de ITEM (respectivement FONC) vers TYPE, elles-mêmes composées des flèches type de domaine ou codomaine OBJ, DOMl, CATl, CAT2, ... 5-2 Type d'un item Exemple 1 : x : Integer = = 1 + 1 Cette instruction définit une expression identifiée et typée, où l'identificateur est x, le type déclaré le domaine I n t e g e r et le corps une application de fonction. L'item ainsi défini est même un objet de base puisque son type déclaré n'est un type ni de domaine ni de catégorie. Sa nature se détermine en étudiant l'application de fonction qui le définit (cf 7.3). Cette expression se traduit dans J^Aidor par : fact(x<...) type o fact(x,td o ix o Integer, "1 + 1") = td o ix o Integer où Integer : 1 ->D0M1. 5.3. Type d'une fonction 68 Exemple 2 : d : BasicType == I n t e g e r add{/(x : %) : % == x ;} Cette définition de constante est celle d'un item d'identificateur d, de type déclaré la catégorie BasicType, et l'analyse seule du corps permet de déduire la nature de l'item, à savoir un domaine. Pareillement, type o fact(d,tlc o i[ o BasicType,...) = t\c o i[ o BasicType, où BasicType : 1 -+CAT1. Exemple 3 : c : Category == Group with{# : % - > % ; } Le domaine Category est le type déclaré de cette expression qui est une catégorie selon l'analyse du corps de l'expression : type o fact(c,tlcoi2o Category,. ..) = tlc o i2 o Category Conclusion : Le type d'un item, lorsqu'il s'agit d'une expression identifiée et typée par déclaration, est exactement le type déclaré. 5,3 Type d'une fonction Sous les hypothèses fortement simplificatrices de ce début de chapitre, une fonction identifiée et typée par déclaration est également une flèche de 1 vers EXPRD dans EAidorExemple: f : Integer—»Integer == (x: Integer ) : I n t e g e r +-> x+1 L'identificateur de l'expression ainsi écrite en Aldor est f, le type déclaré est le domaine Integer—^Integer. Il est obtenu par application de la fonction -> au produit des domaines I n t e g e r et I n t e g e r : 2 FONC -±^<^^' 1 \ Integek TTI DOM —* TYPE ¢ 3 TYPE2 —^ PRODTYPE td 7r2 2T> L'application de —> retourne un domaine. Pr°d TYPE TTO —* ITEM U 5.4. Type d'une expression 69 Notons ( I n t e g e r , Integer) la flèche : tt o 7TQ o prod o fact(tdO Integer, tdO Integer) Si l'on voulait composer cette flèche avec la flèche type de domaine ITEM et de codomaine TYPE, puis comparer le type obtenu avec celui désigné par la flèche sourceo —y, la relation de satisfaction serait vérifiée, ce que l'on ne peut établir pour l'instant puisque la relation de satisfaction sur les couples de types n'a pas encore été spécifiée. Ainsi : fac(idi, fact(-ï, (Integer, Integer))) 1 ^FONCITEMCOMP^ ^DOMl itemcomp Le type de l'expression est alors donné par : -r—DOM i\ type o fact(f, td o ix o itemcomp o fact(idx,fact(-¥, {Integer, Integer))),...) = td o ii o itemcomp o fact(idi,fact(-+, (Integer, Integer))) C'est là aussi le type déclaré pour la fonction. 5*4 Type d'une expression A la lumière des deux paragraphes précédents, le type d'une expression identifiée et typée par déclaration est défini comme étant le type déclaré. Définition 5.4.1 type = decl 5,5 Type et profil d'une fonction Le type déclaxé d'une fonction étant toujours de la forme A —ï B en Aldor, on parle alors de profil de la fonction, puisque A et B, respectivement le type source et le type but de la fonction, déterminent complètement ce type. En outre, le type produit par l'application de -> pouvant être comparé à un type exponentiel, on obtient donc la proposition suivante : 5.6. Relation de satisfaction 70 P r o p o s i t i o n 5.5.1 Considérons la flèche type : FONC relation type = mapping o profil où profil est la flèche -* TYPE, on a la fact(source,but). On démontre cette proposition en utilisant le résultat du chapitre précédent liant l'application de —» au constructeur mapping ( 4.5.1) : type = td o itemcomp o fact{idx o XITEMJ fact(-+ oit o 7r0 o prod o fact(source, = 5.6 o\ITEM, idiTEAf)) but) mapping o profil Relation de satisfaction On s'intéresse de nouveau à l'objet SATISF de EtAidor en donnant une nouvelle façon de réaliser une flèche de codomaine SATISF. Le principe est analogue à celui donné dans le chapitre précédent, à savoir spécifier SATISF comme sommet d'un cône distingué dans E AldorL'objet SATISF est présenté dans le chapitre précédent (4.2.4) comme sommet d'un cône projectif distingué. La relation de satisfaction sur les couples de types pouvant être définie par ailleurs par dix règles exclusives, on présente également l'objet SATISF comme sommet d'un cône inductif distingué dans EtAidor cette fois, à base finie discrète : SATISF Pour 0 < i < 9, chaque objet Ri est lui-même sommet d'un cône projectif distingué, de base un graphe fini : 5.6. Relation de satisfaction 71 *' X où les objets X et Y peuvent s'envoyer sur TYPE par composition de flèches dans EAidor, ils sont donc à prendre parmi les objets TYPE, DOM, CAT, DOMl, et coetera. Dans CAidor, ces cônes distingués deviennent des cônes limites et l'on dispose alors des flèches de factorisation et de cofactorisation vers les produits et les sommes : TYPExTYPE / TYPE ... TYPE \ Ainsi SATISF (ZLÙLCtlfact...) - - ~ ^ ~ ~ ^ TYPEx TYPE fact Règle 0 Tout type domaine T satisfait T. 5.6. Relation de satisfaction 72 '-OÔM idDOM DOM DOM'^ /4dooM R è g l e 1 Le domaine E x i t satisfait tout type T de première espèce. ( E x i t est un domaine prédéfini d'Aldor, d'intérêt limité pour ce qui nous intéresse) E x i t o XDOMIXDOMI = ^"î R è g l e 2 Tout type de catégorie satisfait le type C a t e g o r y . (Pour mémoire, on a donc T satisfait C a t e g o r y s'il est "dans" CAT2) 73 5.6. Relation de satisfaction CAT2 Category o \CAT2XCAT2 = ^2 Règle 3 Tout type T de domaine ou de catégorie satisfait le domaine Type. «3 CAT2 IC\ 7T2 \ CAT2 / Tl / CATl Typ\ •--,.1 CAT2x CAT2 A Type O XcAT2xCAT2 = 7T2 Règle 4 Tout sous-type d'un type T satisfait T. Initialement, dans Axiom,, un sous-type, relativement à un domaine de base fixé, est un type dont les constantes, variables ou expressions satisfont une propriété particulière. Ceci s'écrivait également : 5.6. Relation de satisfaction 74 si T\ et T2 sont deux sous-types Relativement à un domaine de baise £>, et si tous les objets de type 7\ peuvent être déclarés également de type T2, alors T\ est un sous-type de T2 et on note 7\ ÇT 2 . Définissons maintenant une notion de sous-type en Aldor. On définit la relation C entre catégories identifiées par : Pour deux catégories identifiées C\ et C2, Ci satisfait C2 si et seulement si Ci est construite explicitement (ie nommément) à partir de C2. Exemple : C2 : Category == with { % —» Integer ; (•/.,%)->% ; Boolean ; Cl : Category == C2 with { g : (*/.,7.) -*• Boolean ; } La catégorie Ci est construite à partie de C2 et donc Ci C C2. Transcription dans EAidor • Une catégorie en Aldor est soit identifiée soit anonyme, notons CAT{ l'objet des catégories identifiées et CATa l'objet des catégories anonymes, objets de la base d'un cône inductif distingué dans EAldor - CAT *\\ CATi CATa ]:> On se restreint dans ce chapitre à C AT{, les cas relatifs à CATa seront étudiés en 6.4.1. 5.6. Relation de satisfaction 75 On a besoin d'exhiber la séquence d'exports d'une catégorie, notons SEQ l'objet correspondant dans J£ Aldor • Dans une telle séquence apparaissent des déclarations f : % —r Integer et des identificateurs de catégories C2. On présente donc SEQ comme sommet d'un cône projectif distingué dans ÏÏAldor ' SEQ '^DECLSEQ CATSEQy Le prédicat associé à la relation d'appartenance d'une catégorie identifiée à la séquence d'"exports" d'une autre se représente par une flèche € de CATx SEQ vers 1 + 1 : C2 appartient à la séquence d'exports de Cl. On est ainsi en mesure de spécifier R^ objet des couples de catégories identifiées dont la première est dans la séquence d'"exports" de la seconde: R4 CATi \ exporte SEQ \ ^ 2 -CATxSEQ vra\ v^€ . 1 +1 vrai o XCATXSEQ = € et ce cône de sommet R4 est un cône projectif distingué dans E AldorLa description de la règle 4 pour les catégories anonymes se fera en 6.4.1. Chapitre 6 Construction et type inféré d'une expression 6.1 Hypothèses principales On rappelle que toute expression est soit anonyme soit identifiée et typée par déclaration, et que toute expression a un type. La flèche type de domaine EXPR se détermine à partir des flèches de typage des expressions déclarées et des expressions anonymes. On se trouve donc dans la configuration suivante : EXPR EXPRD ™* type\ /type \ type = cofact(type, type) TYPE Cette description du typage n'est malheureusement pas "constructive" au sens où l'on n'a pas encore vu de quelle façon se construisent précisément les expressions et leurs types. C'est ce qui fait l'objet de ce chapitre avec tout d'abord l'introduction de la notion de type inféré. 76 6.1. Hypothèses principales 77 Toute expression, qu'elle soit identifiée et typée par déclaration ou anonyme, a un type inféré : EXPR EXPRD "" typevnj /typeinf/ 1 typeinf = cofact( typeinf, typeinf) TYPE Ainsi : EXPRD typeinf ^ZZ^TYPE tyPe EXPRA typeinf CZZ^TYPE type On a vu en 5.4 que pour une expression identifiée et typée par déclaration, le type est le type déclaré : type = decl. La condition de validité pour une expression identifiée et typée par déclaration est : "/e type inféré satisfait le type déclare* On définit le type inféré dans ce cas tout simple par : typeinf = type o corps Le type inféré est le type de l'expression qui définit l'expression identifiée. Pour une expression anonyme, on a : typeinf = type On va dans ce chapitre spécifier plus généralement la flèche typeinf de EXPR vers TYPE. On le fera au cas par cas en étudiant les flèches typeinf de FONC vers DOMl, OBJ vers DOMl, DOM vers CATl, CAT vers CAT2. On commencera par distinguer les deux présentations possibles d'une expression, sous forme applicative ou sous forme primitive. Cette dernière présentation nous donnera l'occasion d'introduire un certain nombre de constructeurs primitifs d'expressions Aldor, donc de donner ainsi la façon de définir initialement des termes Aldor. Dans la dernière partie, on traitera les cas restants de satisfaction de types, ceux faisant intervenir des expressions anonymes. 6.2. Expression sous forme applicative 6.2 78 Expression sous forme applicative La forme applicative d'une expression correspond en Aldor à une expression de la forme f(x) où / est une fonction et x une fonction ou un item. Cette expression peut s'utiliser comme corps d'une expression identifiée et typée par déclaration ou comme expression anonyme. On la note E par commodité et on cherche à déterminer le type inféré de E. E correspond dans EtAidor à une flèche de 1 vers EXPR qui se décompose en une composée de flèches. 6.2.1 Composée de fonctions Si / et x sont des fonctions alors elles sont composables faiblement et : typeinf FONC FONCCOMP -Cû^FONC J,x))_^^^^^^^ Cç^^TYPE \source * profKx raMin9 TYPE2 Le type inféré de la composée de fonctions est le type de la fonction composée. Les résultats des chapitres précédents avaient permis d'établir les relations type = mapping o profil ainsi que de déterminer source et but de la fonction composée. On obtient par conséquent : typeinf 6.2.2 o comp = mapping o fact(sourceop2oq,butopioq). Application d'une fonction à un item Dans ce cas précis, x est un item et désigne donc un objet de base, un domaine ou une catégorie : 6.3. Expression sous forme primitive ^ITEM 1 79 JiUt f*- FONC typeinf FONCITEMCOMP itemco ^XPR^^TYPE o itemcomp = but o pi o p2 Remarque importante : Un cas problématique est celui d'une fonction dont le type-but est Type, ou un type que satisfait Type, ou une catégorie quelconque. A priori, on ne sait pas dans ce cas si l'expression retournée est un domaine ou une catégorie. Ceci ne peut se produire avec la façon dont nous définissons l'application de fonction en y introduisant la notion de nature (voir 7.3 pour vérification). 6.3 Expression sous forme primitive Aldor dispose de primitives pour construire les fonctions, domaines et catégories : respectivement +->, add et with. On introduit ces primitives comme des constructeurs, représentés chacun dans'EAldorpar une flèche de codomaine FONC, DOM et CAT respectivement, et de domaine adéquat. Les paragraphes suivants détaillent ces constructions et le typage associé. 6.3.1 Type inféré d'une fonction On considère une fonction que l'on désigne par / , de définition : (x : A):B +-> E où A et B sont des types Aldor. Alors le type inféré de / est le domaine A —>• B. Traduisons cette propriété dans E AldorOn détermine tout d'abord le nouvel objet FONCPRIM domaine de la flèche +-> de codomaine FONC. 6.3. Expression sous forme primitive FONCPRIM 80 +-> FONC L'objet FONCPRIM est sommet d'un cône projectif distingué dans 'EAldor FONCPRIM On reviendra sur cet objet DEF dans le chapitre suivant qui détaille l'application de fonction (voir 7.3). Pour définir le type inféré d'une fonction, on impose la commutativité au diagramme suivant : FONCPRIM +-> FONC typeinf DOMF fact(qi,q2) TYPE2 itemcomp prod v PRODTYPE FONCITEMCOMP TYPE ITEM >*- -FONCxITEM 6.3. Expression sous forme primitive 81 typeinf o +-> = itemcomp o fact{\FONCPRlM? it o 7r0 o prod o fact(qi, q2))) 6.3.2 Type inféré d'une catégorie Une forme primitive de catégorie se construit avec with, E x e m p l e : with{ BasicType ; n : Integer ; l o i : (%,%)-»%} à partir d'une séquence de catégories et de déclarations de fonctions, d'objets de base ou de types. Dans EAidon with est une flèche de SEQ vers CAT : SEQ typeinf Wlth > CAT o with = tc o with Remarque : Sur l'objet CATa des catégories anonymes, en se restreignant aux formes primitives, on a typeinf = type et ce diagramme commute : CATa 6.3.3 typeinf ^ _ - ^ type idcAi% TYPE A tc CATa CAT Type inféré d'un domaine Une forme primitive de domaine se construit avec add, Exemple : Half I n t e g e r add{ id(a: : %) : % = = x } à partir d'un domaine "parent", ici Half Integer et d'une séquence de définitions de constantes (fonctions, objets de base ou types). Dans l'exemple cité, le type inféré du domaine est la catégorie : Join(with{coerce : % —KHInt$Machine) ; coerce : (HInt$Machine) - » % } , Join(Logic, OrderedFinite, OrderedRing)) with {id : % -+ %} 6.3. Expression sous forme 82 primitive On explicite la construction d'une forme primitive de domaine add DOMPRIM DOM en distinguant dans EiAidor le cône projectif suivant : DOMPRIM parent \impl DOM EXPRDSEQ où EXPRDSEQ désigne l'objet des séquences d'expressions identifiées et typées par déclaration. Pour déterminer le type inféré d'un domaine à partir d'une forme primitive : add DOMPRIM it DOM \impl EXPflDSEQ typeseq typeinf -CAT SEQ TYPE with typeinf o add = tc o w i t h o fact(...) où fact est une flèche de factorisation de DOMPRIM vers SEQ dans CAidor et typeseq une flèche de EXPRDSEQ vers DECLSEQ que l'on décrit maintenant : 6.4. Extensions de la relation de satisfaction EXPRDSEQ typeseq 83 DECLSEQ EXPRDxEXPRDSEQ EXPRD nom aecO^ ID TYPE TYPE DECLxDECLSEQ DECL patron \ident TYPE ID Remarque : On a utilisé dans cette construction le type du domaine "parent", qui est en général une catégorie sauf dans le cas où il se type en type. Dans cette situation très particulière, on considère alors le type inféré de la forme primitive initiale (voir ch. 7) du domaine "parent". Cette distinction de cas peut tout à fait se traduire dans le cadre de l'esquisse I&Aidor en ajoutant un cône inductif distingué. 6.4 Extensions de la relation de satisfaction On traite dans cette section des cas de satisfaction de types non abordés au chapitre précédent, ceux-ci concernant des types non forcément identifiés. 6.4.1 Satisfaction de catégories La règle générale est toujours la même (voir règle 4) : Règle 5 Tout sous-type dJun type T satisfait T, Elle était utilisée dans le contexte des catégories identifiées au 5.6, et l'on est maintenant en mesure de la compléter dans le contexte des expressions anonymes. 6.4. Extensions de la relation de satisfaction 84 Pour deux expressions de catégorie Ci et C2, on note Ex(Ci) et Ex(C2) l'ensemble des symboles exportés par chacune de ces deux catégories, et on a, relativement au domaine de base C a t e g o r y : Ci C C2 <=ï Ex(Ci) D Ex(C2) ainsi une expression de catégorie est un sous-type d'une autre si elle exporte plus d'opérations. Exemple : C2 ==> w i t h { f : % -> I n t e g e r ; + n Boolean ; } Cl ==> w i t h { % -* I n t e g e r ; f (%,%) - > X ; + Boolean ; n (%,%) -» B o o l e a n ; g } Alors Ex{C2) =< f : % - ^ I n t e g e r , + : (%,%)-> °/„ n : Boolean>, et Ex{Ci)= I n t e g e r , + : (% f X)->X,n : Boolean,g : (%,%)Boolean>. On vérifie que Ex{d) D Ex(C2) donc l'expression de catégorie C\ est un sous-type de l'expression de catégorie C2. Transcription dans l&Aidor ' On introduit pour ce nouveau cas de satisfaction l'objet /2 5 des couples de c a t é g o r i e s a n o n y m e s dont la première satisfait la seconde. 6.4. Extensions de la relation de satisfaction CATa exporte2 \ SEQ 1 * vra\ 85 CATa ^ \exporte2 SEQ SEQxSEQ ysincl ^ 1+ 1 vrai o XSEQXSEQ = ind La condition porte sur une vérification de l'inclusion des séquence d'exports. Elle n'est pets détaillée mais apparaît sous la forme d'une flèche de prédicat incl. Pour la définir rigoureusement dans 'EAldor^ il faudrait passer de la structure de séquences pour les exports à la structure d'ensembles afin de vérifier l'inclusion. Ce n'est pas l'objet de notre travail. On définit également la satisfaction d'une catégorie identifiée à une catégorie anonyme, en considérant uniquement l'expression qui définit la catégorie identifiée, c'est une catégorie anonyme (si sous forme primitive mais on peut toujours s'y ramener). Si Ci est une catégorie identifiée et C2 une expression de catégorie alors Ci E C2 «=> Ex(Ci) D Ex(C2) puisque l'on définit également la liste des "exports" d'une catégorie identifiée, c'est la liste des symboles exportés de l'expression qui la définit : Ci : Category — E où E est une expression de catégorie ; on pose Ex(Ci) = Ex(E). Exemple : 6.4. Extensions de la relation de satisfaction 86 C2 ==> with { 7o - • I n t e g e r ; f + (%,X) ->•/• ; Boolean ; Cl : Category == with { f : y. -> Integer ; } + ('/.//•) - > % ; n g Boolean ; (%,%) -» Boolean ; Ci est une catégorie identifiée, ici une constante, et Ex(Ci) = < f : %->Integer, + : (0/o,°/o)-+% n : Boolean, g : (%,°/0)-+ Boolean>. Donc Ex(Ci) D Ex(C2) et la catégorie Ci est un sous-type de l'expression de catégorie C2. Transcription dans E Aldor • Ce nouveau cas est représenté par un nouvel objet Rsbis dans EAidor-, lui aussi sommet d'un cône projectif distingué : 6.4. Extensions de la relation de satisfaction 11 EXPRD -^-CATa corps y ! = y corps EXPÉD **—CATa ! exporte2 \ ! SEQ CATa CATa \exporte2 SEQ *"i -SEQxSEQ \ vrà\ incl 1+1 vrai o XSEQXSEQ = i>ncl 6.4.2 Satisfaction au type "vide" Règle 6 Tout type T satisfait le type ( ). 6.4. Extensions de la relation de satisfaction td 6.4.3 O ( ) O XTYPEXTYPE 88 = 7T2 Conversions automatiques La règle générale est la suivante : Règle 7 Un type Ti satisfait le type T2 s'il existe une conversion "automatique" de Ti vers T2. On se contentera dans une première approche de donner trois cas de satisfaction issus de la règle générale. Sous-règle 71 Tout type de première espèce T satisfait le type de première espèce Tuple(T). La fonction Tuple d'Aldor s'applique à un argument dont le type satisfait Type. Traduite dans E ^ o r , cette sentence exprime que T est une flèche de 1 vers DOMl. On considère alors le cône projectif distingué suivant dans E»Aidor ' Sous-règle 72 Tout type de première espèce T satisfait le type de première espèce Cross(T). 6.4. Extensions de la relation de satisfaction 89 La fonction Cross d'Aldor s'applique à un argument dont le type satisfait Tuple(Type). Ceci signifie que T est représentable dans E Aldor par une flèche de 1 vers DOML Ainsi cette deuxième sous-règle donne lieu à la construction suivante dans EiAldor - et ce cône projectif est distingué dans E AldorSous-règle 73 Tout type de première espèce Cross(T) satisfait le type de première espèce T. On a donc : 6.4. Extensions de la relation de satisfaction 90 L'objet représentatif de cette règle de satisfaction de types est l'objet # 7 , sommet d'un cône inductif distingué dans EiAidor : '*. R~i 6.4.4 R'72 R?c Compatibilité avec —> La relation de satisfaction est compatible avec l'application de la fonction —> d'Aldor aux sous-catégories. Règle 8 Soient deux couples de catégories identifiées (Si,S2) et (Ti,T2), où S2 satisfait Si et 7\ satisfait T2, alors Si —r î \ satisfait S2 —• T2. On introduit un nouvel objet Rs de EiAidor pour figurer cette satisfaction de types, toujours comme sommet d'un cône projectif distingué dans E^/dor, et cet objet est à ajouter à la somme des configurations de satisfaction dans E Aldor pour définir convenablement SATISF : 6.4. Extensions de la relation de satisfaction 91 9i DOMl DOMl FONCITEMCOMP FONCxITEM PRODTYPE prod TYPE2 TYPE CA TYPE TYPE CAT CAT CAT CATi CATi CATi TYPE ! CATi q2 \ ^ A-, Dans cette présentation on a considéré des catégories identifiées, mais en toute généralité Si, S 2 , . . . ne sont pas forcément des catégories identifiées mais peuvent être de la forme Si = S[ -r T[, etc. Il faudrait alors décrire cette règle sous une forme récursive, ce qu'il est tout à fait possible de faire mais cela n'ajouterait pas à la clarté du propos. Nous nous en dispensons donc. La réciproque est également vraie, si Si —r 7\ satisfait S2 -> T2 alors S2 satisfait Si et 7\ satisfait T2. 6.4. Extensions de la relation de satisfaction 6.4.5 92 Satisfaction induite par Join Parmi les fonctions prédéfinies d'Aldor, à l'instar de ->, Tuple, Cross, il existe une relation de satisfaction particulière pour la fonction Join : Join (A : Category, B : Category) : Category == with Bien qu'il n'y ait rien dans le corps de la fonction qui indique un héritage quelconque de catégories puisque la séquence d'exports est a priori vide, une catégorie créée par l'application de Join a pour exports la réunion des exports des catégories en arguments. On obtient donc un cas de satisfaction supplémentaire : Règle 9 Si Ci et C2 sont deux catégories, alors la catégorie satisfait C\ et C2. Join(Ci,C2) Notons RQ l'objet représentatif de ce dernier cas de satisfaction de types, il est sommet d'un cône inductif distingué dans E*Aidor • '„ #91 où #91 et i?92 sont eux-mêmes sommets de cônes projectifs distingués dans EiAldor ' 93 6.4. Extensions de la relation de satisfaction CAT EXPR A itemcomp FONCITEMCOMP TYPE FONCxITEM ""t Join> -FONC ITEM TYPE -PRODTYPE 7T0 6.4. Extensions de la relation de satisfaction 94 Chapitre 7 Application, héritage et appartenance 7.1 Introduction On revient dans ce chapitre sur des spécificités du langage Aldor, abordables après avoir défini le type de toute expression. On a vu notamment au cours des chapitres précédents que dans un contexte où T est Type ou une catégorie quelconque, a priori une instance de x pourrait être un domaine ou une catégorie si on ne fait appel qu'à une vérification de satisfaction de types. On montre ici, surtout dans un contexte d'application de fonction puisque c'est là que les vérifications sont les plus fortes en Aldor, que la notion de nature permet de lever cette ambiguité. 7.2 Compatibilité entre type et nature Toute expression du langage Aldor possède un type et une nature. Dans un contexte de déclaration x : T, on doit s'assurer évidemment que le type d'une instance de x est en relation de satisfaction avec T. 95 7.2. Compatibilité entre type et nature 96 Mais dans un contexte x : T == E, on doit en outre s'assurer que le type requis pour une instance de x, ici T, est compatible avec la nature requise pour une instance de x par l'expression E. Exemple : f : Considérons la fonction Category -> Category == (c : Category) : Category +-> c with { g :%->%} c doit être de nature une catégorie (à cause du constructeur de catégories with)et donc de type un type qui satisfait Category. Or le type Category de la déclaration est compatible avec toute expression instance de c (qui est une catégorie) puisque le type Category peut typer une catégorie, donc le typage est satisfaisant (idem pour le type de sortie de la fonction). On traduit cette compatibilité par l'ajout d'une flèche compatible dans EtAldor : TYPExEXPR définie par les équations : compatible, ± + 1 7.3. Retour sur la définition de fonction 97 compatible TYPExEXPR 1+1 aux DOMOxOBJ compatible o fact(di °Pi, Ci o i0 op2) = vrai o XDOMOXOBJ compatible o fact(d2opi,ef o p2) = vrai o XDOMFXFONC compatible o fact(ci o p 1? e:- o id o p 2 ) = vrai o ACMTIXDOA/ compatible o fact(c2 o pi, e2- o zc o /¾) = vrai o \CAT2XCAT et par complémentarité on obtient les équations qui définissent la non-satisfaction de la relation de compatibilité. 7.3 Retour sur la définition de fonction Exemple : f : Considérons la fonction Category -> Category == (c : Category) : Category +-> c with { g :%^%} représentable dans CA[dor par une flèche de 1 vers FONC. L'identificateur f et le type Category -» Category sont eux représentables par des flèches de 1 vers ID et vers TYPE respectivement. 7.3. Retour sur la définition de fonction 98 Le terme de droite définissant la fonction est une forme primitive de fonction, utilisant la primitive +->, on s'intéresse à traduire le "terme paramétré" qui détermine le corps de la fonction. Comme terme ouvert, autrement dit avec variable dans une écriture classique, c'est a priori une flèche de EXPR vers EXPR dans CAidorOn peut même préciser qu'il s'agit ici d'une flèche de CAT vers CAT uniquement d'après le typage, ce qu'il n'est pas toujours possible de faire. With SEQ DECLSEQ g \ > CAT CATSEQ S\ 1 %ÇAT \ CAT Le terme ouvert correspond à la flèche with o fact(g o XCATSEQ ° icAT, icAr) de CAT vers CAT. Il reste à intégrer cette flèche dans la définition d'une fonction telle qu'elle est présentée par l'objet FONCPRIM et le cône projectif distingué qui lui est associé. Précisément il s'agit de former une flèche de 1 vers DEF pour obtenir le corps d'une fonction. Afin d'assurer l'existence d'une telle flèche, la propriété utilisée est celle d'esquisse généralisée, avec la construction des objets exponentiels et les mécanismes de curryfication et d'application. On précise alors la base du cône inductif distingué de sommet DEF dans E Aldor par un graphe fini discret : DEF 7.3. Retour sur la définition de fonction 99 où les objets X et Y sont à prendre parmi OBJ, DOM, CAT et FONC Si l'on note fparam la flèche with o fact(g o XCATSEQ ° icAT, icAr) alors on a également dans C Aldor sa curryfiée fparamc codomaine CATCAT. On obtient bien ainsi une flèche de 1 vers DEF. de domaine 1 et Il reste à ajouter dans la base de FONCPRIM les conditions qui font de cette définition une définition de primitive de fonction valide, en termes de compatibilité notamment. 7.3. Retour sur la définition de fonction 100 FONCPRIM TYPE TYPE DEF EXPREXPR x EXPR x EXPR 7 *j EXPR EkPR EXPR EXPR -TYPExEXPR vrai compatible ?L + 1 compatible = vrai o XTYPEXEXPR Ayant maintenant défini une fonction, ie une flèche de 1 vers FONC en composant avec +->, on montre que la condition requise pour CAidor permet de déterminer complètement la flèche itemcomp de FONCITEMCOMP vers EXPR, introduite au paragraphe 4.3. 7.4. Application d'une fonction à un item 7-4 ICQ Application d'une fonction à un item On revient dans ce paragraphe sur la définition de l'application de fonction, amorcée auparavant avec la définition du cône distingué de sommet FONCITEMCOMP. Pour parler d'application, on se donnait une fonction et un item dans une configuration de vérification de types. Il s'agit maintenant d'évoquer le passage des paramètres, où l'on s'aperçoit que la vérification de la relation de satisfaction sur les types est insuffisante pour assurer la validité d'une application. 7.4.1 Première condition Reprenons la fonction f de l'exemple précédent, la flèche associée fparam est une flèche de CAT vers CAT. Elle représente une expression contextuelle et sa composée avec toute flèche de 1 vers CAT représente alors une catégorie d'Aldor. Il s'avère donc nécessaire pour composer et obtenir une expression d'Aldor, de conditionner initialement la nature de l'argument, à savoir une catégorie dans le cas présent. Cette condition exprime que la nature de l'argument éventuel doit être identique à celle requise pour la définition de fonction, autrement dit le diagramme ci-dessous est commutatif : 7.4. Application d'une fonction à un item 102 FONCITEMCOMP FONCxlTEM 2 P ITEM FONC yprvm u EXPR FONCPRIM DEF nature EXPREXPR x EXPR x EXPR 7Tb EXpR 7.4.2 nature NAT Seconde condition La composition étant rendue possible au sens catégorique, il faut s'assurer qu'elle l'est également au sens d'Aldor, ie à une satisfaction de types près. Cette condition est obtenue par la structure de catégorie à composition faible définie au chapitre 4. 7.4.3 Justification de l'application Dans la définition d'une catégorie à composition faible, une flèche itemcomp de FONCITEMCOMP vers EXPR traduit l'obtention d'une expression à partir d'une fonction et d'un argument. On peut maintenant justifier que l'on dispose naturellement d'une telle flèche. Elle provient de la structure d'esquisse généralisée imposée à E ^ o r , où l'on dispose nturellement des flèches d'application de BA x A vers 2?, pour tous objets A et B. 7.4. Application d'une fonction à un item 103 Démonstration par l'exemple (toujours avec la fonction f ) dans CAidor '• FONCITEMCOMP — l t e m c o m P EXPR A FONCxLTEM P. ITEM FONC Iprim FONCPRIM DEF I EXPR FONC OBJ DOM CAT A CATCAT x CAT x CAT CATCAT -CATCAT x CAT ^CAT 3appcAT,CAT Pour une démonstration complète, les flèches appcAT,CAT, appcAT,DOM, etc liées à chacun des objets Yx x X x Y dans la base du cône issu de DEF, permettent de construire un cône de base discrète FONC,OBJ, DOM, CAT, ie de même base que le cône issu deEXPR. On obtient ainsi par factorisation et cofactorisation dans CAldor une flèche de FONCITEMCOMP vers EXPR, celle que l'on avait notée auparavant itemcomp. Il est à noter que la condition sur le type du résultat de l'application de fonction a été donnée au chapitre 4, conjointement à celle sur le type de l'argument. 7.5. Perspectives 104 7.5 Perspectives 7.5.1 Autre point de v u e sur l'application et la composition On se propose ici de donner une présentation légèrement différente de la composition de fonctions. Par constructions dans C Aldor, en utilisant uniquement les propriétés des cônes limites, on va présenter la composition de fonctions comme une composée de flèches consécutives dans C^idor (au sens catégorique). Il est à noter que cette présentation de la composition englobe l'application d'une fonction à un item puisque l'on a vu que, grâce à la flèche if, un item peut se concevoir comme une fonction. Notion de "trace" Etant donnés deux types A et B, ie deux flèches de 1 vers TYPE, on a dans C Aldor la flèche de factorisation correspondante vers TYPE2, notons la (A, B). A cette flèche de 1 vers TYPE2, on associe un objet, appelé "trace" de A et B et noté TR(A, J9), sommet d'un cône limite projective dans CAidor TR(A,B) / f { 1 STYPE As v \sou*ce FONC ) ^X /but y ~ - - TYPE- - ' ' ' Dans un modèle ensembliste, l'objet TR(A, B) s'interpréterait comme l'ensemble des fonctions de source A et de but B, ou plus simplement Hom(A, B). Dès que l'on dispose de deux fonctions Aldor f : A -* B et g : C —ï D, où le type C satisfait le type B, on dispose également dans C^Aidor des deux 7.5. Perspectives 105 objets TR(A, B) et TR(A, D). Comme J&Aidor est en particulier une esquisse des catégories, on va mettre en évidence dans C^idor l'existence d'une flèche TR(g, C, D) de TR{A, B) vers TR(A, D) et qui traduit effectivement un changement de types sous l'action de g (en composant par la fonction g, on va passer du type B au type D). La flèche TR(g, C, D) existe dès que l'on a une flèche trans convenable : rBG4,BW----?-'-r-^->-« ,( 1 "X . r AS TR(A, D) TYPE \sov*ce FONC ^\, /but ^--..TYPE __--^' TYPE On prouve l'existence de trans en utilisant les propriétés de factorisation et de cofactorisation des cônes limites dans C Aldor- 7.5.2 Notion d'héritage On a un héritage direct entre deux catégories si ces deux catégories sont en relation de satisfaction en tant que types, au sens de la règle R4. On étend alors la notion d'héritage à d'autres catégories en utilisant la transitivité de la relation de satisfaction avec les autres cas de satisfaction entre catégories. L'héritage entre catégories peut ainsi se traduire uniquement en termes de satisfaction de types dans CU/ S ; 7.6. Conclusion 107 denom %-+S ; numerator % -> % ; denominator % -+ % ; if S has StepThrough then StepThrough ; if S has RetractableTo Integer then {RetractableTo Integer ; RetractableTo Fraction Integer ; } if S has EuclideanDomain then {wholepart : % -» S} } Remarque : Lorsque l'on teste une propriété d'un domaine dans une conditionnelle, on teste en fait la partie exportée par ce domaine, et le relation nouvellement introduite entre les deux catégories n'est plus un héritage de construction (par un enrichisssement de type "with"), mais de conception. Ici aussi le cadre des esquisses que l'on a choisi se révèle être particulièrement bien adapté puisque une conditionnelle s'exprime à l'aide d'une cofactorisation dans la théorie des esquisses. C'est cette propriété que l'on utilisera dans CAidor, sur des types, avec le prédicat d'appartenance dont on vient de voir que la définition pouvait se faire en termes de satisfaction de types. 7.6 Conclusion Le point crucial de ce travail consiste à remarquer que, pour avoir voulu élever le niveau de description des types, Aldor a introduit ce faisant une ambiguité, qui ne peut pas être levée par des considérations de typage. Si la plupart des langages informatiques typés arrivent à décrire une expression par son type, il y a en revanche peu ou pas de satisfaction de types. En Aldor on a à la fois une satisfaction de types non triviale et des types qui sont valeurs de premier ordre. La contrepartie de cette complexité est paradoxalement une perte de richesse expressive des types et une vérification de validité des expressions qui se décompose donc en deux vérifications distinctes : 7.6. Conclusion 108 x : T == E 1. Le type de x doit satisfaire T. 2. Le type T doit être compatible avec la nature de E. L'introduction de la notion de nature dans le système de typage d'Aldor permet certes de répondre au besoin de vérification de validité d'expressions, mais elle a également l'avantage de préciser le procédé d'évaluation d'un programme Aldor. Un programme Aldor, dans notre formalisme, est une flèche dans CAidor de domaine 1. C'est une composée de flèches élémentaires et tout le problème de l'évaluation consiste à la réduire en une flèche "équivalente" dans CAidorOn utilise entre autres des mécanismes de factorisation et cofactorisation. Le point problématique en Aldor est celui d'une flèche arrivant dans EXPR par application d'une fonction à un item (itemcomp). On ne sait pas a priori décider, en termes de typage, si l'on arrive dans EXPR par les objets de base, les fonctions, les domaines ou les catégories. C'st la donnée de la nature, déterminée par le corps de la fonction, qui résout le problème d'indécision. Ceci est obtenu par le fait qu'il n'y a qu'un nombre fini de constructeurs en Aldor pour les expressions sous forme primitive, et que chacun correspond à une nature déterminée. L'esquisse EtAidor est donc quasi-projective. Bibliographie [1] P. Ageron. Sémantique catégorique des types : comprendre le système F, Diagrammes 19 (1988) [2] M. Barr, C. Wells. Catégories theory for Computing Science, Prentice Hall (1990) [3] D. Bert, R. Echahed, P. Jacquet, M.L. Potet, J.C. Reynaud. Spécification, Généricité, Prototypage : Aspects du langage LPG , Technique et Science Informatiques, TSI (1995) 9(14) 1097-1129 [4] L. Coppey, C. Lair. Leçons de théorie des esquisses (I), Diagrammes 12 (1984) [5] L. Coppey, C. Lair. Leçons de théorie des esquisses (II) , Diagrammes 19 (1988) [6] D. Duval, J.C. Reynaud. Sketches and Computation I : basic définitions and static évaluation , Math. Struct. in Comp. Science, Cambridge University Press (1994) vol 4 185-238 [7] D. Duval, J.C. Reynaud. Sketches and Computation II : dynamic évaluation and applications , Math. Struct. in Comp. Science, Cambridge University Press (1994) vol 4 239-271 [8] C. Ehresmann. Esquisses et types de structures algébriques , Bulletin de l'Institut Polytechnique, Iasi 14 (1968) [9] J.A. Goguen, J.W. Thatcher, E.G. Wagner. An initial algebra approach to the spécification, correctness, and implementation of abstract data types , Current Trends in Programming Methodology, Vol. IV : Data Structuring, R.T. Yeh éd., Prentice Hall (1978) 80-149 109 Bibliographie 1K [10] R. Guitart, C. Lair. Calcul syntaxique des modèles et calcul des formules internes , Diagrammes 4 (1980) [11] R. Guitart, C. Lair. Limites et colimites pour représenter les formules , Diagrammes 7 (1982) [12] Hudak, Jones, Wadler. Report on the programming language Haskell : a non-strict, purely functional language , ACM SIGPLAN Notices (1992) 27(5) [13] R. Jenks, R. Sutor. AXIOM The Scientific Computation Springer (1992) System, [14] J.L. Krivine. Lambda-calcul : types et modèles, ERI Masson (1990) [15] R. Lalement. Logique, réduction, résolution, ERI Masson (1990) [16] S. Mac Lane. Catégories for the working mathematician, Springer (1971) [17] S.K. Lellahi. Categorical abstract data types , Diagrammes 21 (1989) [18] Milner. A proposai for Standard ML , Proc. of the Symposium on Lisp anf Functional Programming, ACM (1984) 184-197 [19] S. Watt,R. Sutor, P. Broadbery, S. Dooley, P. Iglio, S. Morrison, J. Steinbach. AXIOM Library Compiler - User Guide, IBM Thomas J.Watson Research Center, The Numerical Algorithms Group Limited Table des matières Typage 1.1 Les langages fonctionnels 1.2 Les langages algébriques - LPG 1.3 Exemple du langage Haskell 1.4 Quelques spécificités d'Aldor 7 7 10 11 13 Les types d'Aldor 2.1 Expressions d'Aldor et types 2.2 Fonctions et objets de base 2.3 Satisfaction de types 2.4 Types-domaines et types des domaines 2.5 Types-catégories et types des catégories 2.5.1 Catégories comme types de domaines 2.5.2 Types des catégories 2.6 Domaines et catégories comme types 2.7 Présentation graphique 15 15 16 17 17 18 18 20 20 22 Esquisses 3.1 Graphes à composition 3.2 Catégories 3.3 Foncteurs 3.4 Cônes 3.5 Esquisses 3.6 Limites projectives et inductives 3.7 Modèle 3.8 Catégorie cartésienne et cartésienne fermée 3.9 Catégorie-type 23 25 27 28 29 32 34 35 36 38 111 112 4 Une interprétation d'Aldor en termes d'esquisses 4.1 Structure de catégorie 4.2 Fonctions, items et types 4.2.1 Fonctions et items 4.2.2 Types et items 4.2.3 Typage 4.2.4 Satisfaction de types 4.3 Structure de catégorie à composition faible 4.4 Structure de catégorie cartésienne 4.4.1 Uplets de types 4.4.2 Produits de deux types 4.4.3 Produit de "rien" 4.5 Structure de catégorie cartésienne fermée 4.5.1 Exponentielle 4.5.2 Curryfication 4.5.3 Application 41 . 42 44 44 45 47 47 49 52 52 53 55 56 56 57 58 5 Typage d'une expression par déclaration 5.1 Rappels et hypothèses 5.1.1 Types de première espèce 5.1.2 Types de deuxième espèce 5.1.3 Présentations de TYPE 5.1.4 Nature d'une expression 5.1.5 Expressions identifiées 5.2 Type d'un item 5.3 Type d'une fonction 5.4 Type d'une expression 5.5 Type et profil d'une fonction 5.6 Relation de satisfaction 60 60 61 62 63 63 64 67 68 69 69 70 6 76 76 78 78 78 79 79 Construction et type inféré d'une expression 6.1 Hypothèses principales 6.2 Expression sous forme applicative 6.2.1 Composée de fonctions 6.2.2 Application d'une fonction à un item 6.3 Expression sous forme primitive 6.3.1 Type inféré d'une fonction 113 6.3.2 Type inféré d'une catégorie 6.3.3 Type inféré d'un domaine 6.4 Extensions de la relation de satisfaction 6.4.1 Satisfaction de catégories 6.4.2 Satisfaction au type "vide" 6.4.3 Conversions automatiques 6.4.4 Compatibilité avec —> 6.4.5 Satisfaction induite par Join 81 . 81 83 83 87 88 90 92 Application, héritage et appartenance 95 7.1 Introduction 95 7.2 Compatibilité entre type et nature 95 7.3 Retour sur la définition de fonction 97 7.4 Application d'une fonction à un item 101 7.4.1 Première condition 101 7.4.2 Seconde condition 102 7.4.3 Justification de l'application 102 7.5 Perspectives 104 7.5.1 Autre point de vue sur l'application et la composition . 104 7.5.2 Notion d'héritage 105 7.5.3 Notion d'appartenance 105 7.5.4 Les conditionnelles 106 7.6 Conclusion 107