D IAGRAMMES P IERRE AGERON Sémantique catégorique des constructeurs de types d’ordre supérieur Diagrammes, tome 22 (1989), p. 31-44 © Université Paris 7, UER math., 1989, 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 ACTES DES JOURNEES CUNIV. PARTS 7. 22 , 1939 E.L.I.T. 27 JUIN—2 JUILLET 1988) SEMANTIQUE CATEGORIQUE DES CONSTRUCTEURS DE TYPES D'ORDRE SUPERIEUR Pierre AGERON ÀBSTRÀCT. We describe a new categorical framework for the semantics of polymorphic type theory. Its two main features are : - variable types are mère maps rather than functors - the type Vx.A(X) is the solution of a small inductive universal problem instead that of a big projective one. For this purpose, we introduce abstract "type syntaxes", in the spirit of Ehresmann's sketches, and study their semantics. We get a quite gênerai resuit of algebricity (tripleability). 1 - QU'EST-CE QU'UN TYPE DANS UNE CATEGORIE ? Pourquoi choisir le langage de la théorie des catégories pour parler de types? Un argument de départ peut être le suivant. La notion de type est intuitivement peu différente de celle d'ensemble; or chaque catégorie est une sorte de variante de la théorie des ensembles: il est alors normal de chercher à faire vivre les types dans certaines catégories convenables. La catégorie Ens n'est alors plus qu' une catégorie parmi les autres, sémantiquement adaptée ou non au type ou système de types considéré. r*çu le 04/09/1989 Voici les questions de fond que nous allons discuter: a) Qu'est-ce qu'un type A dans une catégorie Z ? b) Qu'est-ce qu'un terme fonctionnel de type A=>B ? L'idée la plus simple qui vienne à l'esprit, c'est de considérer que les types sont des objets de C, un terme de type A=>B étant alors une flèche de A vers B. Ce point de vue impose de se donner arbitrairement un certain nombre de types de base, à partir desquels les autres types sont construits par produits, exponentielles, sommes;... On retrouve ici les limitations d'expressivité du lambda-calcul typé ordinaire de Curry-Church, dans lequel il n'est pas possible de manipuler les types de données courants (booléen, entier, liste, etc.)- à moins de les considérer comme des types atomiques et d'introduire pour chacun d'eux de nouveaux schémas non-logiques. C'est précisément l'intérêt du système F, ou lambda-calcul typé du deuxième ordre de Girard ( [1]), que d'échapper à l'atomicité, tout en restant purement logique (c'est la version fonctionnelle du calcul propositionnel intuitionniste du deuxième ordre). Dans ce système, comme dans d'autres voisins, il n'y a plus de types de base: tous les types y sont construits, conformément à leur "géométrie" intrinsèque. Ceci est rendu possible par la considération de types variables, c'est-à-dire de types où figurent librement des variables de type : X,Y,... Pour alléger, les types que nous écrirons comporteront au plus une variable libre. Si A(X) est un tel type, on peut construire le type ~X.A(X), dans lequel X est muette. L'étude sémantique devra statuer sur le point de savoir c) Quelle est la construction qui fait variable A(X) au type clos Vx.A(X) ? passer d'un type Dans un premier temps, il est extrêmement tentant d'admettre que les types variables A(X) sont certains foncteurs A : C -> C , qu'un terme fonctionnel de type A(X)=>B(X) est une transformation naturelle de A vers B, et que le type clos VX.A(X) est la limite projective Limproj A(X) ( certains ont pensé aussi, mais xeC ceci semble moins naturel, au produit 'j,r A(X) :^ 32 ) Or cette belle simplicité ne tient pas la route. D'abord, imposer la covariance de tous les types variables est excessif: il faut pouvoir séparer occurrences négatives et positives d'une même variable par rapport au constructeur =>. Quant aux "gros" produits, leur existence est en général fort problématique. Certains auteurs ont cependant pu établir une sémantique sur ces bases "fonctorielles", au prix d'astuces peu convaincantes: travailler avec des catégories internes (Seely, Pitts), supposer que tous les morphismes sont des monomorphismes, ou jouer avec deux sortes de morphismes (Girard, Coquand, Lamarche, Taylor). Dans un deuxième temps est venue (Freyd, Girard, Scott, Scedrov) l'idée de dédoubler chaque variable de type X en g d , X et X , donc d'opter pour une représentation "schizophrène" du type variable A(X) par un bifoncteur A : C •-: C -> C . Les termes fonctionnels devenaient alors des transformations dinaturelles, et le type clos Vx.A(X) était la fin projective /A(X,X) du bifoncteur A. Mais on se heurta rapidement à une difficulté grave: contrairement aux transformations naturelles, les transformations dinaturelles ne se composent pas. Il devenait en général impossible de substituer un terme dans un autre. Ajoutons aussi qu'un tel formalisme ruine tout espoir d'algébricité, de présentation équationnelle, etc.: quoi qu'on y fasse, 'Z n'est pas "Z à la puissance op" ! Très récemment, Freyd, constatant que les notions classiques se révélaient inadéquates, a été amené, pour interpréter le système F, à définir de nouvelles notions de "théorie générale des catégories": celles de structeur, de transformation structurelle, et de liaison structeur. Ses premiers résultats ([2]) . sont projective très d'un intéressants Un point commun à tous ces formalismes est de définir le type VX.A(X) comme la solution d'un "gros" problème universel de nature projective. Or il y a une sorte de principe en théorie des catégories qui veut qu'un tel problème soit équivalent à un "petit" problème universel de nature inductive. Par exemple, l'objet initial d'une catégorie peut être vu indifféremment comme la limite projective de "tout" ou la limite inductive de "rien". Autre exemple: la dualité de Stone-Weierstrass permet de ramener, du point de vue des modèles, l'étude des petites esquisses inductives à celle de grosses esquisses projectives. Ce principe justifie l'idée, proposée en [3], d'aborder la sémantique des types par le versant inductif, d'autant plus que celui-ci est le seul à avoir une représentation informatique. Il reste à espérer un jour un énoncé précis faisant la jonction entre les deux points de vue (le théorème 1-6 de [2], établissant un lien entre "liaison projective" et "algèbre initiale", est un pas important dans cette direction). Dans [3], l'idée de départ était celle, défendue depuis longtemps par l'"école d'Ehresmann" (voir par exemple [6]), qui consiste à prendre au sérieux la structure interne des types. Autrement dit, on cesse d'assimiler un type clos à un seul objet de € , pour le voir plutôt comme un diagramme dans Zt figurant tous les domaines auxiliaires, fonctions de. construction, fonctions d'accès, etc. nécessaires à sa définition. Evidemment, les différents objets et flèches de ce diagramme ne sont pas indépendants, et il nous faut trouver un moyen de spécifier formellement les liens qui existent entre eux. Si ces liens étaient tous de simples limites projectives ou inductives, on pourrait utiliser des esquisses. Mais pour spécifier aussi des propriétés universelles plus complexes, car à plusieurs étages (comme celles définissant une exponentielle ou un objet des entiers naturels), il nous faut recourir à une notion d'esquisse généralisée, comme celle de trame ([4]), ou celle, plus souple encore, et qui s'en inspire directement, de canevas. 2 - CANEVAS, LOGIQUES ET SEMANTIQUES Un canevas ïï est une syntaxe géométrique abstraite, qui consiste en un compographe (son support) et un certain nombre de spécifications (comparer avec esquisse = support + cônes, voir [6]). Ces spécifications définissent une propriété "universelle" (en un sens très général) exprimée elle-même dans le langage des canevas. On note Cpgraph la catégorie des petits compographes. 34 DEFINITION DES CANEVAS ET HOMOMORPHISMES DE CANEVAS a) ïï = ( ïï , (J ) est un canevas d'ordre 0 ssi • ïï est un compographe b) H = ( ÏÏ', H, ïï ) est un homomorphisme de canevas d'ordre 0 ssi • ïï', ïï sont des canevas d'ordre 0 • H : ÏÏ' -> ïï est un foncteur c) ïï = ( ïï, 3£(ïï) ) est un canevas d'ordre ^ n+1 ssi • ÏÏ est un compographe (appelé support de ïï) • 3C(ÏÏ) est une classe de quintuplets q = ( F':G_->ÏÏ, H:D->J, F:J->ÏÏ, (dits spécifications) J:J->ÏÏ, J':J'->0< ) où H,J,J' sont des homomorphismes de canevas d'ordre S n F,F' sont des foncteurs F*H = F' et J-H = J'*H d) H = ( ïï', H, ïï ) est un homomorphisme de canevas d'ordre S n+1 ssi • ïï', ïï sont des canevas d'ordre îi n+1 • H : ïï' -> ïï est un foncteur tel que (F' ,H,F,J,J') ^;>;(ÏÏ') => (H*F' ,H' ,H*F,J,J' ) =Â(ÏÏ) . Les canevas petits (i.e. petit") (resp. les homomorphismes sont clairement les ceux objets pour lesquels entre (resp. canevas est petits) flèches) d'une catégorie localement petite que nous noterons Can. On peut identifier Cpgraph à la sous-catégorie pleine de dont les objets sont les canevas d'ordre 0. 35 les "tout Can DEFINITION DES MODELES M = (ïï, M, C) est un modèle (de ÏÏ dans Z) ssi 1) ÏÏ est un canevas 2) C est une catégorie 3) M : ïï -> C est un foncteur 4) quel que soit (F ' ,H, F, J, J ' ) s&*(ïï), - M*F' = (Q, M*F f , C) est un modèle - M«F = (J, M*F,.C) est un modèle d&î - det pour tout modèle N = (J, N, C) tel que N-H = (J, N*H, C) = M-F' , il existe un unique modèle R = (^, R, C) vérifiant R*J = M*F et R«J' = N . La classe des modèles de ïï dans Z sera notée Mod(~,C). A noter que nous ne cherchons pas à définir une notion d'homomorphisme entre modèles. Si H : C -> 3 et -T M*H = C , M+ H, Z) est un homomorphisme de canevas une catégorie, on dispose de l'application Mod(H,C) : Mod(JVC) -> ModC,C) qui au modèle M = (J, M, Z ) associe dont on vérifie que c'est bien un modèle. DEFINITION DES SYNTAXES DE TYPE Une syntaxe de type canevas est un triplet d'homomorphismes o = ( H::]->J, J:J"->J., J':J->C^ ) de avec J*H = J'*H. Si ïï est un canevas et c une syntaxe de type, on pose X (ïï) = { (F' ,H,F,J,J') •£ Se(ÏÏ) / (H,J,J') = J \ J:S->ï'e subordonnés à Z J':J"->5, ) ^ Z , J, I sont ( i l suffit de le demander pour J' ) . Plus particulièrement, si et est un dit que Z est g-héréditaire ssi J':J->(K ) <= Z , I, cardinal V a = ( régulier, H:G->J, on J:J->S-, D, vS, K sont des objets ^-présentables de Can(Z). 37 DEFINITION DES SEMANTIQUES CATEGORIQUES D'UNE LOGIQUE ET DES HOMOMORPHISMES DE SEMANTIQUES ( C, (a ) __. ) est une sémantique catégorique pour la logigue Z ssi 1) Z est une catégorie 2) pour tout o = ( H:0->J, J:J->C, J':J->^ ) ~ a Z , est une application de Mod(D, 3! R € Mod(!K,C) / R*J = a (M') et R*J' = N . Soient ( C, sémantiques homomorphisme (a ) ) catégoriques de la et (a' ) ( €', d'une première même vers la V _• = ( H:2->^ J: J->: r J' :J->Z. ) s Z , ) deux logique Z. Un seconde est un foncteur G: Z -> 1 ' tel que V M <= Mod(J ,Z) , G*M = (I, G*M, C') est un modèle, G-a (M) = (Z, G * a j M K C ) est un modèle, et a' (G-M) = G-a (M) . Les sémantiques catégoriques petites (resp. les homomorphismes entre ces sémantiques) d'une logique Z sont clairement les objets (resp. les flèches) localement petite que nous noterons Sém(O) s'identifie à Cat. d'une Sém(Z). Par catégorie exemple, DEFINITION DE DIVERS FONCTEURS D'OUBLI On dispose d'un certain nombre de foncteurs d'oubli intéressants : 1) U^ : Sém(Z) -> Cat qui envoie la sémantique ( Z, Si Z'c Z, on a plus (a ) __ ) sur la catégorie C généralement U_ _ f : Sém(Z) -> Sém(Z') . un foncteur Pour Z' = 0 , on d'oubli retrouve le foncteur U_ . On a également B„: Sém(Z) -> un foncteur Graph, en d'oubli composant U_ canonique avec l'oubli B : Cat -> Graph. 2) V_ : Sém(Z) -> Can(Z) qui envoie la sémantique ( C, (a ) __ ) sur le canevas ( L, { (M',H,a (M'),J,J') / _ = ( H:Z->Z, J:>>:., J':Z->j) -= I et M' tE ModC ,'C) 1 ) Tout l'intérêt du foncteur V_ réside dans le fait que pour tout canevas ïï subordonné à Z , les dans V_ ( ( Z, dans Z; homomorphismes (a ) __ ) ) s'identifient aux autrement dit, V._ coreprésente modèles les Mod(-,C) : Can(Z)° P -> Ens. Pour Z = 0, V„ n'est d'oubli canonique V autre que le : Cat -> Cpgraph. 3^ foncteur de Z de foncteurs Z 3 - QUELQUES EXEMPLES On se reportera aux planches des syntaxes pages 11 et 12. exemple Z = {a , -• , } : Z est I un prod exp I appelée logique intuitionniste du premier ordre. Ses sémantiques sont exactement les catégories cartésiennes fermées. 0. Soit A tout type A du système F, on peut, par un procédé de décodage systématique (partiellement décrit dans [3]), associer une certaine "syntaxe de type pointée" a = ( H:C->J , J:J->K , J':JJ->2" , ^:1->J ) A avec les intentions suivantes: • JJ décrit la structure interne du type A; • H (resp. v;) pointe dans S les emplacements des variables libres (resp. du domaine principal) de A; • J et J' traduisent la propriété universelle attendue. On dit que A est sémantisable dans une catégorie Z ssi Z est (sous-jacente à ) une sémantique de Z L" [c/ } . I A exemple 1. Au type clos ent = VX.X=>((X=>X)=>X) , on associe •_* représentée page 11. Ce type est ent sémantisable dans Z ssi C est une catégorie cartésienne fermée avec objet des entiers naturels. exemple list(Y) 2. Au type à une variable libre = VX.X=>((X=>(Y=>X))=>X) , on associe list représentée page 11. Ce type s'interprète alors comme "type des listes d'entités de type Y". En "branchant" convenablement a sur c, . , on dessine facilement la ent list syntaxe géométrique du type clos list(ent). exemple 3. Au type clos ( type du '-calcul pur) lambda = VX.(X=>(X=>X))=>(((X=>X)=>X)=>X) , on associe c. ,, représentée page 12. Ce type n'est pas un type lambda naturel au sens de [3], le problème universel dont il est solution est donc plus compliqué que dans les deux exemples précédents (problèmes de co/contravariance). b M v, îfr MN ^ | |b b ÎK ^ ^ il w ii o CL. S Va 41 f> V>- o «4 cr- e-r "pi «-s -> ^a n w 42 O1" 0 V i^ 4 - THEOREME D'ALGEBRICITE On démontre (voir [5]): théorème. Soient •-- un cardinal régulier et q-héréditaire. Alors la g-présentable, et catégorie Sém(Z) une logique est localement foncteur d'oubli canonique admet un adjoint à le V^ : Sém(Z) -> Can(Z) Z gauche et est 2- monadique de rang a. remarque 1. On en déduit en particulier que la structure de catégorie à choix de .^-limites projectives et P'-limites inductives est algébrique (monadique) par rapport de (v?,^' ) -esquisse (ce seul cas particulier à celle semblant déjà nouveau). remarque 2. Le foncteur U_ admet aussi un adjoint à gauche; mais contrairement à V_ pas nécessairement monadique. A ce sujet, il faut noter que si 1'algébricité sur les catégories graphes) (ou , même il n'est sur les est situation remarquable sur le plan mathématique, elle pas très utile pour les applications effet, si les tests de commutativité sont une n'est informatiques: un obstacle en au calcul, il n'en va pas de même de la spécification de types déjà construits (cf les combinateurs catégoriques de Lambek et leur utilisation dans la Categorical Abstract Machine de Cousineau, Curien et Mauny). BIBLIOGRAPHIE [1] J.-Y. Girard, Proofs and types, Cambridge University Press, 1989 (version originale française dactylographiée sous le titre Lambda-calcul typé) [2] P.J. Freyd, Structural polymorphism, draft (23 jan.89) [3] P. Ageron, Sémantique catégorique des types : comprendre le système F, Diagrammes 19, 1988 [4] C. Lair, Trames et sémantiques systèmes de trames, Diagrammes 18, 1987 catégoriques [5] P. Ageron, Logiques, catégories et esquisses, thèse doctorat, à soutenir des de [6] L. Coppey et C. Lair, Leçons de théorie des esquisses (I) Diagrammes 12, 1984 et (II) Diagrammes 19, 1988