No d’ordre

THESE de DOCTORAT de L’UNIVERSITE PARIS VI

Spécialité Systèmes Informatiques Présentée

par Yan-Mei TANG pour obtenir le titre de DOCTORAT de L’UNIVERSITE PARIS VI Sujet de la thèse :

Systèmes d’Effet et Interprétation Abstraite pour l’Analyse de Flot de Contrôle

Soutenue le 28 Mars 1994 devant le jury composé de :

MM. Claude  Girault Président
Charles  Consel  Rapporteur
Michel  Mauny  Rapporteur
Flemming Nielson Rapporteur
Paul  Feautrier Examinateur
Pierre  Jouvelot Examinateur

ECOLE NATIONALE SUPERIEURE DES MINES DE PARIS

Rapport A/258/CRI

Résumé

L’analyse du flot de contrôle est une technique d’importance majeure pour la compilation efficace des langages de programmation fonctionnelle. Cette technique consiste, au moment de compiler un programme, à calculer une approximation de son graphe d’appel, c’est à dire quelles fonctions sont utilisées par le programme, dans quel ordre et à quel niveau. Bien entendu, la précision de telles informations subordonne le possible gain en performance d’exécution résultant de leur l’utilisation au moyen d’un compilateur optimisant. Dans cette thèse, nous considérons deux approches théoriques pour formaliser l’analyse de flot de contrôle: l’inférence d’effet et l’interprétation abstraite. Nous étendons ces deux méthodes d’analyse statique pour ensuite montrer comment les combiner efficacement dans le cadre de l’analyse de flot de contrôle.

La première méthode que nous présentons, l’inférence d’effet, peut être définie comme une extension des techniques qui sont utilisées pour la vérification du typage des programmes en ML. Ainsi, de la même manière qu’un type représente l’approximation d’une valeur, un effet représente l’approximation d’une action ou d’une transition d’état. Ici, plutôt que de nous limiter à adapter les techniques de typage à la ML pour faire de l’analyse de flot de contrôle, nous introduisons une notion avancée de sous-typage qui permet d’augmenter notablement la flexibilité et la précision de cette technique.

La seconde méthode que nous considérons est l’interprétation abstraite qui, utilisant des techniques d’approximation de point-fixe, permet notamment d’obtenir des informations plus précises (sur les fonctions récursives, en particulier), là où d’autres techniques utilisent des méthodes de calcul beaucoup plus simples. Nous proposons de combiner ces deux techniques, introduisant la notion d’analyse sémantique séparée. Nous proposons d’associer une analyse de programme basée sur l’interprétation abstraite, profitant ainsi d’une technique performante pour les expressions closes, avec l’utilisation d’un système d’effet, afin de pouvoir spécifier des informations statiques en présence de compilation séparée, et donc d’information partielle sur l’ensemble d’un programme.

Enfin, nous étudions l’application de l’analyse de flot de contrôle pour la détection d’échappements, c’est à dire la détection, en ML, des variables dont l’existence dépasse le cadre lexical de leur définition. Détecter cette information permet au compilateur de choisir une stratégie optimale pour l’allocation des fonctions. Ainsi, lorsqu’une variable n’est jamais référencée en dehors du cadre lexical de sa définition, on peux alors la représenter dans la pile d’exécution. Dans le cas contraire, elle doit être représentée dans le tas, c’est à dire gérée par le sous-système de gestion mémoire.

Abstract

Control-flow analysis is important in optimizing compilers of functional languages. It strives to approximate at compile time dynamic function call graphs of program evaluation. The precision of the approximation drives the efficiency of optimizations applied in compilers. Control-flow analysis can be expressed by both effect systems and abstract interpretation. My thesis work extends and combines these two static analysis approaches and describes their applications to control-flow analysis.

Effect systems extend classical ML type systems with effect information. Just like types describe the possible values of expressions, effects describe their evaluation behaviors. My thesis introduces subtyping to improve both flexibility and accuracy of effect systems. The subtype relation is limited to the inclusion relation on effects. Control-flow analysis by effect systems collapses different call contexts together, thus limiting the accuracy of control-flow information.

Abstract interpretation is built upon denotational semantics by approximating the fixpoint nature of the language semantics. If abstract interpretation performs more precise static analysis due to its more operational nature, effect systems support separate compilation more naturely thanks to module signatures. My thesis introduces the new notion of separate abstract interpretation that extends abstract interpretation in the context of separate compilation based on the type and effect information of module signatures. It makes the control-flow analysis as effective as the abstract interpretation approach on closed expressions, but is also able to tackle expressions with free variables by using their types to approximate their abstract values.

Finally, my thesis studies the application of control-flow analysis to escape analysis. This analysis identifies the free variables that outlive the lexical scope of function definitions, thus helping compilers choose an efficient closure allocation strategy. Nonescaping variables can be safely allocated in the stack, while heap-allocation is only used for escaping ones.

Remerciements

Je remercie Claude Girault, Professeur à l’Université de Paris 6, d’avoir voulu présider mon jury.

Je remercie Charles Consel, Professeur à l’Université de Rennes, Michel Mauny, Chargé de Recherche à l’INRIA et Flemming Nielson, Professeur à l’Université de Aarhus pour m’avoir fait l’honneur d’accepter d’être mes rapporteurs.

Je remercie Paul Feautrier, Professeur à l’Université de Versailles, pour s’être montré un directeur de thèse agréable et arrangeant.

Je remercie Pierre Jouvelot, Chargé de Recherche à l’Ecole des Mines de Paris, qui m’a accueillie au CRI (Centre de Recherche en Informatique) il y a trois ans et encadré mon travail en y contribuant très largement. Grand merci à lui, car encore, sans lui cette thèse ne serait pas.

Je remercie Michel Lenci, ancien directeur de CRI, de qui je garde le souvenir d’un directeur unique par sa gentillesse et sa sympathie.

Je remercie Jacqueline Altimira, Corinne Ancourt, Vincent Dornic, Francois Irigoin, Marie-Thérèse Lesage, Francois Masdupuy, Nadine Oliver et tous mes autres collègues du CRI pour leur aide et amitié.

Je remercie W. Kluge, Professeur à l’Université de Kiel, qui m’a donné une chance unique de pouvoir venir en Europe il y a cinq ans.

Je remercie mes amis, Hai-fu, Zhen-wu Zhang et Lian Gu, qui m’ont beaucoup aidée et soutenue.

Enfin, je dédie cette thèse à mes parents en Chine, Gui-Zhen et De-Xin, mes beauxparents en France, Annie et Maurice, à mon mari Jean-Pierre et à notre fille Julie.

4

Contents

1 Introduction 9

2 Static Analysis Approaches 23

2.1 Effect Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.1.1 Effect Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.1.2 Verification and Inference . . . . . . . . . . . . . . . . . . . . . . 25 2.1.3 Analysis Framework . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.1.4 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

2.2 Abstract Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.2.1 Analysis Framework . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.2.2 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3 Control-Flow Effect System 31 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Language Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3 Dynamic Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.4 Static Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.5 Consistency Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

3.5.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.5.2 Fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

3.6 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

4 Subeffecting Effect Systems 37 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.2 The Subeffecting Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.3 Subeffecting-Based Reconstruction . . . . . . . . . . . . . . . . . . . . . 38

4.3.1 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.3.2 Algorithm R . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 4.3.3 Constraint Satisfaction . . . . . . . . . . . . . . . . . . . . . . . . 40 4.3.4 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.3.5 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

4.4 System Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 5 Subtyping Effect Systems 45

5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 5.2 The Subtyping Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 5.3 Subtyping-Based Reconstruction . . . . . . . . . . . . . . . . . . . . . . 47

5.3.1 Algorithm S . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 5.3.2 Properties of S . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.3.3 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 5.3.4 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

5.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 5.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

6 Separate Abstract Interpretation 53 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 6.2 Dynamic Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

6.2.1 CPS Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 6.2.2 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

6.3 Abstract Interpretation Semantics . . . . . . . . . . . . . . . . . . . . . 56 6.3.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 6.3.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

6.4 Effect System Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 6.4.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 6.4.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

6.5 Approximating Abstract Values . . . . . . . . . . . . . . . . . . . . . . . 59 6.5.1 Approximation Function A . . . . . . . . . . . . . . . . . . . . . 59 6.5.2 Correctness of A . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

6.6 Separate Abstract Interpretation . . . . . . . . . . . . . . . . . . . . . . 62 6.7 Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

6.7.1 Subtyping Effect Systems . . . . . . . . . . . . . . . . . . . . . . 62 6.7.2 Flexibility of Abstract Semantics . . . . . . . . . . . . . . . . . . 63 6.7.3 Local Control-Flow Effects . . . . . . . . . . . . . . . . . . . . . 63

6.8 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 6.9 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

7 Higher-Order Escape Analysis 65 7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 7.2 Identifying Escaping Variables . . . . . . . . . . . . . . . . . . . . . . . . 65

7.2.1 Escaping Variables . . . . . . . . . . . . . . . . . . . . . . . . . . 65 7.2.2 From Types to Escaping variables . . . . . . . . . . . . . . . . . 66 7.2.3 Algorithm I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

7.3 A Stack-based Abstract Machine . . . . . . . . . . . . . . . . . . . . . . 67 7.3.1 Stack Calling Convention . . . . . . . . . . . . . . . . . . . . . . 67 7.3.2 Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 7.3.3 Instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 7.3.4 Translator C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 7.3.5 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

7.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 7.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 CONTENTS 7

Conclusion 73 Bibliography 75 Appendix 1 81 Appendix 2 87 Appendix 3 97 Appendix 4 109 8 CONTENTS

Chapter 1

Introduction

L’analyse de flot de contrôle joue un rôle-clé dans les compilateurs optimisants pour les langages de programmation fonctionnelle.

Motivation

Les langages de programmation fonctionnelle, comme Lisp [Steele90], Scheme [Rees88] et ML [Mitchell88, Appel90, Milner90] sont largement reconnus pour leur caractère expressif et sémantique simple et bien-fondée. Cependant, il est beaucoup plus difficile de compiler efficacement ces langages, à l’instar d’autres langages plus traditionnels, tels que Fortran ou C. De fait, il existe des différences importantes quant au niveau d’optimisation que tel compilateur est capable d’opérer sur un programme, considérant distinctement ces deux classes de langages de programmation. En particulier, un compilateur pour un langage impératif traditionnel emploie typiquement une variété de techniques d’optimisation inter-procédurales du flot de données, telles que la propagation de constantes, l’élimination des variables non-utilisées, l’élimination des variables dites d’induction, etc [Aho86].

Toutes ces optimisations dépendent, bien entendu, de la bonne connaissance du graphe de flot de contrôle au moment de la compilation. Malheureusement, dans les langages de programmation fonctionnelle, comme les fonctions sont des valeurs à part entière, c’est à dire pouvant être passées en paramètre ou en résultat à par d’autres fonctions, le graphe de flot de contrôle ne peut pas être déterminé avec exactitude au moment de la compilation.

L’imprécision avec laquelle le graphe de flot de contrôle peut être déterminé dans les langages de programmation fonctionnelle rend bien entendu plus difficile, au moment de compiler un programme, les optimisations basées sur une connaissance globale du flot de données. Cette optimisation est pourtant d’importance car, pour ces langages, une fonction est représentée par son code ainsi qu’un environnement, c’est à dire une structure de données qui contient les valeurs de ses variables libres, capturées au moment de sa création. C’est pourquoi de nombreux travaux ont déjà porté sur la détermination du graphe de flot de contrôle afin d’optimiser leur allocation ou leur représentation [Leroy90-1, Appel89, Appel92, Tang92, Wand93]. L’analyse du flot de contrôle permet donc d’effectuer de telles optimisations. Elle peut être exprimée à l’aide de l’interprétation abstraite [Shivers91] ou bien à l’aide de l’inférence d’effet [Tang92].

Les systèmes d’effet utilisent un système de règles comme outil de spécification d’analyse statique. Utiliser un système de règles permet d’établir un jugement des programmes au regard d’un certain critère. Ce moyen d’expression est facile à comprendre et permet donc de raisonner sur les propriétés des programmes. L’utilisation d’un système de règles comme outil de spécification permet également d’isoler plus précisément ce qui est du ressort de l’implémentation : l’algorithme. La distinction entre spécification et réalisation est notamment avantageuse, s’agissant d’étendre l’analyse statique à de nouveaux traits du langage. A l’instar de cette méthode, l’interprétation abstraite ne permet pas une si précise distinction entre spécification et réalisation. Cela rend beaucoup plus difficile la formalisation et la réalisation d’un compilateur optimisant.

Un autre avantage d’un système d’effet par rapport à une interprétation abstraite est l’extension vers un langage de modules. Il est beaucoup plus naturel d’étendre un système d’effet à un langage de module donné (sur des principes similaires au typage) qu’une interprétation abstraite.

Cependant, il est clair que l’interprétation abstraite, utilisant des techniques d’approximation de point-fixe, permet d’obtenir des informations beaucoup plus précises (en particulier sur les fonctions récursives) là où d’autres techniques utilisent des méthodes de calcul beaucoup plus simples, et la précision de telles informations subordonne bien entendu le possible gain en performance d’exécution résultant de leur l’utilisation au moyen d’un compilateur optimisant.

Afin d’évaluer la relative performance de différents systèms de l’analyse de flot de contrôl, [Shivers91] propose de classifier la précision d’une analyse sémantique au moyen d’une notion d’ordre, qui indique en fait le nombre d’appels de fonctions successifs pris en compte dans l’analyse d’une expression donnée. Relativement à cet ordre, nous présentons deux types d’analyses, basées sur les systèmes d’effet et l’interprétation abstraite, qui sont respectivement d’ordre 0 et 1. Nous étudions ensuite l’application de ces techniques à l’analyse de flot de contrôle afin d’optimiser l’allocation des fonctions en ML.

Les Systèmes d’Effet

La vérification du typage dans les langages de programmation fonctionnelle est un domaine de recherche très actif et bien développé [Milner78, MacCracken79, Damas82, Cardelli85, Tofte90, O′Toole90]. L’utilisation de types afin de décrire la structure des valeurs manipulées dans un programme permet à l’utilisateur de comprendre, éventuellement de fournir explicitement, la spécification de son application, mais tend également à favoriser une programmation mieux structurée, et en tout cas à permettre la vérification des erreurs de typage ainsi qu’une meilleure représentation des valeurs manipulées dans le programme.

Nous disons qu’un langage de programmation a un typage statique fort lorsque le compilateur vérifie, contraint et détermine le typage des programmes. Cela permet notamment de prévenir, au moment de la compilation, de l’usage éventuellement incohérent des valeurs manipulées par le programme. En ce sens, le typage statique est la technique d’analyse statique la plus populaire. Cependant, l’utilisation du typage statique impose des contraintes assez fortes sur l’écriture des programmes et peut donc tendre à limiter la souplesse et le pouvoir d’expression d’un langage de programmation.

En ce sens, l’introduction de notions telles que le polymorphisme [Milner78, Kanellakis89, Leroy91] ou le sous-typage [Cardelli88, Aiken93, Fuh88, Stansifer88] a permis d’aller dans le sens de plus de souplesse et d’un caractère plus expressif pour les langages de programmation fortement typés, en autorisant notamment le typage de fonctions génériques ou bien encore en proposant des contraintes plus souples pour leur utilisation.

L’inférence d’effet [Lucassen87, Lucassen88], peut être définie comme une extension des techniques qui sont utilisées pour la vérification du typage des programmes en ML [Milner78, Tofte87]. Ainsi, de la même manière qu’un type représente l’approximation d’une valeur, un effet représente l’approximation d’une action ou d’une transition d’état. Les systèmes d’effet permettent d’élargir notablement le spectre d’utilisation de méthodes de calcul existantes pour la vérification ou l’inférence de type. Cependant, les effets sont souvent représentés dans des algèbres plus complexes que celles utilisées pour les types. A ce jour, les systèmes d’effet sont utilisés dans de nombreux domaines d’application tels que l’analyse d’effets de bord [Talpin92-2, Talpin92-2], l’analyse de complexité [Dornic91], ou l’analyse de liaison statique (binding-time analysis) [Consel93].

Le type d’une fonction est usuellement représenté par t′ → t, où t′ est le type de son paramètre formel et t celui de son résultat. Dans un système d’effet, nous notons t′ \underrightarrow{F} t le type d’une fonction, et nous décrivons par F la transition d’état consécutive à l’utilisation d’une fonction de ce type: F est l’effet latent de la fonction. Comme l’effet latent d’une fonction est propagé à l’aide de son type, il est possible de lier statiquement l’abstraction d’une fonction au regard de cette propriété depuis sa définition jusqu’à son utilisation dans le programme.

Cependant, l’introduction de nouvelles sortes, les effets, dans le système de type du langage de programmation peut introduire de nouvelles contraintes quant au caractère typable des programmes du langage. Nombre de systèmes d’effet existants [Talpin92-1, Dornic91, Tang92] utilisent la notion de sub-effecting pour augmenter la flexibilité du système sur ce point précis. Cette notion consiste à admettre un effet plus grand là où cela est nécessaire afin préserver le typage d’une expression, limitant cependant la précision de l’information calculée.

A la place de cette notion, nous proposons une notion généralisée de sous-typage [Tang93]. Cette notion se définit comme une extension de la relation d’inclusion entre les effets à une relation d’ordre entre les types. Ainsi, à l’instar du sub-effecting, une fonction peut admettre autant de super-types (au sens de cette relation d’ordre) que nécessaire pour préserver le typage d’une expression. L’apport de cette notion de soustypage est certain quant à la précision avec laquelle il devient alors possible d’inférer l’effet d’une expression. En particulier, l’analyse de flot de contrôle peut être réalisée au moyen de cette outils, en présence de fonctions d’ordre supérieures, de constructions impératives et de compilation séparée. Cependant, relativement à la classification de [Shivers91], sa précision est d’ordre 0.

L’Interprétation Abstraite

L’interprétation abstraite [Cousot77, Cousot79, Mycroft81] est un cadre théorique très puissant pour formaliser l’analyse statique de programmes. Cet outil théorique s’appuie sur un modèle de sémantique formel, sémantique dénotationnelle ou bien sémantique opérationnelle, afin de décrire strictement comment s’effectue l’exécution d’un programme.

De cette sémantique, dite standard, du langage est ensuite dérivée une sémantique dite exacte, qui met en évidence les propriétés que l’on cherche à calculer. Cette sémantique exacte peut, par exemple à l’aide de la sémantique dénotationnelle, être décrite à l’aide d’équations de point-fixe sur des structures ordonnées. Ensuite, l’interprétation abstraite consiste à déterminer un point-fixe de ces équations sémantiques, telles qu’elles apparaissent dans un programme donné. Ces équations décrivent récursivement certaines propriétés du programme et sont définies, non pas sur une algèbre rudimentaire comme pour les systèmes d’effet, mais sur des structures de treillis pouvant être assez complexes. C’est au moyen de fonctions d’abstraction et de concrétisation que s’établie ensuite un lien cohérent entre la sémantique exacte et la sémantique abstraite, celle qui exprime les propriétés du programme effectivement calculables.

Le procédé est, on le voit, assez complexe. D’autre part, comme l’interprétation abstraite consiste essentiellement à déterminer un point-fixe des équations exprimées dans un programme, là où l’inférence d’effet utilise l’unification, l’interprétation abstraite autorise le calcul de propriétés beaucoup plus précises que les systèmes d’effet. Ceci étant, les systèmes d’effet donnent au contraire une information beaucoup plus facile à comprendre et à utiliser. En particulier, il est facile de spécifier le type et l’effet d’une fonction dans l’interface d’un module, et de supporter ainsi la compilation séparée de manière plus naturelle.

L’interprétation abstraite a été étudiée dans les langages traditionnels (impératifs) [Cousot77, Cousot79] mais aussi les langages de haut-niveau (fonctionnels) [Mycroft81, Deutsch90, Shivers91], tels que l’analyse du critère strict (Strictness analysis) [Mycroft81], l’analyse d’échappement (Escape analysis) [Goldberg90], ou l’analyse du flot de contrôle [Shivers91]. L’analyse de flot de contrôle basée sur l’interprétation abstraite peut en particulier distinguer les différents points d’appel d’une fonction d’une manière plus précise, permettant ainsi de réaliser une analyse d’ordre n, mais au détriment d’une compilation séparée aisée.

Si une interprétation abstraite permet effectivement de calculer des informations très précises sur les programmes, l’utilisation d’un système de type et d’effet permet au programmeur de spécifier une approximation raisonnable des propriétés statiques de chacun des modules de son programme, interfacés au reste de l’application au moyen d’une signature [Sheldon90]. Ainsi, les systèmes d’effet sont des outils d’analyse plus souples et plus adaptés à la compilation séparée.

Afin de profiter de chacun de ces avantages, nous présentons dans cette thése une notion combinée d’interprétation abstraite séparée [Tang94], qui permet d’utiliser plus naturellement les techniques d’interprétation abstraite dans le contexte de la compilation séparée. Nous considérons le cadre de la compilation séparée comme la compilation des composants, ou modules, d’un programme en isolation les uns des autres. Nous formulons ainsi une analyse de flot de contrôle à l’aide de cette technique, qui permet d’obtenir des informations tout aussi précises que l’interprétation abstraite standard dans le cas d’un petit programme , mais qui est également capable de traiter efficacement les différents modules d’un programme plus important, en utilisant les information de type et d’effets de contrôle spécifiées dans l’interface des autres modules. Dans le cadre d’une analyse globale de flot de contrôle, l’utilisation d’un système de type et d’effet permet au programmeur de spécifier une approximation raisonnable des propriétés statiques de chacun des modules de son programme, interfacé au reste de l’application au moyen d’une signature. Cette signature utilise un système de type et d’effet afin de donner une approximation des informations de flot de contrôle pour le reste du programme.

L’Analyse d’Échappement

Enfin, nous présentons une application immédiate de l’analyse de flot de contrôle, qui consiste en l’optimisation de la représentation et de l’allocation des fonctions [Tang92]: l’analyse d’échappement. Cette technique consiste à identifier les variables d’une fonction pouvant être capturées par d’autres fonctions, et ainsi avoir une durée de vie, ou un cadre d’utilisation, plus grand que le cadre lexical de leur définition.

Cette information est d’importance pour la compilation et permet notamment de décider la classe de représentation des variables. Ainsi, lorsqu’une variable n’est jamais référencée en dehors du cadre lexical de sa définition, on peux alors la représenter dans la pile d’exécution. Dans le cas contraire, elle doit être représentée dans le tas, c’est à dire gérée par le sous-système de gestion mémoire.

Contributions

Dans cette thèse, nous présentons de nouvelles techniques permettant l’analyse de flot de contrôle dans les langages haut-niveau, sur principe de système d’effet et interprétation abstraite. Nous réalisons l’analyse de flot de contrôle basé sur les systèmes d’effet pour le compilateur Mini-FX.

Nous apportons une contribution notable au domaine des systèmes d’effet en introduisant une notion de sous-typage. Cette notion se définit comme une extension de la relation d’inclusion entre les effets à une relation d’ordre entre les types. Ainsi, à l’instar du sub-effecting, une fonction peut admettre autant de super-types (au sens de cette relation d’ordre) que nécessaire pour préserver le typage d’une expression. L’apport de cette notion de sous-typage est certain quant à la précision avec laquelle il devient alors possible d’inférer l’effet d’une expression. Nous montrons que l’introduction d’une règle de sous-typage dans un système d’effet permet de spécifier un problème de résolution décidable. Nous présentons un algorithme correct par rapport à cette spécification. Le cadre de ce travail se limite à un langage doté d’un système de type monomorphe. Il s’étend cependant de manière parfaitement naturelle en présence de types polymorphes, comme tout autre système de sous-typage doté des mêmes caractéristiques.

L’interprétation abstraite est une technique d’importante pour les analyses statiques des langages de programmation fonctinnelle. Si une interprétation abstraite permet effectivement de calculer des informations très précises sur les programmes, un système de type et d’effet peux etre untilisè dans le contexte de la compilation séparée. Afin de profiter de chacun de ces avantages, nous présentons la notion d’interprétation abstraite séparée qui permet de combiner les techniques d’analyse basées sur l’interprétation abstraite et l’inférence d’effet en un seul et même outil. L’utilisation d’un système d’effet permet de d’interfacer les différents modules d’un programme au moyen d’une spéfification du type et des effets de leurs variables exportées, permettant ainsi l’interprétation abstraite des différents modules du programme.

Nous étudions l’application de l’analyse de flot de contrôle à la détection des variables dont l’existence dépasse le cadre lexical de leur définition. Détecter cette information permet au compilateur de choisir une stratégie optimisée pour l’allocation des fonctions. Ainsi, lorsqu’une variable n’est jamais référencée en dehors du cadre lexical de sa définition, on peut alors la représenter dans la pile d’exécution. Nous définissons une machine abstraite dotée d’une pile de contrôle pour son exécution, et nous montrons comment les variables peuvent être représentées en pile lorsque les fonctions ne les capturent pas.

Résumé des Chapitres

Chapitre 3 : Un Système d’Analyse de Flot de Contrôle

L’analyse du flot de contrôle est une technique utilisée pour la compilation efficace des langages de programmation fonctionnelle. Elle consiste à calculer une approximation de son graphe d’appel de fonction du programme. Le flot de contrôle d’une expression peut par exemple être statiquement représenté par un ensemble de fonctions susceptibles d’être appelées durant l’exécution de l’expression. Nous présentons dans ce chapitre une première spécification de l’analyse de flot de contrôle utilisant un système d’effet.

Ce chapitre a pour but essentiel de servir d’introduction à un certain nombre de concepts qui seront plus amplement développés et améliorés dans les chapitres suivants. Nous définissons le cadre formel permettant de prouver notre spécification, au moins d’un critère de cohérence vis à vis de la sémantique dynamique du langage. Nous montrons que notre formulation de l’analyse de flot de contrôle à l’aide d’un système d’effet s’adapte très simplement à des traits variés des langages de haut-niveau: fonctions d’ordre supérieur, opérations de style impératif, compilation séparée. Cependant, ce premier système n’offre pas de performances remarquables en terme de précision ou de flexibilité, et nous tenterons dans les chapitres suivant d’améliorer cet outil en ce sens.

Chapitre 4 : Un Système d’Effet Flexible

Afin d’améliorer la flexibilité du système présenté dans le précédent chapitre, nous introduisons dans notre spécification de l’analyse de flot de contrôle une règle autorisant l’utilisation de la relation d’inclusion sur les effets de contrôle. Ainsi, si une expression admet un effet F, elle admet tout effet F′ supérieur à F au sens de cette relation. Cet ajout a pour conséquence d’augmenter la flexibilité du typage proprement dit, bien qu’avec une imprécision notable.

Nous présentons un premier algorithme qui permet de calculer le type et l’effet de contrôle minimal au sens de notre spécification. Nous prouvons formellement les invariants de cet algorithme par rapport à notre spécification. Enfin, nous montrons comment étendre cette spécification de manière à autoriser un typage générique. Pour cela, nous introduisons une notion de polymorphisme. L’analyse de flot de contrôle présentée dans ce chapitre a été réalisée pour le compilateur Mini-FX.

Chapitre 5 : Systèmes d’Effet et Sous-Typage

Maintenant, nous remplaçons la règle d’inclusion sur les effets, présentée dans le chapitre précédent, pour l’étendre aux types. Nous définissons ainsi une relation de sous-typage contra-variante. Cette relation permet à une fonction d’avoir un type différent dans chacun de ses contextes d’appel.

Ainsi, là où la spécification du chapitre précédent n’admettait qu’une borne supérieure de l’effet pour plusieurs fonctions susceptibles d’être propagées aux mêmes points d’un programme, l’information d’effet relative à chaque fonction peut être maintenant déterminée avec plus de localité. Notre nouvelle spécification est en conséquence beaucoup plus précise qu’auparavant.

Nous présentons un nouvel algorithme permettant de déterminer le type minimal des expressions au regard de notre nouvelle spécification. Nous prouvons que cet algorithme est correct par rapport à cette spécification en utilisant des outils de preuve similaires à ceux du chapitre précédent.

Chapitre 6 : Interprétation Abstraite Séparée

Nous considérons le cadre de la compilation séparée comme la compilation des composants, ou modules, d’un programme en isolation les uns des autres. Dans le cadre d’une analyse globale de flot de contrôle, l’utilisation d’un système de type et d’effet permet au programmeur de spécifier une approximation raisonnable des propriétés statiques de chacun des modules de son programme, interfacé au reste de l’application au moyen d’une signature. Cette signature utilise un système de type et d’effet afin de donner une approximation des information de flot de contrôle pour le reste du programme.

L’interprétation abstraite séparée consiste à utiliser un système d’effet afin de spécifier le type et les effets des différents modules d’un programme, au moyen d’une interface. Cette information sert à l’interprétation abstraite de chacun des modules d’un programme (en isolation des autres) afin de donner une approximation des valeurs abstraites de leurs variables libres (définies dans d’autres modules du programme).

L’idée de base de notre contribution est de considérer que l’inférence d’effet de contrôle est cohérente avec une analyse de flot de contrôle basée sur l’interprétation abstraite (à la [Shivers91]). Dans notre système d’effet de contrôle, les types servent a représenter statiquement la structure des valeurs. Dans le cas d’une fonction, nous notons t′ →^{d} t son type. L’effet latent d est ici très utile, puisqu’il donne un ensemble de fonctions pouvant correspondre à la valeur ayant ce type, mais aussi les possibles effets de contrôle correspondants.

A partir de ce type, il est alors très facile de donner une approximation de la valeur abstraite qui correspondrait à la même valeur, si nous avions utilisé l’interprétation abstraite pour la déterminer. Nous montrons que notre système d’effet de contrôle est une approximation de l’interprétation abstraite du contrôle pour le même langage et en préserve les invariants.

Nous proposons d’associer une analyse de programme basée sur l’interprétation abstraite, profitant ainsi d’une technique performante pour les expressions closes, avec l’utilisation d’un système d’effet, afin de pouvoir spécifier des informations statique en présence de compilation séparée, et donc d’information partielle sur l’ensemble d’un programme.

Chapitre 7 : Analyse d’Echappement d’Ordre Supérieur

Nous étudions dans ce chapitre l’application de l’analyse de flot de contrôle pour la détection d’échappements, c’est à dire la détection, dans un programme, des variables dont l’existence dépasse le cadre lexical de leur définition. Détecter cette information permet au compilateur de choisir une stratégie optimisée pour l’allocation des fonctions. Ainsi, lorsqu’une variable n’est jamais référencée en dehors du cadre lexical de sa définition, on peut alors la représenter dans la pile d’exécution. Dans le cas contraire, elle doit être représentée dans le tas, c’est à dire gérée par le sous-système de gestion mémoire.

Nous présentons une nouvelle technique pour l’analyse statique d’échappement, basée sur l’information que procure notre système d’effet de contrôle. Il est notable de considérer que cette analyse peut ici être mis en oeuvre en présence de fonctions d’ordre supérieur, de constructions impératives ainsi que de compilation séparée. Nous définissons une machine abstraite dotée d’une pile de contrôle pour son exécution, et nous montrons comment les variables peuvent être représentées en pile lorsque les fonctions ne les capturent pas.

18 CHAPTER 1. INTRODUCTION

Introduction

Control-flow analysis plays a key role in optimizing compilers of functional languages

Overview

Functional programming languages like Lisp [Steele90], Scheme [Rees88] and ML [Mitchell88, Appel90, Milner90] are widely recognized for their expressive power and straightforward semantics. Nevertheless they are more difficult to implement efficiently than traditional languages such as FORTRAN and C. There exists a big gap between the optimization levels of these two class of languages. Compilers of traditional languages employ a variety of interprocedural data-flow optimizations like induction-variable elimination, useless-variable elimination, constant propagation, etc [Aho86].

All these optimizations depend on the knowledge of control-flow graphs of programs at compile time. In functional languages, however, since functions are firstclass values, i.e. they can be passed as parameters, returned as results of function calls or stored in memory locations, function call graphs are dynamic in nature. The lack of control-flow graphs at compile time makes interprocedural data-flow optimizations quite difficult when compiling functional languages. Moreover since higher-order functions are represented as closures including their codes and the values of their free variables, control-flow graphs help compilers optimize closure implementations [Leroy90-1, Appel89, Appel92, Tang92, Wand93], such as closure representation and closure allocation. Control-flow analysis is introduced to approximate the dynamic function call graphs at compile time. Control-flow analysis can be expressed by using the framework of effect systems [Tang92] and abstract interpretation [Shivers91].

Effect systems rely on a proof system to specify a particular analysis. This new program analysis technique separates the semantic specification from the implementation of the analysis. Thanks to such a separation, static analyses based on effect systems can be easily extended to other language features and used to formally specify optimization techniques. However abstract interpretation does not provide such a clear separation. As a consequence, optimization techniques related to an analyzer based on abstract interpretation are hard to formalize and extend. Another advantage of effect systems over abstract interpretation is that they can be straightforwardly extended in the context of separate compilation via module signatures. However the abstract interpretation approach performs more precise control-flow analysis thanks to fixed point iteration techniques. The precision of control-flow analysis controls the precision of the interprocedural optimizations performed by optimizing compilers. [Shivers91] introduces the notion of order to mesure the precision of control-flow analysis. The order indicates the number of pending calls remembered during the analysis of a given application expression. My thesis presents zeroth and first-order control-flow analysis systems expressed by both effect systems and abstract interpretation and studies the application of control-flow information in optimizing closure allocation.

Effect systems [Lucassen87, Lucassen88] extend classical polymorphic type systems [Milner78, Tofte87] with effect information. Just like types describe the possible values of expressions, effects specify their possible evaluation behaviors. However the introduction of effects imposes new constraint on the typability of languages. The existing effect systems [Talpin92-1, Dornic91, Tang92] use the notion of subeffecting to increase the flexibility of effect systems. It allows expressions to admit larger effects whenever effect matching would cause type clashes, thus limiting the accuracy of effect systems. Instead of subeffecting, my thesis introduces the notion of subtyping [Tang93]. The subtype relation is limited to the subsumption relation on effect information. Subtyping allows the same function to have different supertypes at different call sites, as long as certain they satisfiy certain subtype relations. The introduction of subtyping improves both flexibility and accuracy of effect systems. Control-flow analysis by effect systems can be performed in presence of higher-order functions, imperative constructs and separate compilation. However it collapses different call contexts together, thus limiting the analysis accuracy to the 0th-order control-flow analysis (0CFA).

Abstract interpretation [Cousot77, Cousot79, Mycroft81] is another static analysis framework. It approximates language semantics by using the fixed point iteration technique. Control-flow analysis based on abstract interpretation [Shivers91] can distinguish different call contexts, thus performing nth-order control-flow analysis (nCFA), but fails to support separate compilation. If the abstract interpretation approach performs more precise static analysis due to fixed point iteration techniques, effect systems support separate compilation more naturally via module signatures [MacQueen90, Sheldon90]. My thesis introduces the new notion of separate abstract interpretation [Tang94] that combines effect systems and abstract interpretation in a single framework. It extends abstract interpretation in the context of separate compilation based on the type and effect information of module signatures. The control-flow analysis expressed by the separate abstract interpretation is as precise as the abstract interpretation approach on closed expressions, but is also able to tackle expressions with free variables by using their type and control-flow information to approximate their abstract values.

As a direct application of control-flow analysis, my thesis presents a new escape analysis for optimizing closure allocation [Tang92]. Escape analysis identifies the free variables that outlive their lexical scope in function definitions. This compile-time knowledge of escaping variables helps compilers choose a more efficient allocation strategy for closures, i.e. non-escaping variables can be safely stored in the stack, while heap allocation is only used for escaping ones.

Outline

The thesis presents different control-flow analysis systems expressed by effect systems (Chapter 3, 4, 5) and abstract interpretation (Chapter 6). The related work is discussed in each chapter and the proofs are presented in the appendix at the end of the thesis.

• Chapter 2 gives an informal description of what effect systems and abstract interpretation are. We discuss the basic ideas, describe their frameworks for static analysis and present their applications in several static analyses.

• Chapter 3 presents a simple control-flow effect system. We give our language syntax, define the dynamic semantics, introduce the static semantics for controlflow analysis and state its consistency w.r.t. the dynamic semantics.

• Chapter 4 introduces subeffecting in the static semantics to increase the flexibility of effect systems. We present a reconstruction algorithm R that reconstructs type and control-flow information of expressions based on subeffecting and prove it sound and complete w.r.t. the static semantics.

• Chapter 5 introduces subtyping in the static semantics to increase the accuracy of the subeffecting effect systems. We present a reconstruction algorithm S that reconstructs type and control-flow information of expressions based on subtyping and prove it sound and complete w.r.t. the static semantics.

• Chapter 6 introduces the new technique of separate abstract interpretation to perform control-flow analysis. We describe the abstract interpretation semantics and state its consistency with the type semantics, show the approach of approximating abstract values of free variables by their types and control-flow information and prove that separate abstract interpretation is a conservative extension of abstract interpretation.

• Chapter 7 describes a new escape analysis based on the control-flow effect systems. We present an algorithm I to identify escaping variables of functions, introduce an efficient closure allocation strategy, describe a stack-based abstract machine and compare our analysis with other escape analyses, particularly that based on abstract interpretation [Goldberg90].

• Finally, we conclude and discuss future work.

22 CHAPTER 1. INTRODUCTION

Static Analysis Approaches

Effect systems and abstract interpretation provide general frameworks of static analyses.

Modern compilers perform a variety of program analyses in order to produce good code [Steele78, Cardelli84, Appel87, Kelsey89, Leroy90-2]. The goal of the analyses is to approximate at compile time evaluation behaviors of programs, which help compilers identify optimization opportunities. Standard analysis techniques have been developed [Aho86] for the traditional languages like PASCAL and C, which are built upon static control-flow graphs. However the traditional analysis approaches are not applicable to higher-order programming languages, since control-flow graphs are absent at compile time. Therefore effect systems and abstract interpretation are introduced to perform static analysis for the programming languages in which functions are first-class values.

2.1 Effect Systems

Type systems have been developed in both traditional and functional languages [Milner78, MacCracken79, Damas82, Cardelli85, Tofte90, O′Toole90]. By using types to describe the data structure of values, programmers can describe the intended specifications of expressions, which makes programs more structured, and compilers can detect type errors, which allows greater execution-time efficiency. The static strong typing of programming languages requires that the type of every expression can be determined at compile time. It allows type inconsistencies to be discovered at compile time and guarantees that executed programs are type consistent. Static typing is a popular technique used for program analysis. Nevertheless by imposing constraints on acceptable expressions, static type systems, may lead to the loss of flexibility and expressive power of programming languages. Polymorphism, expressed by both generic types [Milner78, Kanellakis89, Leroy91] and subtyping [Cardelli88, Aiken93, Fuh88, Stansifer88, Benjamin92] is often introduced to allow an expression to have more than one type.

Effect systems extend classical type systems with effect information. Just like types describe the possible values of expressions, effects specify their possible evaluation properties. In effect systems, a classical function type t′ → t ^{1} is extended to t′ \underrightarrow{F} t where the latent effect F records the evaluation property of functions of this type. Since the latent effect statically links a function from its definition site to its call sites, it plays an important role in effect systems. The introduction of effects increases the applicability of type systems. Nevertheless since effects have their own domains and richer algebras than types, they make type systems much more complicated.

2.1.1 Effect Semantics

Types in effect systems are extended with effect information. A type t can either be a basic type like int, bool or unit, a reference type ref (t) that represents updatable memory locations containing values of the type t, or a function type t′ \underrightarrow{F} t representing a function that accepts arguments of the type t′ and return values of the type t. The evaluation property of the function body is approximated by the latent effect F.

t ∈ Type = BasicTypes | ref (t) | t′ \underrightarrow{F} t

Just as types, effects have their own domain and algebra corresponding to the evaluation properties we are interested in. For example, in a memory side-effect analysis, an effect is defined as a set of store operations and belongs to a set algebra. An effect F can be defined as either the emptyset ∅ meaning the absence of side-effects, a basic store operation like init, read or write, or a set of side-effects gathered with the infix union operator ∪ :

F ::= ∅

                              read | write | init
                              F ∪ F′

The side-effects belong to the following set algebra :

F ∪ (F′ ∪ F′′) = (F ∪ F′) ∪ F′′
F ∪ F′  = F′ ∪ F
F ∪ ∅  = F

                       F ∪ F  = F

An effect system is uniformly specified by a set of inference rules [Plotkin81]. An inference rule (called name) is made of a set of predicates P and P_{1} … P_{n}, which means that the conclusion P holds if the premises P_{1} … P_{n} have been proved. We note:

(name) : \frac{P_{1}, … P_{n}}{P}

If the conclusion P always holds, the inference rule is degenerated to an axiom.

(name) : P

In effect semantics, a predicate E ⊢ e : T, F means that in an environment E, the expression e is evaluated to a value of the type T and its possible evaluation behavior is recorded by the effect F. Note that the environment E defines the types of the free variables in the expression e.

1The whole syntax is formally presented in Chapter 5

Using inference rules, the effect semantics inductively specifies the predicate for each expression on its structure. The crucial rules are the (abs) rule for lambda abstractions and (app) rule for applications.

Given a type environment E and a lambda abstraction (λ (x) e), x is of the type t′ the function body e is evaluated to a value of the type t in the extended type environment E[x ↦ t′] and the evaluation property of e is approximated by the effect F. Then the lambda abstraction has the function type t′ \underrightarrow{F} t. The latent effect is thus introduced in the function type.

(abs) : \frac{E[x ↦ t′] ⊢ e : t, F}{E ⊢ (λ (x) e) : t′ \underrightarrow{F} t, ∅}

When such a function is applied in the application case, its latent effect appears in the resulted effect of the application expression to approximate the evaluation property of the function body. Given a type environment E and an application (e e′), if e and

e′ are evaluated to values of the type t′ \underrightarrow{F′′} t and t′, and their evaluation behaviors are approximated by the effects F and F′ respectively, then (e e′) is of the type t and its evaluation behavior is approximated by F ∪ F′ ∪ F′′ where F′′ represents the evaluation behavior of the function body.

(app) : E ⊢ e : t′ \underrightarrow{F′′} t, F E ⊢ e′ : t′, F′ E ⊢ (e e′) : t, F ∪ F′ ∪ F′′

Note that the latent effect statically links functions from their definition sites to their call sites, thus playing a key role in effect systems.

2.1.2 Verification and Inference

There are two families of effect systems based on either verification or inference. Effect verification systems ask programmers to explicitly specify the types and effects of some expressions in a program, and statically verify the type and effect correctness of the program based a type checking technique. The effect system presented in [Gifford87, Lucassen87, Hammel88] defines the FX programming language and uses an effect verification system [Jouvelot88] to check polymorphic types and side-effect declarations in FX programs.

In order to spare programmers from specifying type and effect information, [Jouvelot91, Talpin92-1] introduce a new effect system that automatically determines the types and effects for implicitly typed programs. This effect inference system extends classical type inference systems [Milner78, Tofte87] with effect information and introduces the notion of algebraic reconstruction and considers the type and effect inference issue as a constraint satisfaction problem.

The difference of these two sorts of effect systems is represented by the (abs) rule for the lambda abstraction. In inference systems, the type of the parameter of each lambda abstraction is computed automatically by a reconstruction algorithm, while in verification systems, it has to be explicitly specified by programmers like below :

(abs) : \frac{E[x ↦ t′] ⊢ e : t, F}{E ⊢ (λ (x : t′) e) : t′ \underrightarrow{F} t, ∅}

2.1.3 Analysis Framework

Effect systems provide a general framework for performing static analysis of programs. Suppose we have a program written in some programming language, and we wish to approximate at compile time some property X about the program evaluation process. For instance, X can be the set of side-effects performed during the evaluation of the program, or the time that the programs need to run, etc. We use the following threestep process to obtain the approximation of the property X.

1. We start with a dynamic semantics for the language that precisely defines what the program means. The dynamic semantics defines the result value V and the property X of the program.

2. Then, we develop a static semantics that conservatively approximates the dynamic semantics. The static semantics defines the type T and effect F of the program where the type T describes the data structure of the result value V , and the effect F is an approximation of the property X.

3. The static semantics defines the static analysis we wish to perform. However the semantic specification is too abstract to tell how to compute the static information. The final step is to define a reconstruction algorithm that computes the type T′ and the effect F′ of the program.

To guarantee that the static information obtained by this effect system is a conservative approximation of the program property, we have to prove the following correctness results :

• The static semantics must be consistent with the dynamic semantics, which means that the effect F defined by the static semantics is a conservative approximation of the property X defined by the dynamic semantics.

• The reconstruction algorithm must be sound and complete w.r.t. the static semantics, stating that, for each program, the type T′ and the effect F′ computed by the reconstruction algorithm satisfy the static semantics and cover all types T and effects F derivable by the static semantics.

2.1.4 Applications

Effect systems have been used to perform several static analyses [Jouvelot88, Talpin92-1, Dornic91, Tang92, Consel93]. Effect systems have the following properties : (1) latent effects are introduced in function types to approximate the evaluation property of functions; (2) Memory locations are explicitly expressed by reference types ref (t), which makes them clearly manifest at compile time ; (3) Types and effects can be expressed in module signatures. Thanks to these properties, static analysis based on effect systems can be performed in the presence of higher-order functions, imperative constructs and separate compilation. Here we give some examples of static analyses performed by effect systems.

• Side-effects analysis

[Talpin92-1] introduces a static side-effect analysis system based on a type and effect inference system that approximates the memory operations like read, write and initialize. The notion of region [Gifford87] is used to specify possible memory sharing. [Talpin92-2] uses an observation criterion that discards the side-effects related to local data structures, thus allowing more precise side-effect information. The compile-time knowledge of side-effects is important to parallel code generation. A prototype compiler [Talpin93-1] has been designed that targets the FX programming language to the Connection Machine.

• Complexity analysis

[Dornic91] suggests an effect system to estimate the worst-case evaluation time of expressions. Even if it fails to accurately approximate recursive functions, it is helpful for choosing an efficient load balance strategy when compiling programs for multiprocessors.

• Binding-time analysis

[Consel93] uses an effect system to determine which variables can be bound to their values at compile time. This binding-time information is of importance when performing partial evaluation or constant folding on programs.

• Control-flow analysis

[Tang92] applies effect systems for approximating dynamic function call graphs of functional languages at compile time. By using the type and control-flow information, an escape analysis is performed to statically identify the free variables of functions that outlive their definition scopes, which helps compilers choose an efficient closure allocation strategy. [Tang93] introduces subtyping in effect systems to avoid effect information to be merged together, thus improving both flexibility and accuracy of effect systems. [Tang94] introduces a more precise control-flow analysis by extending abstract interpretation to support separate compilation based on type and control-flow information. These control-flow analyses form the core of this thesis.

2.2 Abstract Interpretation

Abstract Interpretation [Cousot77, Cousot79, Mycroft81] is a theory of semantics approximation which provides a powerful approach for static analysis [Mycroft81, Deutsch90, Goldberg90, Shivers91]. It is built upon the denotational semantics by approximating the fixpoint nature of the language semantics. Denotational semantics was developed to define the formal semantic descriptions of programming languages. It uses semantic evaluation functions which map syntactic constructs in programs to the abstract values which they denote. Since these evaluation functions are usually recursively defined, they may or may not suggest a way of implementing the language.

The classical framework starts from a standard denotational semantics describing the evaluation process of a programming language. Then an exact semantics is designed to precisely describe the program properties. The exact semantics is often described using fixpoints on ordered structures. Since the exact semantics is not always computable, an abstract semantics is designed to approximate it. The connection between the static and the abstract semantics is specified by abstraction functions, which map exact values to their abstract counterparts. The definition of the abstract function is based on the fixpoint approximation. The static fixpoint approximation approach simplifies equations of the exact semantics to abstract ones that approximate the exact semantics.

Since the abstract interpretation approach is built on the fixpoint approximation of the exact semantic, which requires the whole structure of programs, while effect systems use an unification-based reconstruction algorithm that only relies on the local structure of program syntax, abstract interpretation allows more precise static analysis than effect systems. Nevertheless type and effect information can be easily specified by module signatures, so that effect systems support separate compilation more naturally.

2.2.1 Analysis Framework

Abstract interpretation provides a general framework for static analysis. Suppose we have a program written in some programming language and we wish to approximate at compile time some property X about the program evaluation process. We use the following three-step procedure to obtain the approximation of the property X.

1. We start with a standard denotational semantics for the language that precisely defines what the program P means. The standard denotational semantics specifies the result value V of the program.

2. Then, we develop an exact semantics that precisely expresses the property X of the program. We derive this exact semantics from the original standard semantics. So, if the standard denotational semantics specifies the evaluation result V of the program, then the exact semantics describes its evaluation property X, which constitutes a precise, formal definition of the property we want to analyze.

3. Since the precision of the exact semantics typically implies that it may be uncomputable at compile time, an abstract semantics is defined to approximate the exact semantics. The abstract semantics defines the approximation X̂ of the evaluation property of the program by trading accuracy for compile-time computability.

The correctness of this abstract interpretation approach requires the following correctness results :

• The equations defining the exact and abstract semantics have solutions.

• The abstract semantics safely approximates the exact semantics.

• The abstract semantics is computable.

2.2.2 Applications

Abstract interpretation has been used for both imperative [Cousot77, Cousot79] and higher-order languages [Mycroft81, Deutsch90, Shivers91]. It provides a basic framework for performing static analysis of programming languages in presence of higherorder functions and side-effects.

• Strictness analysis

[Mycroft81] extends the idea of abstract semantics to a functional language and uses a complex semantic structure called a powerdomain. He applies the abstract interpretation framework to perform a static strictness analysis for normal-order languages that identifies opportunities to evaluate function arguments with the call-by value rule instead of the call-by need rule without changing the result of the program.

• Escape analysis

[Goldberg90] presents an application of abstract interpretation for escape analysis, which helps optimize the allocation of closures. An interesting point of this analysis is that, for any function, its type can be used to approximate its arguments that cause the greatest escapement possible.

• Control-flow analysis

[Shivers91] uses abstract interpretation to approximate control-flow graphs of a higher-order language allowing side-effects. Programs are transformed to CPS form (Continuation-Passing Style) so that transfers of control are uniformly represented as tail-recursive function calls. This abstract interpretation approach can perform nth-order control-flow analysis, but fails to support separate compilation.

30 CHAPTER 2. STATIC ANALYSIS APPROACHES

Control-Flow Effect System

Control-flow analysis can be expressed by effect systems.

3.1 Introduction

Control-flow analysis strives to approximate dynamic control-flow behaviors of functional languages at compile time. Control-flow information can be defined as the set of function names possibly called during the evaluation of expressions. This chapter presents a new control-flow analysis based on effect systems. Effect systems extend classical type systems with effect information. By using effects to specify program evaluation behaviors, effect systems provide a powerful method to perform static analysis in the presence of higher-order functions, imperative constructs and separate compilation.

In the sequel, we present our language syntax (Section 3.2), describe the dynamic semantics (Section 3.3), define a simple static semantics of control-flow analysis (Section 3.4) and state its consistency with respect to the dynamic semantics (Section 3.5). Finally we describe related work (Section 3.6) before concluding (Section 3.7). All proofs are presented in Appendix 1.

3.2 Language Definition

My thesis focuses on a simple functional language for the simplicity of presentation. Nevertheless it could be extended to more complicated languages including imperative constructs, let-bindings, module constructs, etc. Possible extensions are discussed in each chapter.

e ::= x  value identifier
(λn (x) e)  abstraction
(recn (f x) e) recursive function
(e e′)l  application

Note that function definitions and function calls are tagged with unique labels (n and l) that allow to uniquely distinguish them.

n ∈ LFun = Label Label of functions
l ∈ LCall = Label Label of function calls

How this labeling is actually performed is not important, as long as the uniqueness property is preserved. However these labels will appear in types and, eventually, module type signatures, so they must be easily understandable by the user. For instance, the label of a function could consist of an identifier (indicating the name of the module where it is defined) and a number (distinguishing it from other functions in the same module)

3.3 Dynamic Semantics

The dynamic semantics not only defines the values of expressions, but also keeps track of control-flow traces occurring during their evaluation.

A computable value v is either an integer i, or a closure. The closure cl is composed of the function name, the argument name, the body expression and the lexical environment in which the function is defined. The environment E is a finite map from identifiers to values. The control-flow behavior b of an expression is a set of function names that are called during its evaluation. The empty set indicates the absence of control-flow traces.

v ∈ Value = Int + Closure  value
cl ∈ Closure = LFun ∗ Id ∗ Exp ∗ Env closure
E ∈ Env = Id ↦ Value environment
f ∈ Trace = P(LFun)  control-flow trace

The dynamic semantics is specified by a set of inference rules [Plotkin81]. Given an environment E , it associates an expression e with the value v it computes and the set of function names b called during its evaluation. We note :

E ⊢ e → v, b

(var) : \frac{x ∈ Dom(E)}{E ⊢ x → E(x), ∅}

(abs) : E ⊢ (λn (x) e) → (n, x, e, Ex), ∅

(rec) : \frac{cl = (n, x, e, E[f ↦ cl])}{E ⊢ (recn (f x) e) → cl, ∅}

(app) : E ⊢ e → (n, x, e′′, E′), b E ⊢ e′ → v′, b′ E′[x ↦ v′] ⊢ e′′ → v, b′′ E ⊢ (e e′) → v, b ∪ b′ ∪ b′′ ∪ {n} where for any function f, f[x ↦ v] is the extension of f with the property that f[x ↦ v](x) = v and f[x ↦ v](y) = f(y), Dom(f) is the domain of f and fx is f in which x is unbound.

We use a simple example demo to show how control transfers during the evaluation of the program.

demo=((λ_{n_{f}} (f)
(+ (f (λ_{n_{a}} (a) a))_{l_{a}}
(f (λ_{n_{b}} (b) b))_{l_{b}}))
(λ_{n_{g}} (g) (g 1)_{l_{g}}))_{l_{f}}

where the lambda expression n_{g} is bound to the variable f at the call site l_{f} and is applied to the arguments (λ_{n_{a}} (a) a) and (λ_{n_{b}} (b) b) at the call sites l_{a} and l_{b}.

At the call site l_{a}, the function n_{g} (via f) is called by binding the identity function n_{a} to the variable g; then control transfers to the function body of n_{g}, where n_{a} (via g) is applied to the argument 1 at l_{g}; then control transfers to the function body of n_{a}, where there is no function calls, i.e. its call set is ∅. Therefore, the control-flow traces of (f (λ_{n_{a}} (a) a)) is recorded by the call set {n_{g}, n_{a}} meaning that during the evaluation of this function application, the functions n_{g} and n_{a} are called. Similarly with the application (f (λ_{n_{b}} (b) b)), its call set is {n_{g}, n_{b}}.

In functional languages, since functions are first-class values, control-flow traces defined by the dynamic semantics can not be determined at compile time. Therefore we define a static semantics to approximate the dynamic one.

3.4 Static Semantics

For each expression the static semantics specifies its type and a set of functions possibly called during its evaluation.

The control-flow effect c abstracts the trace b in the dynamic semantics and thus records all functions possibly called during the evaluation of an expression. A controlflow effect c can either be a constant ∅ meaning the absence of function calls, a singleton {n} where n is a function name, or a set of function names indicated by the infix union operator ∪. A type t can either be the basic type int, or a function type t′ →^{c} t where the latent control-flow effect c records the set of functions possibly called when a function of this type is called. A type environment E is a finite map from identifiers to types.

c ∈ Control c :: = ∅ | {n} | c ∪ c′ control-flow effect
t ∈ Type t :: = int | t′ →^{c} t  type
E ∈ TEnv  = Id ↦ Type  type environment

The static semantics is specified by a set of inference rules. Given a type environment E, it associates an expression e with its type t and control-flow effect c. We note :

E ⊢ e : t, c

The latent control-flow effect is introduced in function types by the (abs) rule for lambda abstraction and used to approximate control-flow traces of function bodies in the (app) rule for function application. In the abstraction case, the current function name is added to the control-flow effect of the lambda body; the resulting set is the latent control-flow effect of the lambda expression. When such a function is applied, in the function application, this latent control-flow information is used to determine the functions possibly called while evaluating the function body.

(var) : \frac{x ∈ Dom(E)}{E ⊢ x → E(x), ∅}

(abs) : \frac{E[x ↦ t′] ⊢ e : t, c}{E ⊢ (λn (x) e) : t′ →^{\{n\}∪c} t, ∅}

(rec) : \frac{E[f ↦ t] ⊢ (λn (x) e) : t, ∅}{E ⊢ (recn (f x) e) : t, ∅}

(app) : \begin{matrix}E ⊢ e : t′ →^{c′′} t, c \\ E ⊢ e′ : t′, c′ \\ E ⊢ (e e′) : t, c ∪ c′ ∪ c′′ \end{matrix}

3.5 Consistency Theorem

We use the proof method introduced in [Tofte87] to show that the static and dynamic semantics are consistent with respect to a structural relation between values and types, defined as the maximal fixed point of a monotonic function.

3.5.1 Definition

We introduce “:” to define the consistency relation between values and types, noted as v : t. This can be easily extended to their environments.

Definition 3.1 (Types of Values and Environments)

i : int
(n, x, e, E) : t ⇔ ∃E, s.t. E : E and E ⊢ (λn (x) e) : t
E : E ⇔ ∀x ∈ Dom(E), x ∈ Dom(E) and E(x) : E(x)

The above structural property does not uniquely define a relation between values and types and must be regarded as a fixed point equation on the domain R = Value ∗ Type. We define a function F on P(R) ↦ P(R), which for any Q ⊆ R, satisfies the following definition :

F(Q) = {(v, t) ∈ Q | if v = i then t = int if v = (n, x, e, E) then ∃E, s.t. ∀x ∈ Dom(E)

x ∈ Dom(E) and (E(x), E(x)) ∈ Q and E ⊢ (λn (x) e) : t}

Its fixed points are the relations on R that verify the structural property defined by Definition 3.1. In order to guarantee the existence of the fixed points of F, it is sufficient to show that F is monotonic [Stoy77].

Lemma 3.1 (Monotony of F) If Q and Q′ are two subsets of the domain R.

Q ⊆ Q′ ⇒ F(Q) ⊆ F(Q′)

3.5.2 Fixpoints

Since the function F is monotonic, it has a minimal and a maximal fixpoint in the complete lattice (P(R), ⊆), namely

lfp(F) = ∩{Q ⊆ R | F(Q) ⊆ Q}

and

gfp(F) = ∪{Q ⊆ R | Q ⊆ F(Q)}

To reach the least fixpoint of F, we start from a bottom set Q = ∅ and gradually construct its least fixpoint lfp(F). The set F(∅) consists of those relations that can be proved without reference to any other relations. For example we have (1, int) ∈ F(∅) for the F we have defined. Next, F(F(∅)) contains the relations that can be proved based on the relations already proved by F(∅) and so on. Since F is monotonic, the limit of the chain

∅ ⊆ F(∅) ⊆ F(F(∅)) …

is the least fixpoint of F. For any relation q, q ∈ lfp(F) if and only if q can be proved true by F.

The maximal fixpoint finding begins with a top set and gradually eliminates those relations that have been proved wrong. Starting from Q = R, meaning that at the outset F rejects nothing, F(R) is the set of relations that cannot be rejected based on the relation in R. By using the monotonic F we have

… F(F(R)) ⊆ F(R) ⊆ R

and the limit of this chain is the maximal fixpoint of F. For any relation q, q ∈ gfp(F) if and only if F can never prove q to be wrong.

Maximal fixpoints are of more interest whenever we define consistency relations, since in some cases such as in languages with side-effects, the least fixpoint cannot be constructed (see [Tofte87]) and the minimal fixpoint lfp(F) is strictly contained in the maximal fixpoint gfp(F). Therefore we choose the maximal fixpoint of the function F to define the relation between types and values. Definition 3.2 (Types of Values)

v : t ⇔ (v, t) ∈ gfp(F)

The subset operation ⊆ is used to define the consistency between dynamic and static control-flow information.

Using these definitions, we can express that the static semantics conservatively approximates the dynamic semantics. Theorem 3.1 (Consistency of Static Semantics)

\begin{matrix}E ⊢ e → v, b \\ E ⊢ e : t, c \\ E : E \end{matrix} \} ⇒ \{ \begin{matrix}v : t \\ b ⊆ c \end{matrix}

Proof See Appendix 1

3.6 Related Work

Shivers′s thesis [Shivers91] presented a control-flow analysis based on abstract interpretation. This analysis is more precise than the one presented here. It can distinguish certain call contexts, but fails to support separate compilation, thus limiting its pratical application. By contrast, our control-flow analysis is performed by a type and effect system that supports the separate compilation of modules, but collapses all call contexts together.

Control effects, defined in [Jouvelot89], are somewhat related to the control-flow information we gather here. However, these control effects are targeted to non-functional behaviors, such as those created by branches or continuations. Also, this analysis is targeted to an explicitly typed language, which allows explicit polymorphism.

The flow analysis described in [Bondorf93], which is used in their binding-time analysis system, traces the flow of function values in an untyped language. The only information gathered there for first-class functions is the possible arities of functions reaching a given program point. Since we restrict ourselves to typed languages, this information is a special case of our type analysis. Their flow constraint set is generated by a one-pass compositional run over programs and solved by a rewriting system, which has the same complexity as our type and effect inference system.

Effect systems have been used to approximate program evaluation behaviors in higher-order language, such as side-effects [Talpin92-1], evaluation complexity [Dornic91], etc. Control-flow analysis is another application of effect systems.

3.7 Conclusion

We presented a new control-flow analysis system based on effect systems. This controlflow effect system can be used in presence of higher-order functions, imperative constructs and separate compilation. We defined the dynamic semantics of the language, described a static semantics for control-flow analysis, and stated its consistency w.r.t. to the dynamic semantics.

If this simple static semantics is useful to lay the ground to control-flow analysis by effect systems, it suffers from shortcomings that are going to be presented and dealt with in Chapter 4,5. Thus even though a reconstruction algorithm could easily be designed for this semantics, we will delay this aspect until the next chapters.

Subeffecting Effect Systems

Subeffecting improves flexibility of effect systems but at the price of their accuracy.

4.1 Introduction

We extend the static semantics defined in Chapter 3 with the subeffecting rule. Subeffecting allows expressions to admit larger effects when a type mismatch occurs, thus improving the flexibility of the effect system. However it forces a function to have a unique type in different call contexts by merging their effects together, thus limiting the accuracy of the effect system. We introduce a reconstruction algorithm that for each expression computes its type and control-flow effect based on subeffecting. The reconstruction algorithm is sound and complete w.r.t. the static semantics.

We introduce the subeffecting rule (Section 4.2), present the corresponding reconstruction algorithm and prove it sound and complete w.r.t. the static semantics (Section 4.3). Finally we describe system extensions (Section 4.4) before concluding (Section 4.5). All proofs are presented in Appendix 2.

4.2 The Subeffecting Rule

The effect system defined in Chapter 3 extends classical type systems with effect information. However the interplay of types and effects introduces new constraint on the typability of expressions. Effect checking may force the rejection of programs that would be type checked if no effects were present, thus reducing the flexibility of effect systems. We use the example demo to show this problem. For clarity, we use i to indicates the type int.

In classical type systems, since the lambda expressions (λ_{n_{a}} (a) a) and (λ_{n_{b}} (b) b) have the same type i → i, the variable f admits the same type (i → i) → i in its three instances. Therefore this program can be type checked.

In the previously defined effect system, due to the introduction of the latent controlflow effects {n_{a}} and {n_{b}}, the lambda expressions (λ_{n_{a}} (a) a) and (λ_{n_{b}} (b) b) have the different types i →^{{n_{a}}} i and i →^{{n_{b}}} i. Therefore f cannot keep the same type at the different call contexts l_{a} and l_{b}. Thus the program is rejected by type checking.

Subeffecting has been used to improve the flexibility of effect systems [Talpin92-1, Dornic91, Tang92]. It allows expressions to admit larger effects when a type mismatch occurs. The subeffecting approach forces a function to have identical type in different call contexts by merging their effects together, thus limiting the accuracy of effect systems.

Subeffecting is introduced by the (does) rule that allows an expression to admit a larger effect c instead of c′. This rule can be used whenever a type mismatch occurs in the application rule (app) due to its latent effect.

(does) : \begin{matrix}E ⊢ e : t, c′ \\ c′ ⊆ c \\ E ⊢ e : t, c \end{matrix}

For the same example demo, by using the subeffecting technique, the lambda expressions (λ_{n_{a}} (a) a) and (λ_{n_{b}} (b) b) admit a unique type i →^{{n_{a},n_{b}}} i. Therefore f can

keep the same type (i →^{{n_{a},n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i at the different call sites l_{a} and l_{b}, thus this program can be type checked. Note that subeffecting forces the latent effects of the lambda expressions (λ_{n_{a}} (a) a) and (λ_{n_{b}} (b) b) to be merged together, thus limiting the accuracy of effect systems.

4.3 Subeffecting-Based Reconstruction

We present an algorithm based on subeffecting for reconstructing types and control-flow effects of expressions. To stay as close as possible to classical unification-based algorithms, the basic idea is that latent effects of functions are always represented by effect variables. Thus the type unification can be applied on both type and effect variables. Beside reconstructing types and control-flow effects of expressions, the algorithm also computes a set of subsumption constraints between effect variables and control-flow effects of the form {ζ_{i} ⊇ c_{i} | i = 1..s}. Thus the reconstruction of types and control-flow effects of expressions is viewed as a constraint satisfaction problem. For an expression that admits a type and control-flow effect in the static semantics, its corresponding effect constraint set must have at least one solution. This solution satisfies the criteria of the maximality of the type with respect to substitution on type variables, and minimality of the effect with respect to the subsumption on effect variables.

κ ∈ Constraint = P(EfVar ∗ Control)

4.3.1 Unification

The unification algorithm U [Robinson65] solves the equations on types and effect variables built by the reconstruction algorithm. It returns a substitution θ as the most general unifier of two terms, or fails. Note that the reconstruction algorithm only unifies effect variables. Substitutions θ are defined as maps from type or effect variables to their corresponding values. We note Id is the identity substitution.

θ ∈ Subst = (TyVar ↦ Type) + (EfVar ↦ Control)

U(t, t′) = case (t, t′) of

(int, int) ⇒ Id

(α, α′) ⇒ [α ↦ α′]

(α, t)|(t, α) ⇒ if α ∈ fv(t) then fail else [α ↦ t]

(t_{0} →^{ζ_{0}} t′_{0}, t_{1} →^{ζ_{1}} t′_{1}) ⇒ let θ = [ζ_{0} ↦ ζ_{1} ] and θ′ = U(θt_{0} , θt_{1} )

in U(θ′θt′_{0} , θ′θt′_{1} )θ′θ

( , ) ⇒ fail

where for any substitutions θ and θ′, θt is the application of the substitution θ to t and θθ′ is the composition of the substitutions with the property that θθ′(ϑ) = θ(θ′(ϑ)).

Lemma 4.1 (Correctness of U) Let t and t′ be two type terms in the domain of U. If θ = U(t, t′), then

• U is sound : θt = θt′,

• U is complete : If θ′t = θ′t′, there exists a substitution θ′′ such that θ′ = θ′′θ.

Proof U unifies terms over a free algebra, and is thus complete following [Robinson65].

4.3.2 Algorithm R

Given an expression e and its type environment E , the reconstruction algorithm R computes a substitution θ, its type t, control-flow effect c and a constraint set κ. We note :

R(E, e) = ⟨θ, t, c, κ)

The effect constraint set is built during the reconstruction of lambda expressions where a latent effect is introduced into the function type.

R(E, x) ⇒ if x ∈ Dom(E) then ⟨Id, E(x), ∅, ∅⟩ else fail

R(E, (λn (x) e)) ⇒

let α, ζ new

⟨θ, t, c, κ⟩ = R(E[x ↦ α], e)

in ⟨θ, θα →^{ζ} t, ∅, κ ∪ {ζ ⊇ c ∪ {n}}⟩

R(E, (recn (f x) e)) ⇒

let α′, α, ζ new

E′ = E[f ↦ α′ →^{ζ} α][x ↦ α′]

⟨θ, t, c, κ⟩ = R(E′, e)

θ′ = U(θα, t)

in ⟨θ′θ, θ′θ(α′ →^{ζ} α), ∅, θ′(κ ∪ {θζ ⊇ {n} ∪ c})⟩

R(E, (e e′)) ⇒

let ⟨θ, t, c, κ⟩ = R(E, e)

⟨θ′, t′, c′, κ′⟩ = R(θE, e′)

α, ζ new

θ′′ = U(θ′t, t′ →^{ζ} α)

in ⟨θ′′θ′θ, θ′′α, θ′′(θ′c ∪ c′ ∪ ζ), θ′′(θ′κ ∪ κ′)⟩

Note that by the unification of two effect variables ζ and ζ′, the inequalities {ζ ⊇ c, ζ′ ⊇ c′} in the constraint set are replaced by {ζ ⊇ c, ζ ⊇ c′}, which is equivalent to {ζ ⊇ c ∪ c′}.

4.3.3 Constraint Satisfaction

An expression e with its type environment E is type and effect safe if and only if R(E, e) does not fail and the returned constraint set κ admits at least one solution. The constraint set is of the normal form {ζ_{i} ⊇ c_{i} | i = 1..s}, which guarantees the existence of solutions. We are interested at the minimal one.

The substitutions satisfying κ are called effect models.

Definition 4.1 (Effect Model) A substitution μ is an effect model of a constraint set κ, noted as μ ⊧ κ, if and only if ∀ζ ⊇ c ∈ κ, μζ ⊇ μc.

Theorem 4.1 (Satisfaction) Every normal form constraint set κ = {ζ_{i} ⊇ c_{i} | i = 1..s} admits at least one effect model.

Proof {ζ_{i} ↦ c′_{i} | i = 1 … n} is an effect model of κ, where c′_{i} = ∪_{i=1}^{n}c_{i} \ ∪_{i=1}^{n}ζ_{i}.

A constraint set may admit more than one effect model, among which we are interested in the minimal one. We define a function Min to characterize the minimal effect model of a constraint set κ. Note that the solution is independent of the order of inequalities in κ.

Min(∅) = Id
Min({ζ ⊇ c} ∪ κ′) = let μ = Min(κ′) in {ζ ↦ μc \ ζ}μ

The constraint set of the reconstruction algorithm always admits a unique minimal model with respect to the subsumption relation ⊇ on effects.

Theorem 4.2 (Minimality) Any constraint set admits a unique minimal effect model. Proof By induction on the constraint set.

4.3.4 Correctness

The reconstruction algorithm terminates and is sound and complete with respect to the static semantics.

Theorem 4.3 (Termination) For all inputs (E, e), the algorithm R either fails or terminates.

Proof Since the reconstruction algorithm R is defined on the structure of expressions of finite height, it terminates or fails.

The soundness theorem states that the application of any effect model of the reconstructed constraint set to the reconstructed type and effect satisfies the static semantics.

Theorem 4.4 (Soundness) Given an expression e and its type environment E, if R(E, e) = ⟨θ, t, c, κ⟩, then, for any effect model μ of κ, one has:

μθE ⊢ e : μt, μc

The completeness theorem states that the reconstructed type t and control-flow effect c are maximal with respect to any type t_{1} and control-flow effect c_{1} derivable by the static semantics, for some substitution μ that satisfies the computed constraint set κ.

Theorem 4.5 (Completeness) If θ_{1}E ⊢ e : t_{1}, c_{1}, then R(E, e) = ⟨θ, t, c, κ⟩ and there exists an effect model μ of κ such that:

θ_{1}E = μθE and t_{1} = μt and c_{1} ⊇ μc

4.3.5 Example

We use the same example demo to show the reconstruction process by solving the effect constraint set. Here we give the following table to show the type of the variables f, g and the lambda expressions n_{f}, n_{a}, n_{b}, n_{g}.

\begin{matrix}f : & (i →^{ζ_{1}} i) →^{ζ_{2}} i \\ g : & i →^{ζ_{1}} i \\ n_{f} : & ((i →^{ζ_{1}} i) →^{ζ_{2}} i) →^{ζ_{3}} i \\ n_{a} : & i →^{ζ_{1}} i \\ n_{b} : & i →^{ζ_{1}} i \\ n_{g} : & (i →^{ζ_{1}} i) →^{ζ_{2}} i \end{matrix}

The constraint set is of the form:

{ζ_{1} ⊇ {n_{a}, n_{b}}, ζ_{2} ⊇ {n_{g}} ∪ ζ_{1}, ζ_{3} ⊇ {n_{f}} ∪ ζ_{2}}

The minimal solution of this constraint set is as below :

ζ_{1} ↦ {n_{a}, n_{b}}, ζ_{2} ↦ {n_{g}, n_{a}, n_{b}}, ζ_{3} ↦ {n_{f}, n_{g}, n_{a}, n_{b}}

4.4 System Extensions

The subeffecting effect system can be straightforwardly extended to imperative constructs and let-bound expressions in a way as presented in [Talpin92-1]. A reference type ref (t) needs to be introduced to represent updatable memory locations containing values of the type t.

The parametric polymorphism introduced in ML type systems [Milner78, Tofte87] can be extended to effect systems [Talpin92-1]. The type of e′ in (let (x e′) e) can be generalized on both type and effect variables, if e′ is side-effect free. Therefore its effect variables can be instantiated to different effects in different call contexts, thus increasing the accuracy of effect systems. [Tofte87] introduces an expansiveness function to detect if expressions have side-effects or not. A non-expansive expression is syntactically guaranteed to be side-effect free. By using side-effect analysis [Talpin92-1], especially by introducing an observation criterion [Talpin92-2], type generalization in let-expressions can be performed in a more precise way. One can use syntactic substitution to avoid the complication of introducing sophisticated type schemes. We write e′[e/x] for the textual substitution of e for x in e′. The syntactic substitution e′[e/x] reflects the fact that different types of e can be used for each occurrence of x in e′. In the static semantics, the type generalization of let expression is specified by the following (let) rule :

(let) : ¬expansive[[e]] E ⊢ e : t, ∅ E ⊢ e′[e/x] : t′, c′ E ⊢ (let (x e) e′) : t′, c′

In the reconstruction algorithm, in order to avoid recomputing the type of expressions bound in let constructs, we use algebraic type schemes to generalize their types and associated constraints. Here algebraic type schemes, noted ∀v_{1..n}.(t, κ), are composed of a type t and a set of inequalities κ universally quantified over type and effect variables v_{1..n}. Algebraic type schemes are used to implement the textual substitution specified in the let rule in the statics semantics. The type and constraint set associated with e only depend on the free variables of e and, thereby, on the type environment E. An algebraic type scheme caches the effect constraint that would have to be recomputed each time e appeared in the substituted body. Constrained type environments E map value identifiers to algebraic type schemes.

∀v_{1..n}.(t, κ) ∈ TyScheme  type scheme
E  ∈ TEnv  = Id ↦ TyScheme type environment

The reconstruction algorithm only needs to be modified for the case of identifiers and let-bound expressions.

R(E, x) ⇒ if x ↦ ∀v_{1..n}.(t, κ) ∈ E then let {v′_{1...n}} new

θ = {v_{i} ↦ v′_{i} | i = 1 … n}

in ⟨θ, θt, ∅, θκ⟩

else fail R(E, (let (x e) e′)) ⇒

let ⟨θ, t, c, κ⟩ = R(E, e)

in let v_{1..n} = (fv(t) ∪ fv(κ)) \ fv(E) E′ = θEx ∪ {x ↦ ∀v_{1..n}.(t, κ)} ⟨θ′, t′, c′, κ′⟩ = R(E′, e′) in ⟨θ′θ, t′, c′, κ′⟩

The example program demo can be equivalently written in the let-binding form.

                  let-demo= (let (f (λ_{n_{g}} (g) (g 1)_{l_{g}}))

(+ (f (λ_{n_{a}} (a) a))_{l_{a}}
(f (λ_{n_{b}} (b) b))_{l_{b}}))

The type of the let-binding expression (λ_{n_{g}} (g) (g 1)) can be generalized to ∀ζ_{1}ζ_{2}.((i →^{ζ_{1}}

i) →^{ζ_{2}} i, ∅). When it is called (via f) at the call site l_{a} and l_{b}, it can be instantiated to

(i →^{ζ′_{1}} i) →^{ζ′_{2}} i and (i →^{ζ′′_{1}} i) →^{ζ′′_{2}} i respectively and the constraint set is as below:

{ζ′_{1} ⊇ {n_{a}}, ζ′′_{1} ⊇ {n_{b}}, ζ′_{2} ⊇ {n_{g}} ∪ ζ′_{1}, ζ′′_{2} ⊇ {n_{g}} ∪ ζ′′_{1}, ζ_{3} ⊇ {n_{f}} ∪ ζ′_{2} ∪ ζ′′_{2}}

By solving the constraint set, we get the minimal solution of this constraint set :

ζ′_{1} ↦ {n_{a}}, ζ′′_{1} ↦ {n_{b}}, ζ′_{2} ↦ {n_{g}, n_{a}}, ζ′′_{2} ↦ {n_{g}, n_{b}}, ζ_{3} ⊇ {n_{f}, n_{g}, n_{a}, n_{b}}

Therefore the control-flow information at the call site l_{a} or l_{b} is {n_{g}, n_{a}} or {n_{g}, n_{b}} respectively. With the previously defined subeffecting effect system, the control-flow information of (f (λ_{n_{a}} (a) a)) and (f (λ_{n_{b}} (b) b)) are both {n_{g}, n_{a}, n_{b}}, even if only {n_{g}, n_{a}} or {n_{g}, n_{b}} are called during their evaluations, thus collapsing different call contexts together.

Here we give the following table to compare the control-flow information at the call sites l_{a} and l_{b} collected by effect systems with and without the introduction of the generic types. Note that the introduction of generic types can distinguish different call contexts (n_{a} and n_{b}), thus performing more precise control-flow analysis.

              Dynamic Semantics  Effect Systems  Generic Types

l_{a} {n_{g}, n_{a}}  {n_{g}, n_{a}, n_{b}}  {n_{g}, n_{a}}
l_{b} {n_{g}, n_{b}}  {n_{g}, n_{a}, n_{b}}  {n_{g}, n_{b}}

4.5 Conclusion

We introduced subeffecting to improve the flexibility of effect systems. The subeffecting approach allows expressions to admit larger effects when a type mismatch occurs. We presented the subeffecting rule in the static semantics, discussed the reconstruction algorithms R and proved it sound and complete w.r.t. the static semantics. Finally, we described how to extend generic polymorphism in effect systems. This polymorphic control-flow effect system has been implemented in a Mini-FX compiler [Grundman92] where Mini-FX is a variant of the Scheme programming language [MIT90].

44 CHAPTER 4. SUBEFFECTING EFFECT SYSTEMS

Subtyping Effect Systems

Subtyping improves both flexibility and accuracy of effect systems.

5.1 Introduction

Instead of subeffecting, we introduce subtyping in effect systems. Subtyping allows a function to have different types in different call contexts, as long as they obey certain subtype relation. The subtype relation is induced by a subsumption rule on effects. This subtyping effect system avoids effect information to be merged together when forcing two types to be identical, thus collecting more precise effect information than the previous effect system based on subeffecting. We introduce a reconstruction algorithm that for each expression computes its type and control-flow effect based on subtyping. The reconstruction algorithm is sound and complete w.r.t. the static semantics.

We introduce the subtyping rule (Section 5.2), present the corresponding reconstruction algorithm and prove it sound and complete w.r.t. the static semantics (Section 5.3). Finally we describe related work (Section 5.4) before concluding (Section 5.5). All proofs are presented in Appendix 3.

5.2 The Subtyping Rule

The subtype relation is defined between types of the same structure. The type structure is defined by the classical types. A classical type τ can either be int, a type variable α, or a function type τ′ → τ.

τ ∈ CType = int | α | τ′ → τ classical type

An effect, here specified by a set of function names, can be conservatively approximated by one of its supersets. The subeffect relation is thus the usual set inclusion relation.

If two function types have the same structure, the subtype relation ≤ is defined via the inclusion relation between their latent effects. To properly define this notion, we introduce the Erase function which transforms types to classical types by deleting latent effects.

Erase(int)  = int
Erase(α)  = α
Erase(t′ →^{c} t) = Erase(t′) → Erase(t)

The type structure of t is Erase(t). Two types t and t′ have the same structure if and only if Erase(t) = Erase(t′).

The subtype relation t ≤ t′ is defined whenever t and t′ have the same structure. Note that the subtype relation between function types is contravariant.

Definition 5.1 (Subtype)

int ≤ int
α ≤ α
t′_{0} →^{c_{0}} t_{0} ≤ t′_{1} →^{c_{1}} t_{1} ⇔  t′_{1} ≤ t′_{0} ∧ t_{0} ≤ t_{1} ∧ c_{1} ⊇ c_{0}

The function Eff generates the set of effect inequalities corresponding to a given type inequality. An effect inequality is a pair (c_{i}, c′_{i}) written c_{i} ⊇ c′_{i}.

Eff (int ≤ int)  = ∅
Eff (α ≤ α)  = ∅
Eff (t′_{0} →^{c_{0}} t_{0} ≤ t′_{1} →^{c_{1}} t_{1}) = {c_{1} ⊇ c_{0}} ∪ Eff (t′_{1} ≤ t′_{0}) ∪ Eff (t_{0} ≤ t_{1})

Subtyping is introduced by the following (sub) rule that allows a larger type t to be used in lieu of t′. This increases the flexibility of the static semantics by allowing a function to admit different types, as long as a certain subtype relation is satisfied. It avoids merging effect information together when forcing two types to be identical, thus collecting more precise effect information than the subeffecting technique.

(sub) : \begin{matrix}E ⊢ e : t′ \\ t′ ≤ t \\ E ⊢ e : t \end{matrix}

We use the same example demo to show how subtyping improves the accuracy of effect systems compared to subeffecting. When the function f (bound to n_{g}) is called

at l_{a} and l_{b}, it can admit the supertypes (i →^{{n_{a}}} i) →^{{n_{g},n_{a},n_{b}}} i and (i →^{{n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i

respectively instead of having the unique type (i →^{{n_{a},n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i. The following table shows the difference between subeffecting and subtyping. We give the types of f at these three occurrences (t_{f}, t′_{f} and t′′_{f}), and the types of the arguments n_{a} and n_{b} (t_{n_{a}} and t_{n_{b}})

                   Subeffecting         Subtyping

t_{f} (i →^{{n_{a},n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i (i →^{{n_{a},n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i
t′_{f} (i →^{{n_{a},n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i (i →^{{n_{a}}} i) →^{{n_{g},n_{a},n_{b}}} i
t_{n_{a}} i →^{{n_{a},n_{b}}} i  i →^{{n_{a}}} i
t′′_{f} (i →^{{n_{a},n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i (i →^{{n_{b}}} i) →^{{n_{g},n_{a},n_{b}}} i
t_{n_{a}} i →^{{n_{a},n_{b}}} i  i →^{{n_{b}}} i
t_{f} = t′_{f}  t_{f} ≤ t′_{f}
t_{f} = t′′_{f}  t_{f} ≤ t′′_{f}

Notice that, when using subeffecting, all occurrences of f are forced to have the same type, while, when using subtyping, they only have to obey a subtype relation, leading to more precise local control-flow information.

5.3 Subtyping-Based Reconstruction

The reconstruction of types and effects based on subtyping operates on the expressions that are already typed by classical type systems. For each expression e annotated with classical types, the reconstruction algorithm S computes its type, its effect and a set of type inequalities based on subtyping. Since the subtype relation in our system is defined by the subsumption relation on effects and the structures of the types are known, type inequalities amount to sets of effect inequalities. Therefore solving type inequalities is reduced to solving the corresponding effect inequalities. Thus the subtyping-based reconstruction can be also viewed as an effect constraint satisfaction problem. For every expression that has a type and a control-flow effect in the static semantics, its effect constraint set must have at least one solution, which satisfies the set of type inequalities.

For any expression e, the classical type reconstruction algorithm computes its principal type τ w.r.t. the types t defined by the static semantics (modulo Erase). In other words, for any expression, if τ is its type computed by the classical type reconstruction algorithm and t is derivable from the static semantics, then there exists a type substitution θ, such that :

Erase(t) = θτ

5.3.1 Algorithm S

Given a type environment E and an expression e assumed priorly decorated with its classical type (we use a straightforward expression annotation mechanism to express this information in the algorithm), the reconstruction algorithm S computes a type t, an effect c and an effect constraint set κ. We note :

S(E, e) = ⟨t, c, κ⟩

The effect constraint set is partly built by application of Eff to type inequalities and partly during the reconstruction of lambda and rec expressions:

S(E, x) ⇒

let t′ = E(x)

t = New(Erase(t′)) in ⟨t, ∅, Eff (t′ ≤ t)⟩

S(E, (λn (x : τ) e)) ⇒

let t′ = New(τ)

ζ new

⟨t, c, κ⟩ = S(E[x ↦ t′], e)

in ⟨t′ →^{ζ} t, ∅, κ ∪ {ζ ⊇ {n} ∪ c}⟩

S(E, (recn (f : τ′ → τ x : τ′) e)) ⇒

let t′ →^{ζ} t = New(τ′ → τ)

⟨t′′, c, κ⟩ = S(E[f ↦ t′ →^{ζ} t][x ↦ t′], e)

in ⟨t′ →^{ζ} t, ∅, κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c}⟩

S(E, (e e′)) ⇒

let ⟨t′′ →^{c′′} t, c, κ⟩ = S(E, e)

⟨t′, c′, κ′⟩ = S(E, e′) in ⟨t, c ∪ c′ ∪ c′′, κ ∪ κ′ ∪ Eff (t′ ≤ t′′)⟩

where the function New transforms a classical type τ to a type t by adding fresh latent effect variables to τ. Its proper definition is:

New(int)  = int
New(α)  = α
New(τ′ → τ) = New(τ′) →^{ζ} New(τ) for fresh ζ

Note that subeffecting can be easily related to subtyping by noticing that its related reconstruction algorithm R is similar to S, except that ≤ is replaced by the more restrictive =, implemented by unification.

5.3.2 Properties of S

We can easily prove by induction that the reconstruction algorithm S has the following properties :

Lemma 5.1 (Properties of S) For any E, e, if S(E, e) = ⟨t, c, κ⟩, then :

• t only includes fresh effect variables.

• All environment extensions within S refer to types with only fresh effect variables.

The previous lemma implies that the constraint set computed by the reconstruction algorithm S has the following normal form property:

Lemma 5.2 (Normal Effect Constraints) If S(E, e) = ⟨t, c, κ⟩, then κ has the following normal form:

{ζ_{i} ⊇ c_{i} | i = 1..s}

As stated in Chapter 4, effect constraint sets in this normal form guarantee the existence of unique minimal effect models. The following lemma shows how to satisfy a type inequality by solving its corresponding effect constraint.

Lemma 5.3 (Solution of Type Inequality) If t and t′ have the same structure, then

μ ⊧ Eff (t′ ≤ t) ⇔ μt′ ≤ μt

Proof By induction of the structure of types.

5.3.3 Correctness

Since the reconstruction algorithm S is defined by induction on the structure of expressions, which are of finite height, it always terminates. It is sound and complete with respect to the static semantics.

The soundness theorem states that the application of any effect model of the reconstructed type constraint set to the reconstructed type and effect satisfies the static semantics.

Theorem 5.1 (Soundness) Given an expression e and its type environment E, if S(E, e) = ⟨t, c, κ⟩, then for any effect model μ of κ, one has:

μE ⊢ e : μt, μc

The completeness theorem states that the reconstructed type t and the control-flow effect c are maximal with respect to any type t_{1} and control-flow effect c_{1} derivable from the static semantics, modulo some substitution μ that satisfies the computed constraint set κ.

Theorem 5.2 (Completeness) If θ_{1}E ⊢ e : t_{1}, c_{1}, then S(E, e) = ⟨t, c, κ⟩ and there exists an effect model μ of κ, such that:

θ_{1}E = μE and μt ≤ t_{1} and c_{1} ⊇ μc

5.3.4 Example

We use the same example demo to show how the reconstruction algorithm S works for expressions already typed with classical types. After applying the classical type reconstruction algorithm, the program demo is annotated by classical types like below :

demo-annotated=((λ_{n_{f}} (f : (i → i) → i)

(+ (f (λ_{n_{a}} (a : i → i) a))_{l_{a}}

(f (λ_{n_{b}} (b : i → i) b))_{l_{b}}) )
(λ_{n_{g}} (g : i → i) (g 1)_{l_{g}})_{l_{f}})

We apply the algorithm S to demo-annotated. Here we give the following table to show the type of the variable f, g and the lambda expression n_{a}, n_{b}, n_{g}, n_{f}. Note that the variable f has different types in its three occurrences l_{f}, l_{a} and l_{b}.

f(l_{f}) : (i →^{ζ_{1}} i) →^{ζ_{2}} i
f(l_{a}) : (i →^{ζ′_{1}} i) →^{ζ′_{2}} i
f(l_{b}) : (i →^{ζ′′_{1}} i) →^{ζ′′_{2}} i
g :  i →^{ζ′_{g}} i
n_{a} :  i →^{ζ_{a}} i
n_{b} :  i →^{ζ_{b}} i
n_{g} :  (i →^{ζ′_{g}} i) →^{ζ_{g}} i
n_{f} :  ((i →^{ζ_{1}} i) →^{ζ_{2}} i) →^{ζ_{3}} i

The constraint set is the union of following inequalities:

Eff ((i →^{ζ_{1}} i) →^{ζ_{2}} i ≤ (i →^{ζ′_{1}} i) →^{ζ′_{2}} i),

ζ_{a} ⊇ {n_{a}},

Eff (i →^{ζ_{a}} i ≤ i →^{ζ′_{1}} i),

Eff ((i →^{ζ_{1}} i) →^{ζ_{2}} i ≤ (i →^{ζ′′_{1}} i) →^{ζ′′_{2}} i),

ζ_{b} ⊇ {n_{b}},

Eff (i →^{ζ_{b}} i ≤ i →^{ζ′′_{1}} i),

ζ_{3} ⊇ {n_{f}} ∪ ζ′_{2} ∪ ζ′′_{2}, ζ_{g} ⊇ {n_{g}} ∪ ζ′_{g},

Eff ((i →^{ζ′_{g}} i) →^{ζ_{g}} i ≤ (i →^{ζ_{1}} i) →^{ζ_{2}} i)

which is equivalent to :

{ζ′_{2} ⊇ ζ_{2}, ζ_{1} ⊇ ζ′_{1}, ζ_{a} ⊇ {n_{a}}, ζ′_{1} ⊇ ζ_{a}, ζ′′_{2} ⊇ ζ_{2}, ζ_{1} ⊇ ζ′′_{1}, ζ_{b} ⊇ {n_{b}}, ζ′′_{1} ⊇ ζ_{b}, ζ_{3} ⊇ {n_{f}} ∪ ζ′_{2} ∪ ζ′′_{2}, ζ_{g} ⊇ {n_{g}} ∪ ζ′_{g}, ζ_{2} ⊇ ζ_{g}, ζ′_{g} ⊇ ζ_{1}} The minimal solution of this constraint set is as below :

ζ_{a} ↦ {n_{a}},
ζ_{b} ↦ {n_{b}},
ζ′_{1} ↦ {n_{a}},
ζ′′_{1} ↦ {n_{b}},
ζ_{1} ↦ {n_{a}, n_{b}},
ζ′_{g} ↦ {n_{a}, n_{b}},
ζ_{g} ↦ {n_{a}, n_{b}, n_{g}},
ζ_{2} ↦ {n_{g}, n_{a}, n_{b}},
ζ′_{2} ↦ {n_{g}, n_{a}, n_{b}},
ζ′′_{2} ↦ {n_{g}, n_{a}, n_{b}},
ζ_{3} ↦ {n_{f}, n_{g}, n_{a}, n_{b}}

5.4 Related Work

Subtyping [Cardelli88] adds flexibility to type systems by allowing type coercions to be performed if a type mismatch occurs. It relaxes the form of the type constraints from equations X = Y to inclusions X ⊆ Y. The subtyping problem is reduced to the question of whether a system of inclusion constraints has a solution. However there have been no general results on solving inclusion constraints. The algorithms for type inference based on solving inclusion constraints are quite restrictive [Wand87, Stansifer88, Aiken93, Fuh88, Benjamin92]. The subtyping effect system limites the subtype to a subsumption relation on effects. If classical types of expressions are known, the subtyping-based type and effect inference is reduced to solving effect constraints.

Subtyping in effect systems has been previously introduced in explicitly typed languages [Gifford87, Consel93]. There, a subsumption rule similar to the one presented above was used, but since only type checking was performed, its treatment was simpler than ours. The subtyping approach introduced in my thesis shows that type and effect reconstruction may be performed in an implicitly typed language.

Previous effect systems [Talpin92-1, Dornic91, Tang92] have used subeffecting that forces a function to have an identical type in different call contexts. My thesis introduces subtyping that allows the same function to have different types for different function calls, as long as they obey certain subtype relation. This subtyping effect system avoids effect information to be merged together when forcing two types to be identical, thus improving the accuracy of effect systems based on subeffecting.

5.5 Conclusion

We introduced subtyping in effect systems that allows a function to have different types in different call contexts, as long as they obey certain subtype relation. This subtyping effect system avoids effect information to be merged together when forcing two types to be identical, thus collecting more precise effect information than the previous effect system based on subeffecting. We defined the subtype relation, presented the subtyping rule in the static semantics, discussed the reconstruction algorithms S and proved it sound and complete w.r.t. the static semantics.

52 CHAPTER 5. SUBTYPING EFFECT SYSTEMS

Separate Abstract Interpretation

Type and effect information can be used to extend abstract interpretation in the context of separate compilation.

6.1 Introduction

Abstract interpretation is another basic method for performing static analysis of programs. It is based on denotational semantics by approximating the fixpoint nature of the language semantics. If the abstract interpretation approach performs more precise static analysis due to its more operational nature, effect systems support separate compilation more naturally via module signatures. We introduce the new notion of separate abstract interpretation that combines two approaches in a single framework. It extends abstract interpretation in the context of separate compilation based on the type and effect information of module signatures. Types, enriched with effect information, are used to conservatively approximate abstract values of the free variables of programs, thus enabling abstract interpretation to be performed on non-closed expressions. We use control-flow analysis as a motivating example of this new idea.

Shivers′ thesis [Shivers91] presents a control-flow analysis based on abstract interpretation. Since a CPS form is used as intermediate representation of programs, control transfers are uniformly represented as tail-recursive function calls. Since this abstract interpretation approach is built on the fixpoint approximation technique, it can distinguish between call environments, thus allowing precise control-flow analysis. Nevertheless fixpoint approximation requires the syntax of function bodies to be known and thus fails to support separate compilation.

Separate abstract interpretation use type and control-flow information to approximate abstract values of free variables in an expression. The basis of the separate abstract interpretation approach is that the abstract semantics of control-flow analysis defined in Shivers’ thesis is consistent with the effect semantics used in effect systems. Types describe the structure of values. In particular, from the latent definition d of a function type t′ →^{d} t, one can determine the set of functions this type may correspond to, together with their control-flow behavior. From such types, one can define conservative approximations of abstract values which are used to pursue the abstract interpretation. We have proved that this new static system conservatively extends the abstract interpretation system and retains all its properties. The control-flow analysis expressed by separate abstract interpretation is as precise as the abstract interpretation approach on closed expressions, but is also able to tackle expressions with free variables by using type and control-flow information to approximate their abstract values.

In the remainder of the chapter, we give the syntax and semantics of CPS programs (Section 6.2), describe an abstract interpretation for control-flow analysis (Section 6.3), adapt the type and effect system of Chapter 4 to CPS programs (Section 6.4), show how these two techniques can be merged together (Section 6.5) to perform separate abstract interpretation (Section 6.6), discuss optimizations for increasing its flexibility and accuracy (Section 6.7), discuss the related work (Section 6.8), before concluding (Section 6.9). All proofs are presented in Appendix 4.

6.2 Dynamic Semantics

6.2.1 CPS Syntax

Since Shivers’s abstract interpretation approach uses CPS-transformed programs, we need to define an extended syntax for CPS programs. The main difference with the language defined in Chapter 1 is the introduction of binary functions (to deal with continuation arguments) and the restriction of arguments to self-evaluating expressions.

a ::= x  value identifier
(λn (x k) e) user-defined function
(λn (x) e) continuation function
e ::= (a a′ a′′)l function application
(a a′)l  continuation application

User-defined functions are always binary, while continuation functions are unary. In the sequel, without loss of generality, we only specify the semantics of unary functions and calls. By convention, we use k as identifiers of continuation functions.

6.2.2 Definition

The dynamic semantics not only defines the values of expressions, but also keeps track of control-flow information during evaluation. We restrict the presentation of the dynamic semantics to CPS expressions.

Following [Shivers91], we use the notion of contours to keep track of scoping information. A contour b is a list of labels of function calls describing the current call path. A contour environment (also called a call environment) β maps any variable to the call path that precedes its actual value binding. A value v is either an integer or a closure. A closure cl is composed of a lambda expression (including the function label, argument name and function body) and contour environment. A binding environment E is a finite map from pairs of identifiers and contours to values, recording the bindings of identifiers in a given contour.

b ∈ Contour  = LCall^{∗}  contour
β ∈ ContourEnv = Id ↦ Contour  contour environment
v ∈ Value  = Int + Closure  value
cl ∈ Closure  = Fun ∗ ContourEnv  closure
E ∈ Binding  = Id ∗ Contour ↦ Value binding environment

The control-flow information records the set of functions called at a given call environment. It is defined as a set of tuples {(l, β, s)} where the functions in s are called at call site l and the call environment β; we write such tuples {(l, β) ⇝ s}. In the dynamic semantics, this set is always a singleton. We use sets to be compatible with the subsequent non-standard semantics, where they usually have more than one element. The emptyset ∅ indicates the absence of control-flow information.

c ∈ Control = P(LCall ∗ ContourEnv ∗ P(LFun)) control-flow information

The dynamic semantics is specified by a set of inference rules [Plotkin81]. The usual value environment is split in Shivers’ approach in two components: a contour environment β and a binding environment E. The purpose of this uncoupling is to separate the syntactic component of closures from their semantic aspect. This is of outmost importance when performing abstract interpretation where this syntactic component is furthermore restricted to finite expressions.

The inference rule β, E ⊢ a → v associates the argument a in the contour environment β and global binding environment E with the value v it evaluates to. In the (var) rule, the value of x is retrieved from the binding environment E according to the contour where it was bound (recorded by the current contour environment β). In the (abs) rule, the closure is built with its lambda expression and current contour environment. Note that since abstraction expressions are uniquely identified by their function label, we use the function label n instead of the lambda expression.

(var) : β, E ⊢ x → E(x, β(x))
(abs) : β, E ⊢ n → (n, β)

The inference rule b, β, E ⊢ e → v, c associates the function application e in the current contour b, contour environment β and global binding environment E with (1) the value v it evaluates to and (2) the control-flow information c recording the controlflow traces during its evaluation. In the (app) rule, control reaches the function call site l in the contour environment β, binding environment E and contour b, where the function n is called. Then control enters the function body e, whose control-flow information is c. Note that the binding environment E is global to the whole expression evaluation.

(app) : β, E ⊢ a → (λn(x) e, β′) β, E ⊢ a′ → v′ b′ = b.l b′, β′[x ↦ b′], E ⊢ e → v, c E(x, b′) = v′ b, β, E ⊢ (a a′)l → v, c ∪ {(l, β) ⇝ {n}}

6.3 Abstract Interpretation Semantics

In Shivers’ thesis, first-order control-flow analysis (1CFA) is performed with an abstract interpretation. The contour of the dynamic semantic, which is a call path, is abstracted to a single call site, which is the last element of the call path. Shivers uses a denotational approach for specifying his analysis; we give here a new presentation of this technique using an operational framework which allows us to merge it nicely with the type and effect approach (see Section 6.5).

6.3.1 Definition

The abstract domains correspond to those in the dynamic semantics, except that, since control-flow analysis only deals with functions and ignores integers, values are abstracted to sets of abstract closures. The empty set ∅ represents any integer.

b̂ ∈ Ĉontour  = LCall  contour
β̂ ∈ ĈontourEnv = Id ↦ Ĉontour  contour environment
v̂ ∈ V̂alue  = P(Ĉlosure)  value
ĉl ∈ Ĉlosure  = Fun ∗ ĈontourEnv  closure
Ê ∈ B̂inding  = Id ∗ Ĉontour ↦ V̂alue  binding environment
ĉ ∈ Ĉontrol  = P(LCall ∗ ĈontourEnv ∗ P(LFun)) control-flow information

The inference rule β̂, Ê ⊢ a → v̂ associates the argument a in the contour environment β̂ and global binding environment Ê with the value v̂ it evaluates to.

(var) : β̂, Ê ⊢ x → Ê(x, β̂(x))
(abs) : β̂, Ê ⊢ n → {(n, β̂)}

The inference rule β̂, Ê ⊢ e → v̂, ĉ associates the function application e in the contour environment β̂ and global binding environment Ê with (1) the value v̂ it evaluates to and (2) the control-flow information ĉ. In the (app) rule, when control reaches the function call site l in the contour environment β̂ and binding environment Ê, the function a is evaluated to a set of closures, while the actual argument a′ is evaluated to its value v̂′. Each function n_{i} is possibly called at l at the call environment β̂ from which control transfers to its function body e_{i}. Note that, compared to the dynamic semantics, the call path b̂′ is limited to a single call site; so, calls to the same function but in different environments in the dynamic semantics may get merged together.

(app) : β̂, Ê ⊢ a → \{(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i}) | i = 1 … r\} β̂, Ê ⊢ a′ → v̂′ b̂′ = l \begin{matrix}β̂′_{i}[x_{i} ↦ b̂′], Ê ⊢ e_{i} → v̂_{i}, ĉ_{i} \\ Ê(x_{i}, b̂′) = v̂′ \end{matrix} \} i = 1 … r β̂, Ê ⊢ (a a′)l → ∪_{i=1}^{r}v̂_{i}, ∪_{i=1}^{r}(ĉ_{i} ∪ \{(l, β̂) ⇝ \{n_{i}\}\})

where [x_{i} ↦ v_{i} | i = 1..n] is shorthand for [][x_{1} ↦ v_{1}]...[x_{n} ↦ v_{n}] and [] is the empty constant function.

6.3.2 Correctness

Since the abstract interpretation semantics is defined on finite domains, it terminates. We prove it is well-formed and consistent w.r.t. the dynamic semantics.

Contour environments β̂, global binding environments Ê and abstract values v̂ are related. We define a well-formedness relation WF between them that ensures that free variables of abstract closures are appropriately bound: Definition 6.1 (Well-Formedness)

WF(v̂, Ê) ⇔ ∀(n, β̂) ∈ v̂, WF(β̂, Ê)
WF(β̂, Ê) ⇔ ∀x ∈ Dom(β̂), (x, β̂(x)) ∈ Dom(Ê) ∧ WF(Ê(x, β̂(x)), Ê)

Using this definition, we prove that the abstract interpretation semantics is well-formed.

Lemma 6.1 If β̂, Ê ⊢ a → v̂ and WF(β̂, Ê), then WF(v̂, Ê).

Proof By direct application of Definition 6.1.

Theorem 6.1 (Well-Formedness of Abstract Semantics) If β̂, Ê ⊢ e → v̂, ĉ and WF(β̂, Ê), then

• (v̂, Ê) is well-formed.

• All (β̂′, Ê′) used in the → derivation tree of e are well-formed.

We define the ≤ relation as an approximation relation between abstract values: (v̂, Ê) ≤ (v̂′, Ê′) if (v̂′, Ê′) is a conservative approximation of (v̂, Ê). This relation can be straightforwardly extended to compare exact and abstract values.

Definition 6.2 (Consistency of Abstract Values) For the well-formed (v̂, Ê) and (v̂′, Ê′),

(v̂, Ê) ≤ (v̂′, Ê′) ⇔ ∀(n, β̂) ∈ v̂, ∃β̂′, s.t. (n, β̂′) ∈ v̂′ ∧ (β̂, Ê) ≤ (β̂′, Ê′)
(β̂, Ê) ≤ (β̂′, Ê′) ⇔ ∀x ∈ Dom(β̂), x ∈ Dom(β̂′) ∧ (Ê(x, β̂(x)), Ê) ≤ (Ê′(x, β̂′(x)), Ê′)

We next define the ⊑ relation as an approximation relation between abstract controlflow effects: c ⊑ c′ if c′ is a conservative approximation of c. In other words, c is a more precise control-flow information than c′. Definition 6.3 (Accuracy of Abstract Effects)

c ⊑ c′ ⇔ ∀(l, β̂) ⇝ s ∈ c, ∃β̂′, s′ s.t. (l, β̂′) ⇝ s′ ∈ c′ ∧ s ⊆ s′

Using the previous definitions, we can express that the abstract semantics safely approximates the dynamic one for both arguments and expressions: Lemma 6.2

\begin{matrix}β, E ⊢ a → v \\ β̂, Ê ⊢ a → v̂ \\ (β, E) ≤ (β̂, Ê) \end{matrix} \} ⇒ (v, E) ≤ (v̂, Ê)

Proof By direct application of Definition 6.2. Theorem 6.2 (Consistency of Abstract Semantics)

\begin{matrix}b, β, E ⊢ e → v, c \\ β̂, Ê ⊢ e → v̂, ĉ \\ (β, E) ≤ (β̂, Ê) \end{matrix} \} ⇒ \{ \begin{matrix}(v, E) ≤ (v̂, Ê) \\ c ⊑ ĉ \end{matrix}

6.4 Effect System Semantics

We designed in Chapter 4 an effect system to perform 0th-order control-flow analysis in which all call environments are collapsed together. We adapt below this system to CPS expressions.

6.4.1 Definition

A type t can either be the basic type int, a user-defined function type (t′ ∗ t′′) →^{d} t or continuation function type t′ →^{d} t. The latent definition d is a set of possibly aliased functions n_{i} of the same data type, together with their control-flow effect c̄_{i}. A type environment E is a finite map from identifiers to types.

d ∈ Def  = {(n, c̄)} | d′ ∪ d  function definition
t ∈ Type = int | (t′ ∗ t′′) →^{d} t | t′ →^{d} t type
E ∈ TEnv = Id ↦ Type  type environment
c̄ ∈ Ĉontrol

The control-flow effect c̄ of an expression records all the function calls that possibly occur during its evaluation. Since this type and effect semantics does not keep track of call environments, all contour environments that appear in the domain of control-flow effects are unknown, and thus denoted by the empty constant function [].

The inference rule E ⊢ a : t associates the argument a in the type environment E with its type t. In the (abs) rule, the function label n paired with its control-flow effect c̄ is added to the latent definition d of the function type. These rules use implicit subeffecting by adding more functions to d, thus allowing functions of the same data type to be gathered together. This can be used whenever a type mismatch occurs in an application.

(var) : E ⊢ x : E(x)

(abs) : \begin{matrix}Ex[x ↦ t′] ⊢ e : t, c̄ \\ (n, c̄) ∈ d \\ E ⊢ (λn (x) e) : t′ →^{d} t \end{matrix}

The inference rule E ⊢ e : t, c̄ associates the function application e with its type t and control-flow effect c̄. In the (app) rule, the latent definition of the function type is used to determine all the functions n possibly called at the call site l and their possible control-flow effect c̄.

(app) : E ⊢ a : t′ →^{d} t E ⊢ a′ : t′ E ⊢ (a a′)l : t, ∪_{(n,c̄)∈d}(c̄ ∪ {(l, []) ⇝ {n}})

6.4.2 Correctness

We prove that the type and effect semantics is a conservative approximation of the abstract semantics, which means that the abstract interpretation performs more precise control-flow analysis than the effect system.

To define the consistency between the abstract interpretation and the effect system, we introduce the “:” relation between abstract values, abstract environments and types, noted as (v̂, Ê) : t. This can be easily extended to environments.

Definition 6.4 (Types of Abstract Values) For the well-formed (v̂, Ê),

(∅, Ê) : int
(v̂, Ê) : t ⇔ ∀(n, β̂) ∈ v̂, ∃E, s.t. (β̂, Ê) : E ∧ E ⊢ n : t
(β̂, Ê) : E ⇔ ∀x ∈ Dom(β̂), x ∈ Dom(E) ∧ (Ê(x, β̂(x)), Ê) : E(x)

Using these definitions, we can express that the type semantics conservatively approximates the abstract semantics for both arguments and expressions.

Lemma 6.3

\begin{matrix}E ⊢ a : t \\ β̂, Ê ⊢ a → v̂ \\ (β̂, Ê) : E \end{matrix} \} ⇒ (v̂, Ê) : t

Proof By direct application of Definition 6.4.

Theorem 6.3 (Types of Abstract Semantics)

\begin{matrix}E ⊢ e : t, c̄ \\ β̂, Ê ⊢ e → v̂, ĉ \\ (β̂, Ê) : E \end{matrix} \} ⇒ \{ \begin{matrix}(v̂, Ê) : t \\ ĉ ⊑ c̄ \end{matrix}

6.5 Approximating Abstract Values

As stated before, control-flow analysis by abstract interpretation is more precise than the one based on the type and effect inference system since it distinguishes between call environments. It however fails to support separate compilation because the value environments β̂ and Ê are unknown for separately compiled expressions. Note that the type environment E would be available in this setting.

6.5.1 Approximation Function A

The key idea is to determine a priori the unknown abstract value environment from the type environment, therefore extending the abstract interpretation technique to support separate compilation. The approximation function A takes a type t and returns its abstract value v̂, along with a binding environment Ê that binds the free variables of v̂. Abstract closures are thus either built from actual function definitions or approximated from function types.

The type int denotes integers; its abstract value is thus ∅ and its binding environment [].

A(int) = (∅, [])

The function type (t′ ∗ t_{0}) →^{d} t_{1}, where d is {(n_{i}, c̄_{i}) | i = 1 … q}, describes a set of user-defined functions n_{i} with their control-flow effect c̄_{i} possibly occurring when calling n_{i}. Since the program is in CPS form, t_{0} is a continuation type t →^{d′} t_{1} where t is the type of the result value passed to the final continuation. Thus the abstract value v̂′ corresponding to the function type is a set of closures {(λ_{n_{i}}(xk_{i}) e_{i}), β̂_{i} | i = 1 … q} in which the body e_{i} simulates the control-flow effect c̄_{i} and the contour environment β̂_{i} binds a fresh variable x_{i} to a fresh coutour l_{i}. The binding environment Ê′ corresponding to the function type maps the pair x_{i} and l_{i} to the abstract value v̂ corresponding to the return type t. By binding x_{i} to v̂ in Ê′ and applying, in e_{i}, the final continuation k_{i} to x_{i} (see below), the abstract value v̂ of the result type is passed to its final continuation k_{i}.

A((t′ ∗ t_{0}) →^{d} t_{1}) = let {x_{i}}, {l_{i}} and l fresh

t_{0} = t →^{d′} t_{1}

(v̂, Ê) = A(t)

{e_{i}} = {S(c̄_{i}, k_{i}, x_{i}, l)}

v̂′ = {(λ_{n_{i}}(x k_{i}) e_{i}, [x_{i} ↦ l_{i}]) | i = 1 … q} Ê′ = Ê[(x_{i}, l_{i}) ↦ v̂ | i = 1 … q]

in (v̂′, Ê′) where d = {(n_{i}, c̄_{i}) | i = 1 … q} c̄_{i} = {(l_{j}, []) ⇝ {n_{j1} … n_{jr}} | j = 1 … s}

Each closure body e_{i} simulates the control-flow effect c̄_{i} where, for each call site l_{j}, all n_{jk} functions may be called. The expression S(c̄, k, x, l) simulates the control-flow effect c̄ and, eventually, applies the continuation k to the result x at call site l. It is defined by induction on control-flow effects as below:

S([], k, x, l)  = (k x)l
S(c̄′ ∪ {(l′, []) ⇝ {n_{1} … n_{r}}}, k, x, l) = S′({n_{1} … n_{r}}, c̄′, l′, k, x, l)
S′(∅, c̄′, l′, k, x, l)  = S(c̄′, k, x, l)
S′(s′ ∪ {n′}, c̄′, l′, k, x, l)  = ( (λn′(k′) S′(s′, c̄′, l′, k, x, l)) k )l′
where k′ is fresh

At each call site l′ in c̄, the function S calls S′ which is recursively defined on the set of functions {n_{1} … n_{r}} possibly called at l′. Simulating the behavior of c̄ may require replicating call site labels; this is nonetheless acceptable here since this abstract value is automatically generated.

This general definition of S being somewhat notationally confusing, we give below an example of a closure body for the simple control-flow effect c̄:

c̄ = {(l_{1}, []) ⇝ {n_{1}}, (l_{2}, []) ⇝ {n_{2}, n_{3}}}

where the number of call sites is limited to two, and each call site can only call one or two functions. The corresponding closure body S(c̄, k_{i}, x_{i}, l) is then:

( (λ_{n_{1}}(k_{1})

( (λ_{n_{2}} (k_{2})
( (λ_{n_{3}} (k_{3})
(k_{i} x_{i})l)
k_{i} )_{l_{2}})
k_{i} )_{l_{2}})

k_{i} )_{l_{1}}

6.5.2 Correctness of A

The approximation function A has the following properties :

Lemma 6.4 (Well-Formedness of A(t)) A(t) is well-formed.

Note that the abstract values v̂′ defined by A include simulated call environments whose domains contain only fresh variables. We thus extend the approximation relation ≤ to compare the abstract values and the approximated ones in the following way:

Definition 6.5 (Consistent Abstract Values) For the well-formed (v̂, Ê) and (v̂′, Ê′), if (v̂′, Ê′) is defined via A, then

(v̂, Ê) ≤ (v̂′, Ê′) ⇔ ∀(n, β̂) ∈ v̂, ∃β̂′, s.t. (n, β̂′) ∈ v̂′

Using this extended definition, we get:

Lemma 6.5 (Consistency of A(t)) If (v̂, Ê) : t, then (v̂, Ê) ≤ A(t)

Since simulated call environments do not correspond to actual call environments, we define, for the purpose of comparing them, a function D that deletes these simulated environments in the control-flow effects obtained by abstract interpretation.

\begin{aligned}D([]) & = [] \\ D(ĉ ∪ \{(l, β̂) ⇝ s\}) & = D(ĉ) ∪ \{(l, []) ⇝ s\} \end{aligned}

Using the initial identity continuation Id at a given call site l_{k}, the abstract interpretation of any of the q expressions e_{i}, built by the function S from the control-flow effect c̄_{i} given by the type semantics, yields a control-flow effect ĉ_{i} which, modulo D, is the same as c̄_{i}.

Lemma 6.6 (Simulation) For any β̂_{1} and Ê_{1}, if

β̂_{1}[x_{i} ↦ l_{i}][k_{i} ↦ l_{k}], Ê_{1}[(x_{i}, l_{i}) ↦ v̂][(k_{i}, l_{k}) ↦ {Id}] ⊢ S(c̄_{i}, k_{i}, x_{i}, l) → v̂, ĉ_{i}

then D(ĉ_{i}) = c̄_{i} ∪ {(l, []) ⇝ {Id}}.

6.6 Separate Abstract Interpretation

Separate abstract interpretation uses types and effects to compute conservative approximations of abstract values of the free variables occurring in a separately compiled CPS expression e. These values are used to create initial environments in which the classical abstract interpretation is performed. These initial abstract value environments β̂_{0} and Ê_{0} are defined via the function A, based on the type environment E of e.

Given a CPS expression e, its initial contour environment β̂_{0} maps free variables to the fresh call site labels, since their actual binding call sites are unknown. Its initial binding environment Ê_{0} is defined not only on the free variables of e, but also on those introduced by A; these additional identifiers are bound in the additional binding environments Ê given by A.

β̂_{0} = [x ↦ l | x ∈ Dom(E) ∧ fresh l]
Ê_{0} = ∪_{x∈Dom(E) ∧ (v̂,Ê)=A(E(x))} Ê[(x, β̂_{0}(x)) ↦ v̂]

where ∪ is the function union with the property that (f ∪ g)(x) = f(x) ∪ g(x).

The approximated initial environments have the following properties, corresponding to those of the approximation function A.

Lemma 6.7 (Well-Formedness of (β̂_{0}, Ê_{0})) (β̂_{0}, Ê_{0}) is well-formed.

Lemma 6.8 (Consistency of (β̂_{0}, Ê_{0})) If (β̂′_{0}, Ê′_{0}) : E, then (β̂′_{0}, Ê′_{0}) ≤ (β̂_{0}, Ê_{0})

Classical abstract interpretation can then simply be applied on e with these approximated initial environments:

β̂_{0}, Ê_{0} ⊢ e → v̂, ĉ

to implement the notion of separate abstract interpretation. Thanks to these approximated environments, we extended the abstract interpretation approach to support separate compilation. This new interpretation enjoys all the properties of the abstract interpretation semantics presented above, i.e. it terminates and is well-formed. It is thus a conservative approximation of abstract interpretation.

Theorem 6.4 (Separate Abstract Interpretation) Separate abstract interpretation is a conservative extension of abstract interpretation.

6.7 Optimizations

6.7.1 Subtyping Effect Systems

As stated in Chapter 5, subtyping can be introduced to improve the accuracy of effect systems based on subeffecting. Therefore we can extend abstract interpretation with subtyping effect systems to perform more precise control-flow analysis.

6.7.2 Flexibility of Abstract Semantics

The abstract interpretation semantics defined in Section 6.3 restricts a lambda expression n in the value environment β̂, Ê to a singleton {(n, β̂)}, which limits the number of programs derivable by the abstract semantics. To increase the flexibility of the abstract semantics, we could adjust (abs) rule to (abs′), which allows a lambda expression to admit a larger abstract value as long as its type is persevered.

(abs′) : \begin{matrix}(β̂, Ê) : E \\ E ⊢ n : t \\ WF(v̂, Ê) \\ (v̂, Ê) : t \\ β̂, Ê ⊢ n → \{(n, β̂)\} ∪ v̂ \end{matrix}

By direct application of Definition 6.1 and Definition 6.4, we can see that the (abs′) rule preserves the properties of (abs), namely (1) well-formedness, i.e. if WF(β̂, Ê), then WF({(n, β̂)} ∪ v̂, Ê) and (2) typability, i.e. ({(n, β̂)} ∪ v̂, Ê) : t. Thus this new abstract semantics enjoys all of the properties (see Section 6.3 and Section 6.4) of the previous abstact semantics, but is more flexible. It terminates, is well-formed, is a conservative approximation of the dynamic semantics, and is more precise than the type semantics.

6.7.3 Local Control-Flow Effects

Even though the previously described approximation function A enables abstract interpretation to be applied in the presence of separate compilation, it has the major drawback of limiting its accuracy. Indeed, in the function types of CPS expressions, the control-flow effects in their latent definitions d represent not only the local control-flow effects of function bodies but also,via final continuation calls, those of the continuation of the program. Consequently, the accuracy of separate abstract interpretation is only as good as the one of the type and effect analysis.

To improve the analysis requires the use of A on types restricted to local controlflow effects. This can be achieved by computing the abstract values of the free variables on the basis of their direct, non-CPS type in the following way.

Using the previous notations, the continuation type t_{0} = t →^{d′} t_{1}, where d′ = {(n′_{i}, c̄′_{i}) | i = 1 … p}, describes a set of continuation functions n′_{i} and their control-flow effect c̄′_{i}. User-defined functions of type (t′ ∗ t_{0}) →^{d} t_{1}, where d = {(n_{i}, c̄_{i}) | i = 1 … q}, accept continuations of type t_{0}, beside the argument of type t′. The control-flow effects c̄_{i} of their bodies include the control-flow effects that correspond to applying the final continuation to their result. By subtracting this control-flow effect ∪_{i=1}^{r}c̄′_{i} from c̄_{i}, the remaining effect only corresponds to the local control-flow effect of the body of the function n_{i}. This is equivalent to the control-flow effect recorded in the corresponding direct function type, if one ignores all continuation calls in CPS types.

To summarize, given a non-closed expression e, control-flow analysis using separate abstract interpretation is performed according to the following steps:

1. Apply type and effect inference to get the type environment E of e.

2. Use the function A onto E to approximate the corresponding initial abstract value environment (β̂_{0}, Ê_{0}).

3. Transform e to its CPS form e′.

4. Apply the classical abstract interpretation algorithm to e′, based on (β̂_{0}, Ê_{0}), to get the control-flow information.

6.8 Related Work

In Shivers′s thesis [Shivers91], control-flow analyses of arbitrary order (nCFA, where n is the order) on programs written in continuation-passing style (CPS) [Appel89] are defined and performed by using an abstract interpretation approach. These controlflow analyses are able to distinguish different call environments but fail to support separate compilation, thus limiting their real-world application.

Effect systems extend type systems with effect information. Just as types describe the possible values of expressions, effects describe their possible evaluation behaviors. Our previous papers [Tang92, Tang93] presented a type and control-flow effect system where the inferred control-flow effects of expressions describe all control-flow traces possibly occurring during their evaluation. This analysis supports separate compilation but collapses call environments together, thus is less precise.

Here, we extend the abstract interpretation approach for 1CFA to support modularity, i.e. separate compilation, by approximating unknown value environments of expressions via their type environments. Thus our control-flow analysis performs 1CFA, and possibly nCFA, even in the presence of separate compilation.

6.9 Conclusion

This chapter introduced a new technique to extend abstract interpretation approach in the context of separate compilation based on type and effect information. This separate abstract interpretation makes the control-flow analysis as effective as the abstract interpretation approach on closed expressions, but is also able to tackle expressions with free variables, using their type to approximate their abstract value. We proved that the control-flow information obtained by this new analysis is a conservative approximation of abstract interpretation and is more precise than the type and effect system.

Higher-Order Escape Analysis

Control-flow analysis is helpful to choose an efficient closure allocation strategy.

7.1 Introduction

Escape analysis helps compilers optimize closure allocation in functional program implementation. It determines, at compile time, the free variables of functions that outlive the environment in which they are defined. Therefore non-escaping variables can be safely allocated in the stack while reserving the heap only for escaping ones. We present a new static escape analysis based on the control-flow effect systems (Chapter 3 4, 5). The escape analysis can be performed in presence of higher-order functions, imperative constructs and separate compilation. We design a stack-based abstract machine where closures are allocated in the stack and whenever functions are called, their escaping free variables are copied from the stack to the heap.

In the sequel, we present a static criteria for identifying escaping functions (Section 7.2), design a stack-based abstract machine to show an optimized allocation strategy (Section 7.3) and discuss related work (Section 7.4) before concluding (Section 7.5).

7.2 Identifying Escaping Variables

7.2.1 Escaping Variables

Function values are represented by compilers as closures. Closures are composed of the function code and the free variables that form its environment. Since functions are first-class values, their free variables may outlive the environment in which they are defined. Here we use integers to specify the lexical level of each expression. The top-level expression has the lexical level 0. The escaping variables do not obey the LIFO stack-allocation strategy used in traditional call mechanism and must be heapallocated. Heap allocation is more general than stack allocation in the sense that heap allocation can be used for all free variables of functions, while stack allocation is only safe for non-escaping ones. However, stack allocation is cheaper than heap allocation because useless storage is simply reclaimed by updating a pointer instead of calling the garbage collector. Finding an efficient allocation strategy for closure environments is therefore important for optimizing compilers of functional languages. A good strategy of closure allocation for functional languages is to stack allocate non-escaping variables of functions while reserving the more expensive heap allocation to escaping ones. The key problem is thus to identify escaping variables at compile time safely and as precisely as possible.

7.2.2 From Types to Escaping variables

Escaping variables can be identified based on the types and control-flow effects inferred by the previously defined control-flow effect systems (see Chapter 3,4,5). For any typechecked function call (e e′) at the lexical level l, e must have a function type t′ →^{c} t where t′ is the type of the argument e′ and t is the result type of this function call. If a function n is returned as the result of this function call, it must be recorded by t via its latent control-flow effects; If e′ is evaluated to a memory location loc, t′ must be ref (t′′). When a function n is allocated in loc during the evaluation of e, it must be recorded by t′′ via its latent control-flow effects. Note that the function type t′ →^{c} t includes the information that helps identify the escaping variables of functions. More precisely, for each function, we identify its escape-level and escape-set. The escape-level is the smallest lexical level at which the function escapes (or infinity if the function does not escape) while its escape-set is the set of free variables of the function body that are bound within its escape-level and definition site. The variables recorded by the escape-set are escaping variables.

To compute this information, we use two environments, LE and EE. The lexical environment LE maps identifiers to the integer lexical levels at which they are bound. The escape-environment EE maps a lexical level l defining a lambda expression to the function type t →^{c} t′; this type records, via the latent control-flow effects possibly present in t or t′, the names of all of the functions that may escape at the level l. A function n, defined at the level l′, escapes at the level l by being either part of the value returned at the level l (its name is free in t′) or stored in a location bound at the level l (its name is free in t); the function n is then said to escape from l′ to l.

7.2.3 Algorithm I

Given a lexical environment LE and an escape-environment EE, the algorithm I updates, for an expression e at the level l, the identification function i. This identification function maps a function name to its escape-set. A function may escape to multiple lexical levels; conservatively, the escape-level is the minimum of them. The escape set records all of the free variables of a function bound at a lexical level larger than the escape-level. These two escape attributes are conservative approximations of their dynamic counterparts.

We assume in I that the expression is completely typed, the type and control-flow information having been previously inferred by the effect systems.

I(e) LE EE l i =

case e

x ⇒ i

(e e′) ⇒ I(e) LE EE l (I(e′) LE EE l i)

(λn (x : t) e′ : t′) ⇒

let el = Min{l | n ∈ fn(EE(l))} es = {y ∈ fv(e) | LE(y) ≥ el}

i′ = I(e′) (LE{x ↦ l})

(EE{l ↦ t →^{∅} t′})

(l + 1) i

in i′{n ↦ es}

where fv computes the set of free variables of expressions and environments, while fn restricts this set to function names. By convention, Min∅ is defined to be infinity. The identification function of a whole program expression p is given by calling I on p with the empty environment, lexical level 0 and the identity function.

The previously computed escaping variables can be used to efficiently allocate closure environments. For any function, only its escaping variables need to be allocated in the heap; the others can, as before, be allocated in the stack. We introduce an abstract machine to show how to use this optimized closure allocation strategy.

7.3 A Stack-based Abstract Machine

7.3.1 Stack Calling Convention

The abstract machine is built upon the stack calling convention. Following compilers of traditional languages [Aho86], an activation record is built for each function call, which records the arguments of the function call, together with other information, such as return point, etc. The activation records are allocated in a control stack, obeying the LIFO strategy. The only difference is that when functions are called, their escaping variables, which do not obey the LIFO stack-allocation strategy, have to be copied from the control stack (the activation records), to the heap, while all other nonescaping free variables remain in the control stack. These heap allocated environments are called escaping environments. Therefore closures in our compiler include two kinds of environments : non-escaping environments recorded in the activation records in the control stack, and escaping environments in the heap. When compiling non-escaping functions, our compiler is as efficient as compiling traditional languages. When escaping functions exist, it is more efficient than compiling other functional languages such as SML or SCHEME [Krantz87, Steele78, Appel87] where the static escape information is unknown or less precise. We present the structure of the abstract machine, describe the semantics of its instructions, and give an algorithm C to transform the programs to a list of instructions.

7.3.2 Structure

The state of the abstract machine is specified by the following five elements :

(Code, Accu, TempS, EsEnv, ContS)

which respectively are :

• User program (Code) : it includes a list of instructions of the abstract machine, which are defined in Section 7.3.3.

• Accumulator (Accu) : it stores the immediate result values of the abstract machine. The values can be integers or closures. The closure is composed of the code of the function body, its escaping environment recorded by EsEnv and nonescaping environment recorded in the activation records ActR;

• Temporary stack (TempS) : it temporarily stores the environments of functions. It is organized as a list of values.

• Escaping environment (EsEnv) : it records the escaping free variables of a function, which is represented as a vector. Accessing escaping variables is by their indices in the vector. All escaping environments are allocated in the heap.

• Control stack (ContS) : it stores the activation records of function calls linked together by the access link. They obey the LIFO allocated strategy. An activation record is composed of the argument of the function call, the access link pointing to another activation record, the return point where control will return at the end of the function call. The return point includes the code and its escaping environment. The environments of functions are recorded in the activation records. Accessing them is by their indices in the linked activation records.

7.3.3 Instructions

The abstract machine has a set of instructions:

• \underline{stack}(i) : accesses the value of a variable in the linked activation records allocated in the control stack ContS via the function access(s, i) where i is its index in the linked activation records. The function access(s, i) accesses the value recorded in the ith activation record starting from s.

access(∅, i)  = fail
access(s′.(v, s, r), 1) = v
access(s′.(v, s, r), i) = access(s, i − 1)

• \underline{heap}(i) : accesses the value of an escaping variable in the escaping environment EsEnv allocated in the heap, where i is its index of in the vector.

• \underline{push}: pushes the current value on the temporary stack TempS.

• \underline{close}(m,c) : closes a function with the code c of its body, its escaping environment including m elements (poped from the temporary stack TempS) and its current activation record (including non-escaping variables).

• \underline{call}: updates the control stack ContS by building a new activation record for the function call. This activation record is formed by the argument of the called function (poped from the temporary stack TempS), the access link (copied from the non-escaping environment in the closure), and the return point (including the rest of code and the current escaping environment). The current escaping environment is updated with the one recorded in the closure and then control is transferred to the code of the function body.

• \underline{return}: updates the control stack ContS by poping the activation record, updates the current escaping environment EsEnv with the one recorded by the return point of the poped activation record and transfers control to the code recorded by the return point.

The semantics of the abstract machine is operationally given by the state transition [Plotkin81] of each instruction.

Code  Accu  TempS  EsEnv  ContS
\underline{stack}(i) ; c  v  a  e  s
c  access(s, i)  a  e  s
\underline{heap}(i) ; c  v  a  e = v_{1}..v_{i}..v_{n}  s
c  v_{i}  a  e  s
\underline{push} ; c  v  a  e  s
c  v  a.v  e  s
\underline{close}(m, c′) ; c  v  a.v_{1} … v_{m}  e  s
c  (c′, {v_{1} … v_{m}}, s)  a  e  s
\underline{call} ; c  v = (c′, e′, s′)  a.v′  e  s
c′  v  a  e′  s.(v′, s′, (c, e))
\underline{return} ; c  v  a  e  s.(v′, s′, (c′, e′))
c′  v  a  e′  s

7.3.4 Translator C

The translator C transforms an expression to a list of instructions of the abstract machine based on the result of previous escaping analysis.

A stack environment E_{s} maps identifiers to their indices in the control stack ContS. A heap environment E_{h} maps escaping variables to their indices in the escaping environment EsEnv. The identification function i maps all function names in the expression e to their escaping variables. Given an identification function i, a stack environment E_{s} and a heap environment E_{h}, the translator C transforms the expression e at the lexical level l into a list of instructions of the abstract machine.

For a variable, if it is an escaping variable then its value is accessed by its index in the escaping environment, otherwise it is accessed in the control stack.

C[[x]] i E_{s} E_{h} l = if x ∈ Dom(E_{h}) then \underline{heap}(E_{h}(x)) else \underline{stack}(l − E_{s}(x))

For an application, the expression in the argument position is compiled and its result is temporarily pushed onto the temporary stack TempS. Then the expression in the function position is compiled, by building its closure. Finally the function is called by constructing its activation record in the control stack ContS.

C[[(e e′)]] i E_{s} E_{h} l = C[[e′]] i E_{s} E_{h} l ; \underline{push} ; C[[e]] i E_{s} E_{h} l ; \underline{call}

For an abstraction, all its escaping variables (recorded by the identification function i) should be copied from the control stack and temporarily stored in the temporary stack TempS. The function is closed with the code of its body, the escaping variables moved from TempS and the current control stack pointer.

C[[(λn (x) e)]] i E_{s} E_{h} l =

let {x_{1}...x_{m}} = i(n)

{i_{1} … i_{m}} = {E_{s}(x_{1})...E_{s}(x_{m})} in \underline{stack}(l − i_{1}) ; \underline{push} ;

⋮

      \underline{stack}(l − i_{m}) ; \underline{push} ;

\underline{close}(m, C[[e]] i (E_{s}[x ↦ l]) ([][x_{1} ↦ 1]...[x_{m} ↦ m]) (l + 1) ; \underline{return})

7.3.5 Example

We use the example exam to show how our abstract machine hehaves.

exam = (λ_{n_{z}} (z) ((λ_{n_{x}} (x) (λ_{n_{y}} (y) x)) z))

After applying previous escape analysis to the program, we get its identification function i which maps the lambda expressions n_{z}, n_{y} and n_{x} to their escaping variables, ∅, ∅ and {x} respectively. The translator C starts from the empty initial environments E_{s} and E_{h} and the initial lexical level 0.

Since the lambda expression n_{z} has no escaping variables, it is closed with the code of its body and the pointer of the current control stack.

C[[(λ_{n_{z}} (z) ((λ_{n_{x}} (x) (λ_{n_{y}} (y) x)) z))]] i [] [] 0 = \underline{close}(0, C[[((λ_{n_{x}} (x) (λ_{n_{y}} (y) x)) z)]] i [z ↦ 0] [] 1 ; \underline{return})

For the function application ((λ_{n_{x}} (x) (λ_{n_{y}} (y) x)) z), the variable z has to be accessed in the stack by \underline{stack}(1); Then the lambda expression n_{x} is compiled.

C[[((λ_{n_{x}} (x) (λ_{n_{y}} (y) x)) z)]] i [z ↦ 0] [] 1 = C[[z]] i [z ↦ 0] [] 1 ; \underline{push} ; C[[(λ_{n_{x}} (x) (λ_{n_{y}} (y) x))]] i [z ↦ 0] [] 1 ;

   \underline{call} ;

where C[[z]] i [z ↦ 0] [] 1 = \underline{stack}(1)

The code for n_{x} is similar to that of n_{z}.

C[[(λ_{n_{x}} (x) (λ_{n_{y}} (y) x))]] i [z ↦ 0] [] 1 = \underline{close}(0, C[[(λ_{n_{y}} (y) x)]] i [z ↦ 0, x ↦ 1] [] 2 ; \underline{return})

Sicnce the lambda expression n_{y} has the escaping variable x, x has to be copied from the control-flow stack ContS to the temporary stack TempS by performing \underline{stack}(1) ; \underline{push}. Then n_{y} is closed by the code of its body, the pointer of the current control stack and its escaping environment (popped from the temporary stack TempS).

C[[(λ_{n_{y}} (y) x)]] i [z ↦ 0, x ↦ 1] [] 2 =

   \underline{stack}(1) ; \underline{push} ;

\underline{close}(1, C[[x]] i [z ↦ 0, x ↦ 1, y ↦ 2] [x ↦ 1] 3 ; \underline{return}) where C[[x]] i [z ↦ 0, x ↦ 1, y ↦ 2] [x ↦ 1] 3 = \underline{heap}(1)

The abstract machine code of the program exam is thus as below :

\underline{close}(0, \underline{stack}(1) ; \underline{push} ;
        \underline{close}(0, \underline{stack}(1) ; \underline{push} ; \underline{close}(1, \underline{heap}(1) ; \underline{return}) ; \underline{return}) ;
        \underline{call} ;
        \underline{return})

7.4 Related Work

Escape information can be identified either at compile time, based on a static analysis of programs, or at run time, using a run-time checking mechanism [Baker92]. Here we only discuss compile-time approaches.

A simple escape analysis was used in the Scheme [Rees88] compilers Rabbit [Steele78] and ORBIT [Krantz87] to optimize closure allocation. These analyses are syntax-based, i.e., the escaping functions are identified by their syntactical context through a recursive walk of expressions. Our analysis is based on the type and control-flow information of expressions, computed by a type and effect inference system, thus is more precise, in particular when dealing with higher-order functions.

A higher-order escape analysis [Goldberg90] on a typed functional language was performed using abstract interpretation. This analysis computes abstract escape functions of the programs based on fixpoint approximations. Our analysis applies an identifying algorithm to the programs based on their types and control-flow information, which makes our analysis process a lower cost; Another benefit of using effect systems is that it can straightforwardly deal with imperative constructs in functional languages thanks to explicit reference types of locations. Another main difference between these two analyses is the definition of escape information, which decides the way that they are used for optimizing closure allocation. Goldberg′s analysis identifies, for each function call, which arguments possibly outlive this function call. The escaping arguments are allocated immediately in the heap whenever the function call is performed. Our analysis identifies, for each function, the free variables that possibly outlive the environment where they are defined. The escaping free variables have to be copied to the heap whenever these functions are called at run time, which makes our system more expansive at run-time application.

Taking the example used in Goldberg’s paper, we can see the differences between these two analyses.

let f x y z = x + y + z g a b = f b a

in g 1 2

In Goldberg’s analysis, abstract escape functions for the function f and g are formed by fixed point iteration. With these abstract escape functions, the system identifies if their arguments escape from the calls to them. Here since 1 and 2 escape from the function call (g 1 2), they have to be allocated in the heap when compiling the function call.

In our analysis, the identifying algorithm identifies that x, y are escaping variables of the function λ_{n_{z}} (z) (x + y + z) from the result type int →^{{n_{z}}} int of (g 1 2). Whenever the function n_{z} is called at run time, their values have to be copied from the stack to the heap.

Finally we compare the accuracy of these two analysis. Generally, the abstract interpretation approach performs more precise analysis than effect systems due to its more operational nature. However, since our escape information is used together with run-time evaluation, only the escaping variables of functions that are reached at run time need to be allocated in the heap, which makes our analysis more precise in some cases, for example, in conditional expressions.

7.5 Conclusion

We presented a new higher-order escape analysis based on type and effect systems, supporting higher-order functions, imperative constructs and separate compilation. The escape analysis determines, at compile time, the free variables of functions that outlive the environment in which they are defined. Based on these compile-time knowledge of escape information, we designed a stack-based abstract machine, where non-escaping variables are safely allocated in the stack and only escaping variables are allocated in the heap.

Conclusion

My thesis work lies on the border of the theory and the practice.

We extend and combine two static analysis approaches – effect systems and abstract interpretation, and study their application in performing control-flow analysis.

We present new control-flow analysis systems based on effect systems. Subtyping is introduced to increase the flexibility of effect systems. The subtype relation is defined by a subsumption relation on effect information. A new type and effect reconstruction algorithm is designed, which for each expression already typed with classical types, reconstructs its type and effect based on subtyping. The subtyping approach allows functions to have different types in different call contexts instead of having a unique type, thus improving the accuracy of effect systems based on subeffecting. The current subtyping effect system is built upon a monotonic type system. However it can be extended to ML polymorphic type systems, which makes subtyping effect systems more powerful. Another open issue is how to use the subtyping effect system in the presence of side-effects.

We introduce the new notion of separate abstract interpretation which combines effect systems and abstract interpretation in a single framework. By approximating abstract values of free variables based on type and effect of module signatures, effect systems provide a method to extend abstract interpretation in the context of separate compilation. This separate abstract interpretation makes the control-flow analysis as effective as the abstract interpretation approach on closed expressions, but is also able to tackle expressions with free variables, using their type to approximate their abstract value.

The goal of control-flow analysis is to implement functional languages more efficiently. The static knowledge of control-flow information plays an important role in optimizing compilers of functional languages, such as interprocedural data-flow optimizations and closure optimizations. There remain a lot of open issues in pragmatic use of this control-flow information. We present an application of control-flow information in optimizing closure allocation. This optimization is based on escape analysis, a direct application of types and control-flow information. The escape analysis identifies the free variables that outlive the lexical scope of function definitions. This compile time knowledge of escaping variables helps compilers choose a more efficient allocation strategy for closures, i.e. non-escaping variables can be safely stored in the stack, while heap allocation is only used for escaping ones.

74 CHAPTER 7. HIGHER-ORDER ESCAPE ANALYSIS

Bibliography

[Aho86] Aho, A. V., Sethi, R. and Ullman, J. D. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

[Aiken93] Aiken A. Type Inclusion Constraints and Type Inference. In Conference on Functional Programming Languages and Computer Architecture. August, 1993.

[Appel87] Appel, A. W. and MacQueen, D. B. A Standard ML compiler. In Functional Programming Languages and Computer Architecture, volume 242 of Lecture Notes in Computer Science. Springer-Verlag, 1987.

[Appel89] Appel, A. W. and Jim, T.Y. Continuation-Passing, Closure-Passing Style. In ACM Symposium on Principles of Programming Languages, pages 293-302, 1989.

[Appel90] Appel, A. W. and Mac Queen, D. B. Standard ML Reference Manual. AT&T Bell Laboratories and Princeton University, October 1990.

[Appel92] Appel, A. W. Compiling with Continuations. Cambridge University Press, 1992.

[Baker92] Baker, H.G. CONS Should not CONS its Arguments, or, a Lazy Alloc is Smart Alloc. In ACM SIGPLAN Notices Volume 27, No.3, 1992.

[Benjamin92] Benjamin, P. Intersection Types and Bounded Polymorphism. In LFCS Report Series, University of Edinburgh, 1992.

[Bondorf93] Bondorf, A. and Jorgensen, J. Efficient Analyses for Realistic Off-line Partial Evaluation. In Journal of Functional Programming, Vol 3, Part 3, Cambridge University Press, July 1993.

[Cardelli84] Cardelli, L. Compiling a Functional Language. In ACM Symposium of LAFP, 1984.

[Cardelli85] Cardelli, L. On Understanding Types, Data-Abstractions, and Polymorphism. In Computing Surveys, 17(4),1985.

[Cardelli88] Cardelli, L. Structural Subtyping and the Notion of Power Type. In ACM Symposium on Principles of Programming Languages, pages 70-79, 1988.

[Consel93] Consel, C. and Jouvelot, P. Separate Polyvariant Binding-Time Analysis. In Technical Report, CRI, Ecole des Mines de Paris, 1993.

[Cousot77] Cousot, P. and Cousot, R. Abstract Interpretation, a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In ACM Symposium on Principles of Programming Languages. 1977.

[Cousot79] Cousot, P. and Cousot, R. Systematic Design of Program Analysis Frameworks. In ACM Symposium on Principles of Programming Languages. 1979.

[Damas82] Damas, L. and Milner, R. Principal type-schemes for functional programs. In ACM Symposium on Principles of Programming Languages, pages 207-212. 1982.

[Deutsch90] Deutsch A. On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications. In ACM Symposium on Principles of Programming Languages, 157-168,1990.

[Dornic91] Dornic, V. and Jouvelot, P. Polymorphic Time Systems for Estimating Program Complexity. In LOPLAS’91, Bordeaux, France, 1991.

[Fuh88] Fuh. Y. and Mishra, P. Type Inference with Subtypes. In European Symposium on Programming, pages 94-114. 1988.

[Gifford87] Gifford, D. K., Jouvelot, P., Lucassen, J. M. and Sheldon, M. A. FX-87 Reference Manual. MIT/LCS/TR-407, MIT Laboratory for Computer Science, September 1987.

[Goldberg90] Goldberg. B. and Park, Y. G. Higher Order Escape Analysis, Optimizing Stack Allocation in Functional Program Implementation. In European Symposium on Programming, volume 432 of the Lectures Notes in Computer Science, pages 152-160. Springer-Verlag, 1990.

[Grundman92] Grundman., D, Stata, R. and Toole, J.O. Mini-DX/DLX – A Pedagogic Compiler, M.I.T, 1992.

[Hammel88] Hammel, R. T. and Gifford, D. K. FX-87 Performance Measurements: Dataflow Implementation. MIT/LCS/TR-421, MIT Laboratory for Computer Science, November 1988.

[Jouvelot88] Jouvelot, P. and Gifford, D. K. The FX-87 Interpreter In International Conference on Computer Languages, 1988.

[Jouvelot89] Jouvelot, P. and Gifford, D. K. Reasoning about Continuations with Control Effects. In International Conference on Progamming Language Design and Implementation. ACM, New-York, 1989.

[Jouvelot91] Jouvelot, P. and Gifford, D. K. Algebraic Reconstruction of Types and Effects. In ACM Symposium on Principles of Programming Languages. 1991.

[Kanellakis89] Kanellakis, P. and Mitchell, J. C. Polymorphic Unification and ML Typing. In ACM Symposium on Principles of Programming Languages, 1989.

[Kelsey89] Kelsey, R.A. Compilation by Program Transformation. Ph.D. Thesis. Yale University, May 1989.

[Krantz87] Krantz, D. ORBIT: An Optimizing Compiler for Scheme. Ph.D. Thesis. Yale University, Feb. 1988.

[Leeuwen90] J. Van Leeuwen. Formal Models and Semantics. In Handbook of Theoretical Computer Science, volume B. The MIT press, 1990.

[Leroy90-1] Leroy, X. The ZINC Experiment: an Economical Implementation of the ML Language. Technical report 117, INRIA, 1990.

[Leroy90-2] Leroy, X. Unboxed Objects and Polymorphic Typing In ACM Symposium on Principles of Programming Languages, 1990.

[Leroy91] Leroy, X. and Weis, P. Polymorphic Type Inference and Assignment. In ACM Symposium on Principles of Programming Languages, 1991.

[Lucassen87] Lucassen, J. M. Types and Effects, Towards the Integration of Functional and Imperative Programming. MIT/LCS/TR-408 (Ph. D. Thesis). MIT Laboratory for Computer Science, August 1987.

[Lucassen88] Lucassen, J. M. and Gifford, D. K. Polymorphic Effect Systems. In ACM Conference on Principles of Programming Languages. ACM, New-York, 1988.

[MacCracken79] MacCracken, N. Investigation of a Programming Language with a Polymorphic Type Structure. Ph. D. Thesis, Syracuse University, 1979.

[MacQueen90] MacQueen, D. B. Modules for Standard ML. In ACM Conference on Lisp and Functional Programming, pages 198-207. ACM Press, New-York, 1990.

[Milner78] Milner, R. A Theory for Type Polymorphism in Programming. In Journal of Computer and Systems Sciences, Vol. 17, pages 348-375. 1978.

[Milner90] Milner, R., Tofte, M. and Harper, R. The Definition of Standard ML. The MIT Press, Cambridge, 1990.

[MIT90] Mini-FX Reference Manual. MIT, 1990.

[Mitchell88] Mitchell, J. C. and Harper, R. The Essence of ML. In ACM Symposium on Principles of Programming Languages, 1988.

[Mycroft81] Mycroft, A. Abstract Interpretation and Optimizing Transformations for Applicative Programs. PhD Thesis, University of Edinburgh. 1981.

[O′Toole90] O’Toole, J. W. Type Abstraction Rules for References: a Comparison of Four which Have Achieved Notoriety. Technical Report 390, MIT Laboratory for Computer Science, 1990.

[Plotkin81] Plotkin, G. A Structural Approach to Operational Semantics. Technical Report DAIMI-FN-19. Aarhus University, 1981.

[Stansifer88] Stanifer, R. Type Inference with Subtypes. In ACM Symposium on Principles of Programming Languages, 1988.

[Robinson65] Robinson, J. A. A Machine Oriented Logic Based on the Resolution Principle. In Journal of the ACM, Vol. 12(1), pages 23-41. ACM, New-York, 1965.

[Rees88] Rees, J. and Clinger W., Editors. Fourth Report on the Algorithmic Language Scheme. September 1988.

[Siekmann89] Siekmann, J. H. Unification Theory. In Journal of Symbolic Computations, volume 7, pages 207-274. Academic Press, 1989.

[Sheldon90] Sheldon, A. M. and Gifford, D. K. Static Dependent Types for First Class Modules. In ACM Conference on Lisp and Functional Programming, 1990.

[Shivers91] Shivers, O. Control-Flow Analysis of Higher-Order Languages. Ph. D. Thesis and Technical Report CMU-CS-91-145, Carnegie Mellon University, Pittsburgh, May 1991.

[Steele78] Steele, G. Rabbit: A Compiler for Scheme. In MIT-AI Technical Report No. 474. MIT Laboratory for Computer Science, May 1978.

[Steele90] Steele, G. L. Common Lisp, the language. Digital Press 1990.

[Stoy77] Stoy, J. E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, 1977.

[Talpin92-1] Talpin, J. P. and Jouvelot, P. Polymorphic Type, Region and Effect Inference. In the Journal of Functional Programming, volume 2, number 3. Cambridge University Press, 1992.

[Talpin92-2] Talpin, J. P. and Jouvelot, P. The Type and Effect Discipline. In IEEE Conference on Logic in Computer Science. Santa Cruz, California, June 1992.

[Talpin93-1] Talpin, J. P. and Jouvelot, P. Compiling FX on the Connection Machine. In Workshop on Static Analysis, Sept 1993.

[Talpin93-2] Talpin, J. P. Type Discipline. PhD Thesis. May 1993

[Tang92] Tang, Y. M. and Jouvelot, P. Control-Flow Effects for Closure Analysis. In proceedings of the 2nd Workshop on Semantics Analysis, Bigre numbers 81-82, pages 313-321. Bordeaux, Octobre 1992.

[Tang93] Tang, Y. M. and Jouvelot, P. Effect Systems with Subtyping. In Technical Report, CRI, Ecole des Mines de Paris 1993.

[Tang94] Tang, Y. M. and Jouvelot, P. Separate Abstract Interpretation for Control-Flow Analysis. International Symposium on Theoretical Aspects of Computer Software. Japan, Avril 1994.

[Tofte87] Tofte, M. Operational Semantics and Polymorphic Type Inference. PhD Thesis and Technical Report ECS-LFCS-88-54, University of Edinburgh, 1987.

[Tofte90] Tofte, M. Type Inference for Polymorphic References. In Information and Computation, 89(1), pages 1-34, 1990.

[Wand87] Wand, M. A simple algorithm and proof for type inference. In Fundamenta Informaticae, volume 10, pages 115-122. North Holland, 1987.

[Wand93] Wand, M. and Steckler, P. Selective and Lightweight Closure Conversion In Technical Report 1993 80 BIBLIOGRAPHY

Appendix 1

Proof of Lemma 3.1

Lemma 3.1 [Monotony of F] If Q and Q′ are two subsets of the domain R.

Q ⊆ Q′ ⇒ F(Q) ⊆ F(Q′)

Proof

Taking any q = (v, t), s.t. q ∈ F(Q)

Since q ∈ F(Q), by the definition of F

(1) q ∈ Q

Since Q ⊆ Q′

(2) q ∈ Q′

Now we prove that q ∈ F(Q′)

• Case v = i Since q ∈ F(Q), by the definition of F

(3) q = (i, int)

From (2)(3), by the definition of F

(4) q ∈ F(Q′)

• Case v = (n, x, e, E) Since q ∈ F(Q), by the definition of F, ∃E s.t.

(5) ∀x ∈ Dom(E), x ∈ Dom(E)

(6) (E(x), E(x)) ∈ Q

(7) E ⊢ (λn (x) e) : t

From (6), since Q ⊆ Q′

(8) (E(x), E(x)) ∈ Q′

From (2)(5)(8)(7), by the definition of F

(9) q ∈ F(Q′)

From (4)(9)

(10) ∀q ∈ F(Q), q ∈ F(Q′)

From (10) F(Q) ⊆ F(Q′) ♣

Proof of Theorem 3.1

Theorem 3.1 [Consistency of Static Semantics]

\begin{matrix}E ⊢ e → v, b \\ E ⊢ e : t, c \\ E : E \end{matrix} \} ⇒ \{ \begin{matrix}v : t \\ b ⊆ c \end{matrix}

Proof By induction on the number of reduction steps of expressions.

• Case of (var)

The hypotheses are

(1) E : E

(2) E ⊢ x → E(x), ∅

(3) E ⊢ x : E(x), ∅

From (2), by (var) in the dynamic semantics (4) x ∈ Dom(E)

From (3), by (var) in the static semantics (5) x ∈ Dom(E)

From (1)(4)(5), by Definition 3.1 E(x) : E(x)

• Case of (abs)

The hypotheses are

(1) E : E

(2) E ⊢ (λn (x) e) → (n, x, e, Ex), ∅

(3) E ⊢ (λn (x) e) : t′ →^{{n}∪c} t, ∅

From (1), by Definition 3.1

(4) Ex : E

From (3)(4), by Definition 3.1

(n, x, e, Ex) : t′ →^{{n}∪c} t

• Case of (rec)

The hypotheses are

(1) E : E

(2) E ⊢ (recn (f x) e) → cl, ∅

(3) E ⊢ (recn (f x) e) : t, ∅

From (2), by (rec) in the dynamic semantics

(4) cl = (n, x, e, E′) where E′ = E[f ↦ cl]

From (3), by (rec) in the static semantics

(5) E′ ⊢ (λn (x) e) : t, ∅ where E′ = E[f ↦ t]

By Definition 3.2, for proving cl : t we have to prove : (cl, t) ∈ gfp(F)

We define Q = gfp(F) ∪ {(cl, t)}

By the definition of gfp(F), for proving (cl, t) ∈ gfp(F) we have to prove : Q ⊆ F(Q)

Taking any q, s.t. q ∈ Q

– Case q ∈ gfp(F) Since gfp(F) ⊆ Q and F is monotonic (6) F(gfp(F)) ⊆ F(Q)

By the definition of gfp(F)

(7) gfp(F) ⊆ F(gfp(F))

From (6)(7)

(8) gfp(F) ⊆ F(Q) thus q ∈ F(Q)

– Case q = (cl, t) From (1), by Definition 3.2 ∀x ∈ Dom(E), x ∈ Dom(E)

(9) (E(x), E(x)) ∈ gfp(F)

From (9), since gfp(F) ⊆ Q

(10) (E(x), E(x)) ∈ Q From (10), since (cl, t) ∈ Q ∀x ∈ Dom(E), x ∈ Dom(E)

(11) (E′(x), E′(x)) ∈ Q

From (11)(5), since (cl, t) ∈ Q, by the definition of F (12) (cl, t) ∈ F(Q) thus q ∈ F(Q)

From (8)(12) Q ⊆ F(Q)

By the definition of gfp(F), since (cl, t) ∈ Q (cl, t) ∈ gfp(F)

By Definition 3.2 cl : t

• Case of (app)

The hypotheses are

(1) E : E

(2) E ⊢ (e e′) → v, b ∪ b′ ∪ b′′ ∪ {n}

(3) E ⊢ (e e′) : t, c ∪ c′ ∪ c′′

From (2), by (app) in the dynamic semantics (4) E ⊢ e → (n, x, e′′, E′), b

(5) E ⊢ e′ → v′, b′

(6) E′[x ↦ v′] ⊢ e′′ → v, b′′

From (3), by (app) in the static semantics

(7) E ⊢ e : t′ →^{c′′} t, c

(8) E ⊢ e′ : t′, c′

From (1)(4)(7) and (1)(5)(8), by inductions

(9) (n, x, e′′, E′) : t′ →^{c′′} t

(10) b ⊆ c

(11) v′ : t′

(12) b′ ⊆ c′

From (9), by Definition 3.1

(13) ∃E′, verifying E′ : E′

(14) E′ ⊢ (λn (x) e′′) : t′ →^{c′′} t

From (14), by (abs) in the static semantics (15) E′[x ↦ t′] ⊢ e′′ : t, c′′′

(16) c′′ = c′′′ ∪ {n}

From (13)(11)

(17) E′[x ↦ v′] : E′[x ↦ t′]

From (17)(6)(15), by induction v : t

(18) b′′ ⊆ c′′′

From (10)(12)(18)(16) b ∪ b′ ∪ b′′ ∪ {n} ⊆ c ∪ c′ ∪ c′′ 86 BIBLIOGRAPHY

Proof of Theorem 4.4

Theorem 4.4 [Soundness] Given an expression e and its type environment E, if R(E, e) = ⟨θ, t, c, κ⟩, then, for any effect model μ of κ, one has:

μθE ⊢ e : μt, μc

Proof By induction on the number of reduction steps of expressions.

• Case of (var)

The hypotheses are

(1) R(E, x) = ⟨Id, E(x), ∅, ∅⟩

(2) μ ⊧ ∅

From (1), by the definition of R

(3) x ∈ Dom(E), i.e. x ∈ Dom(μE(x))

From (3), by (var) in the static semantics μE ⊢ x : μE(x), ∅

• Case of (abs)

The hypotheses are

(1) R(E, (λn (x) e)) = ⟨θ, θα →^{ζ} t, ∅, κ ∪ {ζ ⊇ {n} ∪ c}⟩

(2) μ ⊧ κ ∪ {ζ ⊇ {n} ∪ c}

From (1), by the definition of R

(3) R(E[x ↦ α], e) = ⟨θ, t, c, κ⟩

From (2), by the definition of effect models

(4) μ ⊧ κ

(5) μ ⊧ {ζ ⊇ {n} ∪ c}, i.e. μζ ⊇ {n} ∪ μc

From (3)(4), by induction

(6) μθ(E[x ↦ α]) ⊢ e : μt, μc From (6)(5), by (does) in the static semantics

(7) μθE[x ↦ μθα]) ⊢ e : μt, μζ

From (7), by (abs) in the static semantics

μθE ⊢ (λn (x) e) : μ(θα →^{ζ} t), ∅

• Case of (rec)

The hypotheses are

(1) R(E, (recn (f x) e)) = ⟨θ′θ, θ′θ(α′ →^{ζ} α), ∅, θ′(κ ∪ {θζ ⊇ {n} ∪ c})⟩

(2) μ ⊧ θ′(κ ∪ {θζ ⊇ {n} ∪ c})

From (1), by the definition of R

(3) R(E[f ↦ α′ →^{ζ} α][x ↦ α′], e) = ⟨θ, t, c, κ⟩

(4) θ′ = U(θα, t) where α′, α, ζ are fresh

From (2), by the definition of effect models

(5) μθ′ ⊧ κ

(6) μθ′ ⊧ θζ ⊇ {n} ∪ c, i.e. μθ′θζ ⊇ {n} ∪ μθ′c

From (3)(5), by induction

(7) μθ′θ(E[f ↦ α′ →^{ζ} α][x ↦ α′]) ⊢ e : μθ′t, μθ′c

From (7)(6), by (does) rule in the static semantics

(8) μθ′θ(E[f ↦ α′ →^{ζ} α][x ↦ α′]) ⊢ e : μθ′t, μθ′θζ

From (4), by the correctness of unification

(9) θ′θα = θ′t i.e μθ′θα = μθ′t

From (8)(9)

(10) μθ′θ(E[f ↦ α′ →^{ζ} α][x ↦ α′]) ⊢ e : μθ′θα, μθ′θζ

From (10), by (rec) in the static semantics

μθ′θE ⊢ (recn (f x) e) : μθ′θ(α′ →^{ζ} α), ∅

• Case of (app)

The hypotheses are

(1) R(E, (e e′)) = ⟨θ′′θ′θ, θ′′α, θ′′(θ′c ∪ c′ ∪ ζ), θ′′(θ′κ ∪ κ′)⟩

(2) μ ⊧ θ′′(θ′κ ∪ κ′)

From (1), by the definition of R

(3) R(E, e) = ⟨θ, t, c, κ⟩

(4) R(θE, e′) = ⟨θ′, t′, c′, κ′⟩

(5) θ′′ = U(θ′t, t′ →^{ζ} α)

for fresh variables α and ζ

From (2), by the definition of effect models

(6) μθ′′θ′ ⊧ κ

(7) μθ′′ ⊧ κ′

From (3)(6) and (4)(7), by inductions

(8) μθ′′θ′θE ⊢ e : μθ′′θ′t, μθ′′θ′c

(9) μθ′′θ′θE ⊢ e′ : μθ′′t′, μθ′′c′

From (5), by the correctness of unification

(10) θ′′θ′t = θ′′(t′ →^{ζ} α), i.e. μθ′′θ′t = μθ′′t′ →^{μθ′′ζ} μθ′′α

From (8)(9)(10), by (app) in the static semantics μθ′′θ′θE ⊢ (e e′) : μθ′′α, μθ′′(θ′c ∪ c′ ∪ ζ) ♣

Proof of Theorem 4.5

Theorem 4.5 [Completeness] If θ_{1}E ⊢ e : t_{1}, c_{1}, then R(E, e) = ⟨θ, t, c, κ⟩ and there exists an effect model μ of κ such that:

θ_{1}E = μθE and t_{1} = μt and c_{1} ⊇ μc

Proof By induction on the number of reduction steps of expressions.

• Case of (var)

The hypothesis is θ_{1}E ⊢ x : θ_{1}E(x), ∅

By (var) in the static semantics x ∈ Dom(E)

By the definition of R R(E, x) = ⟨Id, E(x), ∅, ∅⟩

Taking μ = θ_{1}, such that μ ⊧ ∅ θ_{1}E = μE θ_{1}E(x) = μE(x)

• Case of (abs)

The hypothesis is

θ_{1}E ⊢ (λn (x) e) : t′_{1} →^{{n}∪c_{1}} t_{1}, ∅

By (abs) in the static semantics

(1) θ_{1}E[x ↦ t′_{1}] ⊢ e : t_{1}, c_{1}

Suppose α new, we define a substitution θ′_{1}, such that :

θ′_{1}ϑ = \{ \begin{matrix}t′_{1} & ϑ = α \\ θ_{1}ϑ & otherwise \end{matrix}

By the definition of θ′_{1}, (1) is equivalent to

(2) θ′_{1}(E[x ↦ α]) ⊢ e : t_{1}, c_{1}

From (2), by induction

(3) R(E[x ↦ α], e) = ⟨θ, t, c, κ⟩ ∃μ, μ ⊧ κ, such that

(4) θ′_{1}(E[x ↦ α]) = μθ(E[x ↦ α])

(5) t_{1} = μt

(6) c_{1} ⊇ μc

From (3), by the definition of R

R(E, (λn (x) e)) = ⟨θ, θα →^{ζ} t, ∅, κ ∪ {ζ ⊇ {n} ∪ c}⟩

where ζ is fresh

We define a substitution μ′ on fv(θE, θα, t, c, κ) and ζ.

μ′ϑ = \{ \begin{matrix}μ(ϑ) & ϑ ∈ fv(θE, θα, t, c, κ) \\ \{n\} ∪ c_{1} & ϑ = ζ \end{matrix}

By the definition of μ′

(7) μ′ζ = {n} ∪ c_{1}

(8) μ′({n} ∪ c) = {n} ∪ μc

(9) μ′κ = μκ

From (6)(7)(8), by the definition of effect models

(10) μ′ ⊧ {ζ ⊇ {n} ∪ c}

From (9), since μ ⊧ κ

(11) μ′ ⊧ κ From (10)(11), by the definition of effect models μ′ ⊧ κ ∪ {ζ ⊇ {n} ∪ c}

From (4), by the definition of θ′_{1} and μ′ θ_{1}E = μθE = μ′θE

(12) t′_{1} = μθα = μ′θα

From (5), by the definition of μ′

(13) t_{1} = μ′t

From (7)(12)(13)

t′_{1} →^{{n}∪c_{1}} t_{1} = μ′(θα →^{ζ} t)

• Case of (rec)

The hypothesis is

θ_{1}E ⊢ (recn (f x) e) : t′_{1} →^{{n}∪c_{1}} t_{1}, ∅

By (rec) in the static semantics

(1) θ_{1}E[f ↦ t′_{1} →^{{n}∪c_{1}} t_{1}][x ↦ t′_{1}] ⊢ e : t_{1}, c_{1}

Suppose α′, α, ζ new, we define a substitution θ′_{1}, such that :

θ′_{1}ϑ = \{ \begin{matrix}t′_{1} & ϑ = α′ \\ t_{1} & ϑ = α \\ \{n\} ∪ c_{1} & ϑ = ζ \\ θ_{1}ϑ & otherwise \end{matrix}

By the definition of θ′_{1}, (1) is equivalent to

(2) θ′_{1}(E[f ↦ α′ →^{ζ} α][x ↦ α′]) ⊢ e : t_{1}, c_{1}

From (2), by induction

(3) R(E[f ↦ α′ →^{ζ} α][x ↦ α′], e) = ⟨θ, t, c, κ⟩

∃μ, μ ⊧ κ, such that

(4) θ′_{1}(E[f ↦ α′ →^{ζ} α][x ↦ α′]) = μθ(E[f ↦ α′ →^{ζ} α][x ↦ α′])

(5) t_{1} = μt

(6) c_{1} ⊇ μc

From (4), By the definition of θ′_{1}

(7) θ_{1}E = μθE

(8) t′_{1} →^{{n}∪c_{1}} t_{1} = μθ(α′ →^{ζ} α)

(9) t_{1} = μθα (10) {n} ∪ c_{1} = μθζ

From (5)(9)

(11) μt = μθα

From (11), by the correctness of unification

(12) ∃θ′, θ′ = U (t, θα) and ∃μ′, such that:

(13) μ = μ′θ′

From (3)(12), by the definition of R

R(E, (recn (n, x) e)) = ⟨θ′θ, θ′θ(α′ →^{{n}∪c} α), ∅, θ′(κ ∪ {θζ ⊇ {n} ∪ c})⟩

From (13), since μ ⊧ κ

(14) μ′ ⊧ θ′κ

From (6)(10)

(15) μθζ ⊇ {n} ∪ μc

From (15)(13), by the definition of effect models

(16) μ′ ⊧ {θ′θζ ⊇ {n} ∪ θ′c}

From (14)(16), by the definition of the effect models μ′ ⊧ θ′(κ ∪ {θζ ⊇ {n} ∪ c})

From (7)(13) θ_{1}E = μθE = μ′θ′θE

From (8)(13)

t′_{1} →^{{n}∪c_{1}} t_{1} = μ′θ′θ(α′ →^{ζ} α)

• Case of (app)

The hypothesis is θ_{1}E ⊢ (e e′) : t_{1}, c_{1} ∪ c′_{1} ∪ c′′_{1}

By (app) in the static semantics

(1) θ_{1}E ⊢ e : t′_{1} →^{c′′_{1}} t_{1}, c_{1}

(2) θ_{1}E ⊢ e′ : t′_{1}, c′_{1}

From (1), by induction

(3) R(E, e) = ⟨θ, t, c, κ⟩ ∃μ, μ ⊧ κ, such that:

(4) θ_{1}E = μθE

(5) t′_{1} →^{c′′_{1}} t_{1} = μt

(6) c_{1} ⊇ μc

From (4), (2) is equivalent with:

(7) μ(θE) ⊢ e′ : t′_{1}, c′_{1}

From (7), by induction

(8) R(θE, e′) = ⟨θ′, t′, c′, κ′⟩ ∃μ′, μ′ ⊧ κ′, such that:

(9) μθE = μ′θ′θE

(10) t′_{1} = μ′t′

(11) c′_{1} ⊇ μ′c′

Let α, ζ be fresh. We define a substitution θ_{0} on fv(θE, t, c, κ), fv(θ′θE, t′, c′, κ′), α and ζ

θ_{0}ϑ = \{ \begin{matrix}μϑ & ϑ ∈ fv(θE, t, c, κ) \\ μ′ϑ & ϑ ∈ fv(θ′θE, t′, c′, κ′) \\ t_{1} & ϑ = α \\ c′′_{1} & ϑ = ζ \end{matrix}

Note that ∀ϑ, if ϑ ∈ fv(θE, t, c, κ) and ϑ ∈ fv(θ′θE, t′, c′, κ′) then by the definition of R, ϑ ∈ fv(θE) and ϑ ∈ fv(θ′θE), which means θ′ϑ = ϑ From (9), we know μϑ = μ′ϑ, thus θ_{0} is well defined.

From (10), by the definition of θ_{0},

(12) θ_{0}(t′ →^{ζ} α) = μ′t′ →^{c′′_{1}} t_{1} = t′_{1} →^{c′′_{1}} t_{1}

By the definition of R, ∀ϑ ∈ fv(t, c, κ) v is either in fv(θE) or is a fresh variable introduced by R(E, e).

– case ϑ ∈ fv(θE) By the definition of θ_{0}

(13) θ_{0}(θ′θE) = μ′(θ′θE)

From (9)(13)

(14) θ_{0}θ′(θE) = μ(θE), i. e θ_{0}θ′ϑ = μϑ

– case ϑ is fresh Since ϑ ∈ fv(t, c, κ), by the definition of θ_{0} (15) θ_{0}ϑ = μϑ From (15), since θ′ϑ = ϑ (16) θ_{0}θ′ϑ = θ_{0}ϑ = μϑ

From (14)(16)

(17) ∀ϑ ∈ fv(t, c, κ), θ_{0}θ′ = μ

From (5)(17)

(18) t′_{1} →^{c′′_{1}} t_{1} = θ_{0}θ′t

From (12)(18)

(19) θ_{0}(θ′t) = θ_{0}(t′ →^{ζ} α)

From (19), by the correctness of unification, ∃θ′′ such that (20) θ′′ = U(θ′t, t′ →^{ζ} α) and ∃μ′′ such that

(21) θ_{0} = μ′′θ′′

From (3)(8)(20), by the definition of R R(E, (e e′)) = ⟨θ′′θ′θ, θ′′α, θ′′(θ′c ∪ c′ ∪ ζ), θ′′(θ′κ ∪ κ′)⟩

From (17), since μ ⊧ κ

(22) θ_{0}θ′ ⊧ κ

Since μ′ ⊧ κ′, by the definition of θ_{0}

(23) θ_{0} ⊧ κ′

From (22)(23), by the definition of effect models

(24) θ_{0} ⊧ θ′κ ∪ κ′

From (24)(21), by the definition of effect models μ′′ ⊧ θ′′(θ′κ ∪ κ′)

From (4)(9)(21), by the definition of θ_{0}

(25) θ_{1}E = μ′(θ′θE) = θ_{0}(θ′θE) = μ′′θ′′θ′θE

From (21), since θ_{0}α = t_{1} t_{1} = μ′′θ′′α

From (6)(17)(21)

(26) c_{1} ⊇ μc = θ_{0}θ′c = μ′′θ′′θ′c From (11)(21), by the definition of θ_{0}

(27) c′_{1} ⊇ μ′c′ = θ_{0}c′ = μ′′θ′′c′

From (21), by the definition of θ_{0}

(28) c′′_{1} = θ_{0}ζ = μ′′θ′′ζ

From (26)(27)(28) c_{1} ∪ c′_{1} ∪ c′′_{1} ⊇ μ′′θ′′(θ′c ∪ c′ ∪ ζ) ♣ 96 BIBLIOGRAPHY

Proof of Lemma 5.2

Lemma 5.2 [Formal Effect Constraints] If S(E, e) = ⟨t, c, κ⟩, then κ is of form:

{ζ_{i} ⊇ c_{i} | i = 1..s}

Proof By induction of the structure of expressions.

• Case of x The hypothesis is S(E, x) = ⟨t, ∅, Eff (t′ ≤ t)⟩

By the definition of S

(1) t′ = E(x)

(2) t = New(Erase(t′))

From (1), by Lemma 5.1

(3) t′ includes only fresh effect variables

From (2)(3), by the definition of Eff Eff (t′ ≤ t) verifies the lemma.

• Case of (λn (x) e) The hypothesis is

S(E, (λn (x : τ) e)) = ⟨t′ →^{ζ} t, ∅, κ ∪ {ζ ⊇ {n} ∪ c}⟩

By the definition of S

(1) ζ new

(2) ⟨t, c, κ⟩ = S(E[x ↦ t′], e)

From (2), by induction

(3) κ verifies the lemma

From (1)(3) κ ∪ {ζ ⊇ {n} ∪ c} verifies the lemma • Case of (recn (f x) e)

The hypothesis is

S(E, (recn (f : τ′ → τ x : τ′) e)) = ⟨t′ →^{ζ} t, ∅, κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c}⟩

By the definition of S

(1) t′ →^{ζ} t = New(τ′ → τ)

(2) ⟨t′′, c, κ⟩ = S(E[f ↦ t′ →^{ζ} t][x ↦ t′], e)

From (1), by the definition of New

(3) t = New(τ)

(4) ζ new

From (2), by Lemma 5.1

(5) t′′ includes only fresh effect variables

From (2), by induction

(6) κ verifies the lemma

From (3)(5), by the definition of Eff

(7) Eff (t′′ ≤ t) verifies the lemma

From (6)(7)(4) κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c} verifies the lemma

• Case of (e e′)

The hypothesis is S(E, (e e′)) = ⟨t, c ∪ c′ ∪ ζ, κ ∪ κ′ ∪ Eff (t′ ≤ t′′)⟩

By the definition of S

(1) ⟨t′′ →^{c′′} t, c, κ⟩ = S(E, e)

(2) ⟨t′, c′, κ′⟩ = S(E, e′)

From (1)(2), by Lemma 5.1

(3) t′′ →^{c′′} t includes only fresh effect variables

(4) t′ includes only fresh effect variables

From (3)

(5) t′′ includes only fresh effect variables

From (1)(2), by induction

(6) κ and κ′ verify the lemma From (6)(4)(5), by the definition of Eff κ ∪ κ′ ∪ Eff (t′ ≤ t′′) verifies the lemma ♣

Proof of Theorem 5.1

Theorem 5.1 [Soundness] Given an expression e and its type environment E, if S(E, e) = ⟨t, c, κ⟩, then for any effect model μ of κ, one has :

μE ⊢ e : μt, μc

Proof By induction on the structure of expressions

• Case of (var)

The hypotheses are

(1) S(E, x) = ⟨t, ∅, Eff (t′ ≤ t)⟩

(2) μ ⊧ {t′ ≤ t}

From (1), by the definition of S

(3) t′ = E(x), i.e. μE(x) = μt′

From (3), by (var) rule in the static semantics

(4) μE ⊢ x : μt′, ∅

From (2), by Lemma 5.3

(5) μt′ ≤ μt

From (4)(5), by (sub) rule in the static semantics μE ⊢ x : μt, ∅

• Case of (abs)

The hypotheses are

(1) S(E, (λn (x : τ) e)) = ⟨t′ →^{ζ} t, ∅, κ ∪ {ζ ⊇ {n} ∪ c}⟩

(2) μ ⊧ κ ∪ {ζ ⊇ {n} ∪ c} where t′ = New(τ) and ζ new

From (1), by the definition of S

(3) ⟨t, c, κ⟩ = S(E[x ↦ t′], e)

From (2), by the definition of effect models

(4) μ ⊧ κ

(5) μ ⊧ {ζ ⊇ {n} ∪ c} i.e. μζ ⊇ μ({n} ∪ c)

100 BIBLIOGRAPHY From (3)(4), by induction

(6) μ(E[x ↦ t′]) ⊢ e : μt, μc From (6), by (abs) in the static semantics

(7) μE ⊢ (λn (x) e) : μ(t′ →^{{n}∪c} t), ∅

From (5), by the definition of subtype relation

(8) μ(t′ →^{{n}∪c} t) ≤ μ(t′ →^{ζ} t)

From (7)(8), by (sub) rule in the static semantics

μE ⊢ (λn (x) e) : μ(t′ →^{ζ} t), ∅

• Case of (rec) The hypotheses are

(1) S(E, (recn (f : τ′ → τ x : τ′) e)) = ⟨t′ →^{ζ} t, ∅, κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c}⟩

(2) μ ⊧ κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c} where t′ →^{ζ} t = New(τ′ → τ) From (1), by the definition of S

(3) ⟨t′′, c, κ⟩ = S(E[f ↦ t′ →^{ζ} t][x ↦ t′])

From (2), by the definition of effect models

(4) μ ⊧ κ

(5) μ ⊧ Eff (t′′ ≤ t)

(6) μ ⊧ {ζ ⊇ {n} ∪ c}, i.e. μζ ⊇ {n} ∪ μc From (3)(4), by induction

(7) μ(E[f ↦ t′ →^{ζ} t][x ↦ t′]) ⊢ e : μt′′, μc

From (5), by Lemma 5.3

(8) μt′′ ≤ μt From (7)(8), by (sub) in the static semantics

(9) μ(E[f ↦ t′ →^{ζ} t][x ↦ t′]) ⊢ e : μt, μc

From (9), by (abs) in the static semantics

(10) (μE)[f ↦ μ(t′ →^{ζ} t)] ⊢ (λn (x) e) : μ(t′ →^{{n}∪c} t), ∅

From (6), by the definition of subtype relation

(11) μ(t′ →^{{n}∪c} t) ≤ μ(t′ →^{ζ} t)

From (10)(11), by (sub) rule in the static semantics

(12) (μE)[f ↦ μ(t′ →^{ζ} t)] ⊢ (λn (x) e) : μ(t′ →^{ζ} t), ∅

From (12), by (rec) rule in the static semantics

μE ⊢ (rec n (f x) e) : μ(t′ →^{ζ} t), ∅

• Case of (app)

The hypotheses are

(1) S(E, (e e′)) = ⟨t, c ∪ c′ ∪ c′′, κ ∪ κ′ ∪ Eff (t′ ≤ t′′)⟩

(2) μ ⊧ κ ∪ κ′ ∪ Eff (t′ ≤ t′′)

From (1), by the definition of S

(3) S(E, e) = ⟨t′′ →^{c′′} t, c, κ⟩

(4) S(E, e′) = ⟨t′, c′, κ′⟩

From (2), by the definition of effect models

(5) μ ⊧ κ

(6) μ ⊧ κ′

(7) μ ⊧ Eff (t′ ≤ t′′)

From (3)(5) and (4)(6), by induction

(8) μE ⊢ e : μ(t′′ →^{c′′} t), μc

(9) μE ⊢ e′ : μt′, μc′

From (7), by Lemma 5.3

(10) μt′ ≤ μt′′

From (9)(10), by the (sub) rule in the static semantics

(11) μE ⊢ e′ : μt′′, μc′

From (8)(11), by (app) in the static semantics μE ⊢ (e e′) : μt, μ(c ∪ c′ ∪ c′′) ♣

Proof of Theorem 5.2

Theorem 5.2 [Completeness] If θ_{1}E ⊢ e : t_{1}, c_{1}, then S(E, e) = ⟨t, c, κ⟩ and there exists a effect model μ of κ, such that:

θ_{1}E = μE and μt ≤ t_{1} and c_{1} ⊇ μc

Proof By induction on the structure of expressions • Case of (var)

The hypothesis is θ_{1}E ⊢ x : t_{1}, ∅

By (var) and (sub) rules in the static semantics

(1) t′_{1} = E(x)

(2) θ_{1}t′_{1} ≤ t_{1}

From (1), by the definition of S S(E, x) = ⟨t, ∅, Eff (t′_{1} ≤ t)⟩ where t = New(Erase(t′_{1}))

Since t includes only fresh effect variables, taking θ, such that:

(3) θt = t_{1}

We define the effect model μ, such that :

μϑ = \{ \begin{matrix}θϑ & ϑ ∈ fv(t) \\ θ_{1}ϑ & otherwise \end{matrix}

Note that since t includes only fresh effect variables, μ is well defined.

From (2)(3), by the definition of μ

(4) μt′_{1} = θ_{1}t′_{1} ≤ t_{1}

(5) μt = θt = t_{1}

From (4)(5), by Lemma 5.3 μ ⊧ Eff (t′_{1} ≤ t)

By the definition of μ θ_{1}E = μE

From (5) μt ≤ t_{1}

• Case of (abs)

The hypothesis is

θ_{1}E ⊢ (λn (x) e) : t′_{2} →^{c_{2}} t_{2}, ∅

By (abs) and (sub) rule in the static semantics

(1) θ_{1}E ⊢ (λn (x) e) : t′_{1} →^{{n}∪c_{1}} t_{1}, ∅

(2) t′_{1} →^{{n}∪c_{1}} t_{1} ≤ t′_{2} →^{c_{2}} t_{2}

From (1), by (abs) rule in the static semantics

(3) (θ_{1}E)[x ↦ t′_{1}] ⊢ e : t_{1}, c_{1}

If x is of the principal type τ, let t′ = New(τ) then there exists a substitution θ, such that:

(4) t′_{1} = θt′

we define a substitution θ′_{1}, such that :

θ′_{1}ϑ = \{ \begin{matrix}θϑ & ϑ ∈ fv(t′) \\ θ_{1}ϑ & otherwise \end{matrix}

Note that since t′ includes only fresh effect variables, θ′_{1} is well defined.

From (4), by the definition of θ′_{1}, (3) is equivalent with :

(5) θ′_{1}(E[x ↦ t′]) ⊢ e : t_{1}, c_{1}

From (5), by induction

(6) S(E[x ↦ t′], e) = ⟨t, c, κ⟩ ∃μ, such that :

(7) μ ⊧ κ

(8) θ′_{1}(E[x ↦ t′]) = μ(E[x ↦ t′])

(9) μt ≤ t_{1}

(10) c_{1} ⊇ μc

From (8)(4), by the definition of θ′_{1}

(11) θ_{1}E = μE

(12) t′_{1} = μt′

From (6), since t′ = New(τ), by the definition of S

(13) S(E, λn (x : τ) e) = ⟨t′ →^{ζ} t, ∅, κ ∪ {ζ ⊇ {n} ∪ c}⟩

where ζ new

We define a effect substitution μ′ on fv(E, t′, t, c, κ) and ζ, such that :

μ′ϑ = \{ \begin{matrix}μϑ & fv(E, t′, t, c, κ) \\ c_{2} & ϑ = ζ \end{matrix}

Note that since ζ is fresh, μ′ is well defined.

From (7), by the definition of μ′

(14) μ′ ⊧ κ By the definition of μ′

(15) μ′ζ = c_{2}

(16) μ′({n} ∪ c) = {n} ∪ μc

From (10)(16), by the definition of μ′

(17) {n} ∪ c_{1} ⊇ μ′({n} ∪ c)

From (2), by the definition of subtype relation

(18) t_{1} ≤ t_{2}

(19) t′_{2} ≤ t′_{1}

(20) c_{2} ⊇ {n} ∪ c_{1}

From (20)(15)(17), by the definition of effect models (21) μ′ ⊧ {ζ ⊇ {n} ∪ c}

From (14)(21), by the definition of effect models μ′ ⊧ κ ∪ {ζ ⊇ {n} ∪ c}

From (11)(12), by the definition of μ′ θ_{1}E = μ′E

(22) t′_{1} = μ′t′

From (9), by the definition of μ′

(23) μ′t ≤ t_{1}

From (22)(23)(15), by the definition of subtype relation

(24) μ′(t′ →^{ζ} t) ≤ t′_{1} →^{c_{2}} t_{1}

From (18)(19), by the definition of subtype relation

(25) t′_{1} →^{c_{2}} t_{1} ≤ t′_{2} →^{c_{2}} t_{2}

From (24)(25)

μ′(t′ →^{ζ} t) ≤ t′_{2} →^{c_{2}} t_{2}

• Case of (rec)

The hypothesis is

θ_{1}E ⊢ (recn (f x) e) : t′_{2} →^{c_{2}} t_{2}, ∅

By (rec) and (sub) rule in the static semantics

(1) θ_{1}E ⊢ (recn (f x) e) : t′_{1} →^{{n}∪c_{1}} t_{1}, ∅

(2) t′_{1} →^{{n}∪c_{1}} t_{1} ≤ t′_{2} →^{c_{2}} t_{2}

From (1), by (rec) rule in the static semantics

(3) (θ_{1}E)[f ↦ t′_{1} →^{{n}∪c_{1}} t_{1}][x ↦ t′_{1}] ⊢ e : t_{1}, c_{1}

If f and x is of the principal type τ′ → τ, τ′ respectively, let (t′ →^{ζ} t) = New(τ′ → τ), then there exists a substitution θ, such that:

(4) t′_{1} →^{{n}∪c_{1}} t_{1} = θ(t′ →^{ζ} t)

We define a substitution of effect variables θ′_{1}, such that :

θ′_{1}ϑ = \{ \begin{matrix}θϑ & ϑ ∈ fv(t′ →^{ζ} t) \\ θ_{1}ϑ & otherwise \end{matrix}

Note that since t′ →^{ζ} t includes only fresh effect variables, θ′_{1} is well defined.

From (4), by the definition of θ′_{1}, (3) is equivalent with :

(5) θ′_{1}(E[f ↦ t′ →^{ζ} t][x ↦ t′]) ⊢ e : t_{1}, c_{1}

From (5), by induction

(6) S(E[f ↦ t′ →^{ζ} t][x ↦ t′], e) = ⟨t′′, c, κ⟩

∃μ, such that :

(7) μ ⊧ κ

(8) θ′_{1}(E[f ↦ t′ →^{ζ} t][x ↦ t′]) = μ(E[f ↦ t′ →^{ζ} t][x ↦ t′])

(9) μt′′ ≤ t_{1}

(10) c_{1} ⊇ μc

From (6), since t′ →^{ζ} t = New(τ′ → τ), by the definition of S

(11) S(E, (recn (f : τ′ → τ x : τ′) e)) = ⟨t′ →^{ζ} t, ∅, κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c}⟩

From (8)(4), by the definition of θ′_{1} θ_{1}E = μE

(12) t′_{1} →^{{n}∪c_{1}} t_{1} = μ(t′ →^{ζ} t)

(13) t_{1} = μt

(14) {n} ∪ c_{1} = μζ

From (9)(13), by Lemma 5.3

(15) μ ⊧ Eff (t′′ ≤ t)

From (14)(10), by the definition of effect models

(16) μ ⊧ {ζ ⊇ {n} ∪ c} From (7)(15)(16), by the definition of effect models μ ⊧ κ ∪ Eff (t′′ ≤ t) ∪ {ζ ⊇ {n} ∪ c}

From (12)(2)

μ(t′ →^{ζ} t) ≤ t′_{2} →^{c_{2}} t_{2}

• Case of (app)

The hypotheses is θ_{1}E ⊢ (e e′) : t_{2}, c_{1} ∪ c′_{1} ∪ c′′_{1}

By (app) and (sub) rules in the static semantics

(1) θ_{1}E ⊢ (e e′) : t_{1}, c_{1} ∪ c′_{1} ∪ c′′_{1}

(2) t_{1} ≤ t_{2}

From (1), by (app) in the static semantics

(3) θ_{1}E ⊢ e : t′_{1} →^{c′′_{1}} t_{1}, c_{1}

(4) θ_{1}E ⊢ e′ : t′_{1}, c′_{1}

From (3), by induction

(5) S(E, e) = ⟨t′′ →^{c′′} t, c, κ⟩

∃μ, such that :

(6) μ ⊧ κ

(7) θ_{1}E = μE

(8) μ(t′′ →^{c′′} t) ≤ t′_{1} →^{c′′_{1}} t_{1}

(9) c_{1} ⊇ μc

From (4), by induction

(10) S(E, e′) = ⟨t′, c′, κ⟩ ∃μ′, such that :

(11) μ′ ⊧ κ′

(12) θ_{1}E = μ′E

(13) μ′t′ ≤ t′_{1}

(14) c′_{1} ⊇ μ′c′

From (5)(10), by the definition of S S(E, (e e′)) = ⟨t, c ∪ c′ ∪ c′′, κ ∪ κ′ ∪ Eff (t′ ≤ t′′)⟩

We define a substitution μ′′ on fv(E, t′′ →^{c′′} t, c, κ), and fv(E, t′, c′, κ′)

μ′′ϑ = \{ \begin{matrix}μϑ & ϑ ∈ fv(E, t′′ →^{c′′} t, c, κ) \\ μ′ϑ & ϑ ∈ fv(E, t′, c′, κ′) \end{matrix}

Note that ∀ϑ, if ϑ ∈ fv(E, t′, c′, κ′) and ϑ ∈ fv(E, t, c, κ) then by the definition of S, ϑ ∈ fv(E) By (7)(12), μϑ = μ′ϑ, thus μ′′ is well defined.

From (6)(11), by the definition of μ′′

(16) μ′′ ⊧ κ

(17) μ′′ ⊧ κ′

From (8), by the definition of μ′′

(18) μ′′(t′′ →^{c′′} t) = μ(t′′ →^{c′′} t) ≤ t′_{1} →^{c′′_{1}} t_{1}

From (18), by the definition of subtype relation

(19) μ′′t ≤ t_{1}

(20) t′_{1} ≤ μ′′t′′

(21) c′′_{1} ⊇ μ′′c′′

From (13), by the definition of μ′′

(22) μ′′t′ = μ′t′ ≤ t′_{1}

From (20)(22), by Lemma 5.3

(23) μ′′ ⊧ Eff (t′ ≤ t′′)

From (16)(17)(23), by the definition of effect models μ′′ ⊧ κ ∪ κ′ ∪ Eff (t′ ≤ t′′)

From (19)(2) μ′′t ≤ t_{2}

From (9)(14)(21), by the definition of μ′′ c_{1} ∪ c′_{1} ∪ c′′_{1} ⊇ μ′′(c ∪ c′ ∪ c′′) ♣ 108 BIBLIOGRAPHY

Proof of Theorem 6.1

Theorem 6.1 [Well-Formedness of Abstract Semantics] If β̂, Ê ⊢ e → v̂, ĉ and WF(β̂, Ê), then

• (v̂, Ê) is well-formed.

• All (β̂′, Ê′) used in the → derivation tree of e are well-formed.

Proof By induction on the number of reduction steps of expressions.

• The hypotheses are (1) β̂, Ê ⊢ (a a′)l → ∪_{i=1}^{r}v̂_{i}, ∪_{i=1}^{r}(ĉ_{i} ∪ {(l, β̂) ⇝ {n_{i}}})

(2) WF(β̂, Ê)

From hypothesis (1), by (app) in abstract semantics

(3) β̂, Ê ⊢ a → {(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i}) | i = 1 … r}

(4) β̂, Ê ⊢ a′ → v̂′

(5) β̂′_{i}[x_{i} ↦ b̂′], Ê ⊢ e′_{i} → v̂_{i}, ĉ_{i}

(6) Ê(x_{i}, b̂′) = v̂′ where b̂′ = l and i = 1 … r

From (2)(3)(4), by Lemma 6.1

(7) WF({(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i}) | i = 1 … r}, Ê)

(8) WF(v̂′, Ê)

From (7), by Definition 6.1

(9) WF(β̂′_{i}, Ê)

From (6)(8)(9), by Definition 6.1

(10) WF(β̂′_{i}[x_{i} ↦ b̂′], Ê)

From (10), by induction All (β̂′, Ê′) used in the → derivation tree of e are well-formed From (5)(10), by induction

(11) (v̂_{i}, Ê) is well-formed

From (11), by Definition 6.1 (∪_{i=1}^{r}v̂_{i}, Ê) is well-formed ♣

Proof of Theorem 6.2

Theorem 6.2 [Consistency of Abstract Semantics]

\begin{matrix}b, β, E ⊢ e → v, c \\ β̂, Ê ⊢ e → v̂, ĉ \\ (β, E) ≤ (β̂, Ê) \end{matrix} \} ⇒ \{ \begin{matrix}(v, E) ≤ (v̂, Ê) \\ c ⊑ ĉ \end{matrix}

Proof By induction on the number of reduction steps of expressions.

• The hypotheses are (1) (β, E) ≤ (β̂, Ê)

(2) b, β, E ⊢ (a a′)l → v, c ∪ {(l, β) ⇝ {n}}

(3) β̂, Ê ⊢ (a a′)l → ∪_{i=1}^{r}v̂_{i}, ∪_{i=1}^{r}(ĉ_{i} ∪ {(l, β̂) ⇝ {n_{i}}})

From hypothesis (2), by (app) in the dynamic semantics

(4) β, E ⊢ a → (λn(x) e, β′)

(5) β, E ⊢ a′ → v′

(6) b′, β′[x ↦ b′], E ⊢ e → v, c

(7) E(x, b′) = v′ where b′ = b.l

From hypothesis (3), by (app) in the abstract semantics

(8) β̂, Ê ⊢ a → {(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i})}

(9) β̂, Ê ⊢ a′ → v̂′

(10) β̂′_{i}[x_{i} ↦ b̂′], Ê ⊢ e_{i} → v̂_{i}, ĉ_{i}

(11) Ê(x_{i}, b̂′) = v̂′ where b̂′ = l and i = 1 … r

From (1)(4)(8) and (1)(5)(9), by Lemma 6.2

(12) ((λn(x) e, β′), E) ≤ ({(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i}) | i = 1 … r}, Ê)

(13) (v′, E) ≤ (v̂′, Ê)

From (12), by Definition 6.2, ∃j (1 ≤ j ≤ r) s.t.

(14) λn(x) e = λ_{n_{j}}(x_{j}) e_{j}

(15) (β′, E) ≤ (β̂′_{j}, Ê)

From (15)(7)(11)(13), by Definition 6.2

(16) (β′[x ↦ b′], E) ≤ (β̂′_{j}[x_{j} ↦ b̂′], Ê)

From (16)(6)(10), by induction

(17) (v, E) ≤ (v̂_{j}, Ê) (17)′ c ⊑ ĉ_{j}

From (17), by Definition 6.2 (v, E) ≤ (∪_{i=1}^{r}v̂_{i}, Ê)

From (14)(17)′, by Definition 6.3 c ∪ {(l, β) ⇝ {n}} ⊑ ∪_{i=1}^{r}(ĉ_{i} ∪ {(l, β̂) ⇝ {n_{i}}}) ♣

Proof of Theorem 6.3

Theorem 6.3 [Types of Abstract Semantics]

\begin{matrix}E ⊢ e : t, c̄ \\ β̂, Ê ⊢ e → v̂, ĉ \\ (β̂, Ê) : E \end{matrix} \} ⇒ \{ \begin{matrix}(v̂, Ê) : t \\ ĉ ⊑ c̄ \end{matrix}

Proof By induction on the number of reduction steps of expressions.

• The hypotheses are (1) (β̂, Ê) : E

(2) E ⊢ (a a′)l : t, ∪_{(n,c̄)∈d}(c̄ ∪ {(l, []) ⇝ {n}})

(3) β̂, Ê ⊢ (a a′)l → ∪_{i=1}^{r}v̂_{i}, ∪_{i=1}^{r}(ĉ_{i} ∪ {(l, β̂) ⇝ {n_{i}}})

From (2), by (app) in the type semantics

(4) E ⊢ a : t′ →^{d} t

(5) E ⊢ a′ : t′

From (3), by (app) in the abstract semantics

(6) β̂, Ê ⊢ a → {(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i}) | i = 1 … r}

(7) β̂, Ê ⊢ a′ → v̂′

(8) β̂′_{i}[x_{i} ↦ b̂′], Ê ⊢ e_{i} → v̂_{i}, ĉ_{i}

(9) Ê(x_{i}, b̂′) = v̂′ where b̂′ = l and i = 1 … r

From (1)(4)(6) and (1)(5)(7), by Lemma 6.3

(10) ({(λ_{n_{i}}(x_{i}) e_{i}, β̂′_{i}) | i = 1 … r}, Ê) : t′ →^{d} t

(11) (v̂′, Ê) : t′ From (10), by Definition 6.4, ∀i (i = 1 … r), ∃E′_{i} s.t.

(12) (β̂′_{i}, Ê) : E′_{i}

(13) E′_{i} ⊢ (λ_{n_{i}} (x_{i}) e_{i}) : t′ →^{d} t

From (13), by (abs) in the type semantics

(14) E′_{ix_{i}}[x_{i} ↦ t′] ⊢ e_{i} : t, c̄_{i}

(15) (n_{i}, c̄_{i}) ∈ d

From (12)(11)(9), by Definition 6.4

(16) (β̂′_{i}[x_{i} ↦ b̂′], Ê) : E′_{ix_{i}}[x_{i} ↦ t′]

From (16)(8)(14), by induction

(17) (v̂_{i}, Ê) : t (17)′ ĉ_{i} ⊑ c̄_{i}

From (17), by Definition 6.4 (∪_{i=1}^{r}v̂_{i}, Ê) : t

From (15)(17)′, by Definition 6.3 ∪_{i=1}^{r}(ĉ_{i} ∪ {(l, β̂) ⇝ {n_{i}}}) ⊑ ∪_{(n,c̄)∈d}(c̄ ∪ {(l, []) ⇝ {n}}) ♣

Proof of Lemma 6.4

Lemma 6.4 [Well-Formedness of A(t)] A(t) is well-formed. Proof By induction on the structure of types

• Case int

By the definition of A A(int) = (∅, [])

By Definition 6.1 A(int) is well-formed

• Case (t′ ∗ t_{0}) →^{d} t_{1} where t_{0} = t →^{d′} t_{1}

By the definition of A

A((t′ ∗ t_{0}) →^{d} t_{1}) = (v̂′, Ê′)

where

(1) v̂′ = {(λ_{n_{i}}(x k_{i}) e_{i}, [x_{i} ↦ l_{i}]) | i = 1 … q}

(2) Ê′ = Ê[(x_{i}, l_{i}) ↦ v̂]

(3) (v̂, Ê) = A(t)

From (3), by induction

(4) A(t) is well-formed, i.e. (v̂,Ê) is well-formed

From (2)(4), since x_{i} is fresh , by Definition 6.1

(5) (v̂, Ê′) is well-formed

From (5), by Definition 6.1

(6) ([x_{i} ↦ l_{i}], Ê′) is well-formed

From (6)(1)(2), by Definition 6.1 A((t′ ∗ t_{0}) →^{d} t_{1}) is well-formed ♣

Proof of Lemma 6.5

Lemma 6.5 [Consistency of A(t)] If (v̂, Ê) : t, then (v̂, Ê) ≤ A(t) Proof By induction on the structure of types

• Case int

By the definition of A

(1) A(int) = (∅, [])

Since (v̂, Ê) : t, by Definition 6.4

(2) (∅, Ê) : int

From (1)(2), by Definition 6.5 (∅, Ê) ≤ A(int)

• Case (t′ ∗ t_{0}) →^{d} t_{1}

By the definition of A

(1) A((t′ ∗ t_{0}) →^{d} t_{1}) = (v̂′, Ê′)

where v̂′ = {(λ_{n_{i}}(x k_{i}) e_{i}, [x_{i} ↦ l_{i}]) | i = 1 … q} d = {(n_{i}, c̄_{i}) | i = 1 … q}

Since (v̂, Ê) : t, by Definition 6.4

(2) ∀(n, β̂) ∈ v̂, ∃E, s.t. (β̂, Ê) : E

(3) E ⊢ n : t

From (3), by the (abs) rule in the effect semantics

(4) ∃c̄, s.t. (n, c̄) ∈ d From (1)(2)(4), by Definition 6.5 (v̂, Ê) ≤ A(t)

Proof of Lemma 6.6

Lemma 6.6 [Simulation] For any β̂_{1} and Ê_{1}, if

β̂_{1}[x_{i} ↦ l_{i}][k_{i} ↦ l_{k}], Ê_{1}[(x_{i}, l_{i}) ↦ v̂][(k_{i}, l_{k}) ↦ {Id}] ⊢ S(c̄_{i}, k_{i}, x_{i}, l) → v̂, ĉ_{i}

then D(ĉ_{i}) = c̄_{i} ∪ {(l, []) ⇝ {Id}}. Proof By induction on c̄_{i}

Supposing ∀j ≥ 1 β̂′_{j} = β̂_{j}[x_{i} ↦ l_{i}][k_{i} ↦ l_{k}] Ê′_{j} = Ê_{j}[(x_{i}, l_{i}) ↦ v̂][(k_{i}, l_{k}) ↦ {Id}]

• Case c̄_{i} = []

By the definition of S S([], k_{i}, x_{i}, l) = (k_{i} x_{i})l

By the abstract semantics, since k_{i} is bound to Id β̂′_{1}, Ê′_{1} ⊢ (k_{i} x_{i})l → v̂, {(l, β̂′_{1}) ⇝ {Id}}

By the definition of D D({(l, β̂′_{1}) ⇝ {Id}}) = {(l, []) ⇝ {Id}}

• Case c̄_{i} = c̄′_{i} ∪ {(l′, []) ⇝ {n_{1} … n_{r}}}

By the definition of S

(1) S(c̄_{i}, k_{i}, x_{i}, l) = S′({n_{1} … n_{r}}, c̄′_{i}, l′, k_{i}, x_{i}, l)

By the definition of S′, ∀j = 1 … r

(2) S′({n_{j} … n_{r}}, c̄′_{i}, l′, k_{i}, x_{i}, l) = ( (λ_{n_{j}}(k_{j}) S′({n_{j+1} … n_{r}}, c̄′_{i}, l′, k_{k}, x_{i}, l)) k_{i} )l′ Note that {n_{j+1} … n_{r}} = ∅

By induction on j, we prove that β̂′_{j}, Ê′_{j} ⊢ S′({n_{j} … n_{r}}, c̄′_{i}, l′, k_{i}, x_{i}, l) → v̂, ĉ′ such that D(ĉ′) = c̄′_{i} ∪ {(l, []) ⇝ {Id}} ∪ {(l′, []) ⇝ {n_{j} … n_{r}}} where ĉ′ = ĉ′_{i} ∪ {(l′, β̂′_{j}) ⇝ {n_{j}}} … {(l′, β̂′_{r}) ⇝ {n_{r}}} β̂_{j+1} = β̂_{j}[k_{j} ↦ l′] Ê_{j+1} = Ê_{j}[(k_{j}, l′) ↦ k_{i}] – Case j = r + 1

By the definition of S′, since {n_{r+1} … n_{r}} = ∅

(3) S′(∅, c̄′_{i}, l′, k_{i}, x_{i}, l) = S(c̄′_{i}, k_{i}, x_{i}, l)

From (3), by the induction on c̄_{i} β̂′_{r+1}, Ê′_{r+1} ⊢ S′(∅, c̄′_{i}, l′, k_{i}, x_{i}, l) → v̂, ĉ′_{i} such that D(ĉ′_{i}) = c̄′_{i} ∪ {(l, []) ⇝ {Id}}

– Case j = 1 … r By induction on j

(4) β̂′_{j+1}, Ê′_{j+1} ⊢ S′({n_{j+1} … n_{r}}, c̄′_{i}, l′, k_{i}, x_{i}, l) → v̂, ĉ′ such that

(5) D(ĉ′) = c̄′_{i} ∪ {(l, []) ⇝ {Id}} ∪ {(l′, []) ⇝ {n_{j+1} … n_{r}}} where ĉ′ = ĉ′_{i} ∪ {(l′, β̂′_{j+1}) ⇝ {n_{j+1}}} … {(l′, β̂′_{r}) ⇝ {n_{r}}}

From (2)(4), by the abstract semantics β̂′_{j}, Ê′_{j} ⊢ S′({n_{j} … n_{r}}, c̄′_{i}, l′, k_{i}, x_{i}, l) → v̂, ĉ′ ∪ {(l′, β̂′_{j}) ⇝ {n_{j}}}

From (5), by the definition of D D(ĉ′ ∪ {(l′, β̂′_{j}) ⇝ {n_{j}}}) = c̄′_{i} ∪ {(l, []) ⇝ {Id}} ∪ {(l′, []) ⇝ {n_{j} … n_{r}}}

From (1), using the initial abstract value environments β̂′_{1} and Ê′_{1}, we get : β̂′_{1}, Ê′_{1} ⊢ S(c̄_{i}, k_{i}, x_{i}, l) → v̂, ĉ_{i} such that D(ĉ_{i}) = c̄_{i} ∪ {(l, []) ⇝ {Id}} where ĉ_{i} = ĉ′_{i} ∪ {(l′, β̂′_{1}) ⇝ {n_{1}}} … {(l′, β̂′_{r}) ⇝ {n_{r}}} ♣

Proof of Lemma 6.7

Lemma 6.7 [Well-Formedness of (β̂_{0}, Ê_{0})] (β̂_{0}, Ê_{0}) is well-formed. Proof

• By the definition of (β̂_{0}, Ê_{0}) (1) ∀x ∈ Dom(β̂_{0}), (x, β̂_{0}(x)) ∈ Dom(Ê_{0})

(2) Ê_{0}(x, β̂_{0}(x)) = v̂

(3) Dom(Ê) ⊆ Dom(Ê_{0})

(4) (v̂, Ê) = A(E(x))

From (4), by Lemma 6.4

(5) (v̂, Ê) is well-formed

From (5)(3), by Definition 6.1

(6) (v̂, Ê_{0}) is well-formed From (1)(2)(6), by Definition 6.1 (β̂_{0}, Ê_{0}) is well-formed ♣

Proof of Lemma 6.8

Lemma 6.8 [Consistency of (β̂_{0}, Ê_{0})] If (β̂′_{0}, Ê′_{0}) : E, then (β̂′_{0}, Ê′_{0}) ≤ (β̂_{0}, Ê_{0}) Proof

• By the definition of (β̂_{0}, Ê_{0}) (1) ∀x ∈ Dom(E), x ∈ Dom(β̂_{0})

(2) Ê_{0}(x, β̂_{0}(x)) = v̂

(3) Dom(Ê) ⊆ Dom(Ê_{0})

(4) (v̂, Ê) = A(E(x))

Since (β̂′_{0}, Ê′_{0}) : E, by Definition 6.4

(5) ∀x ∈ Dom(β̂′_{0}), x ∈ Dom(E)

(6) (Ê′_{0}(x, β̂′_{0}(x)), Ê′_{0}) : E(x)

From (6), by Lemma 6.5

(7) (Ê′_{0}(x, β̂′_{0}(x)), Ê′_{0}) ≤ A(E(x))

From (7)(4)

(8) (Ê′_{0}(x, β̂′_{0}(x)), Ê′_{0}) ≤ (v̂, Ê)

From (8)(3), by Definition 6.2

(9) (Ê′_{0}(x, β̂′_{0}(x)), Ê′_{0}) ≤ (v̂, Ê_{0})

From (5)(1)

(10) ∀x ∈ Dom(β̂′_{0}), x ∈ Dom(β̂_{0})

From (10)(9)(2), by Definition 6.2 (β̂′_{0}, Ê′_{0}) ≤ (β̂_{0}, Ê_{0}) ♣