Expansion: the Crucial Mechanism for Type Inference with Intersection Types: Survey and Explanation
---
paper_title: What are principal typings and what are they good for?

paper_content:

We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ML. Its principal typing property provides elegant support for separate compilation, including "smartest recompilation" and incremental type inference. Moreover, it motivates a new rule for typing recursive definitions that can type some interesting examples of polymorphic recursion.
---
paper_title: Type error slicing in implicitly typed higher-order languages

paper_content:

Previous methods have generally identified the location of a type error as a particular program point or the program subtree rooted at that point. We present a new approach that identifies the location of a type error as a set of program points (a slice) all of which are necessary for the type error. We describe algorithms for finding minimal type error slices for implicitly typed higher-order languages like Standard ML.
---
paper_title: What are principal typings and what are they good for?

paper_content:

We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ML. Its principal typing property provides elegant support for separate compilation, including "smartest recompilation" and incremental type inference. Moreover, it motivates a new rule for typing recursive definitions that can type some interesting examples of polymorphic recursion.
---
paper_title: A New Presentation of the Intersection Type Discipline Through Principal Typings of Normal Forms

paper_content:

We introduce an intersection type system which is a restriction of the intersection type discipline. This restriction leads to a principal type property for normal forms in the classical sense, while retaining the expressivity of the classical discipline. We characterize the structure of principal types of normal forms and give an algorithm that reconstructs normal forms from types. Having shown the equivalence between principal types and normal forms, we define an expansion operation on types which allows us to recover all possible types for any normalizable $\lambda$-term. The contribution of this work is a new and simpler presentation of the intersection type discipline through a purely syntactic and completely characterized notion of principal types.
---
paper_title: Strictness, Totality, and Non-Standard Type Inference

paper_content:

In this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. We also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. A main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. This leads to a rather direct presentation which involves relatively little mathematical overhead. Copyright 2002 Elsevier Science B.V.
---
paper_title: Rank 2 intersection types for local definitions and conditional expressions

paper_content:

We propose a rank 2 intersection type system with new typing rules for local definitions (let-expressions and letrec-expressions) and conditional expressions (if-expressions and match-expressions). This is a further step towards the use of intersection types in "real" programming languages.The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 intersection), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to "limit the use" of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might also be useful for other type systems.
---
paper_title: Type reconstruction in Fω

paper_content:

We investigate Girard's calculus F ω as a ‘Curry style’ type assignment system for pure lambda terms. First we show an example of a strongly normalizable term that is untypable in F ω. Then we prove that every partial recursive function is nonuniformly represented in Fω (even if quantification is restricted to constructor variables of level 1). It follows that the type reconstruction problem is undecidable and cannot be recursively separated from normalization.
---
paper_title: A modular, polyvariant and type-based closure analysis

paper_content:

We observe that the principal typing property of a type system is the enabling technology for modularity and separate compilation [10]. We use this technology to formulate a modular and polyvariant closure analysis, based on the rank 2 intersection types annotated with control-flow information.Modularity manifests itself in a syntax-directed, annotated-type inference algorithm that can analyse program fragments containing free variables: a principal typing property is used to formalise it. Polyvariance manifests itself in the separation of different behaviours of the same function at its different uses: this is formalised via the rank 2 intersection types. As the rank 2 intersection type discipline types at least all (core) ML programs, our analysis can be used in the separate compilation of such programs.
---
paper_title: Rank 2 intersection types for modules

paper_content:

We propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for the module language. We first consider a "plain" notion of module, where a module is just a set of mutually recursive top-level definitions, and illustrate the notions of: module intrachecking (each module is typechecked in isolation and its interface, which is the set of typings of the defined identifiers, is inferred); interface interchecking (when linking modules, typechecking is done just by looking at the interfaces); interface specialization (interface intrachecking may require to specialize the typing listed in the interfaces); principal interfaces (the principal typing property for the type system of modules); and separate typechecking (looking at the code of the modules does not provide more type information than looking at their interfaces). Then we illustrate some limitations of the "plain" framework and extend the module language and the type system in order to overcome these limitations. The decidability of the system is shown by providing algorithms for the fundamental operations involved in module intrachecking and interface interchecking.
---
paper_title: Implementing Compositional Analysis Using Intersection Types With Expansion Variables

paper_content:

Abstract A program analysis is compositional when the analysis result for a particular program fragment is obtained solely from the results for its immediate subfragments via some composition operator. This means the subfragments can be analyzed independently in any order. Many commonly used program analysis techniques (in particular, most abstract interpretations and most uses of the Hindley/Milner type system) are not compositional and require the entire text of a program for sound and complete analysis. System ::: I is a recent type system for the pure λ-calculus with intersection types and the new technology of expansion variables. System ::: I supports compositional analysis because it has the principal typings property and an algorithm based on the new technology of β-unification has been developed that finds these principal typings. In addition, for each natural number k, typability in the rank-k restriction of System ::: I is decidable, so a complete and terminating analysis algorithm exists for the rank-k restriction. This paper presents new understanding that has been gained from working with multiple implementations of System ::: I and β-unification-based analysis algorithms. The previous literature on System ::: I presented the type system in a way that helped in proving its more important theoretical properties, but was not as easy to follow as it could be. This paper provides a presentation of many aspects of System ::: I that should be clearer as well as a discussion of important implementation issues.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: Principal Types and Unification for Simple Intersection Type Systems

paper_content:

In this paper we introduce a decidable restriction of the intersection type discipline. The restriction is based on a uniform principle rather than on a notion of rank. For this system we give a type checking algorithm that we prove to be sound and complete. An extended language of types with labelled intersections and intersection schemes is needed to describe the principal type of terms which turns out to be unique module a set of equations between labels. The unification algorithm far labelled types, that extends first order unification, could be used as a basis to define inference algorithms for other (more powerful) systems with intersection.
---
paper_title: Principality and decidable type inference for finite-rank intersection types

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable α-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principality and type inference for intersection types using expansion variables

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Implementing Compositional Analysis Using Intersection Types With Expansion Variables

paper_content:

Abstract A program analysis is compositional when the analysis result for a particular program fragment is obtained solely from the results for its immediate subfragments via some composition operator. This means the subfragments can be analyzed independently in any order. Many commonly used program analysis techniques (in particular, most abstract interpretations and most uses of the Hindley/Milner type system) are not compositional and require the entire text of a program for sound and complete analysis. System ::: I is a recent type system for the pure λ-calculus with intersection types and the new technology of expansion variables. System ::: I supports compositional analysis because it has the principal typings property and an algorithm based on the new technology of β-unification has been developed that finds these principal typings. In addition, for each natural number k, typability in the rank-k restriction of System ::: I is decidable, so a complete and terminating analysis algorithm exists for the rank-k restriction. This paper presents new understanding that has been gained from working with multiple implementations of System ::: I and β-unification-based analysis algorithms. The previous literature on System ::: I presented the type system in a way that helped in proving its more important theoretical properties, but was not as easy to follow as it could be. This paper provides a presentation of many aspects of System ::: I that should be clearer as well as a discussion of important implementation issues.
---
paper_title: A calculus with polymorphic and polyvariant flow types

paper_content:

We present λCIL, a typed λ-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of λCIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since λCIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: A typed intermediate language for flow-directed compilation

paper_content:

We present a typed intermediate language λCIL for optimizing compilers for function-oriented and polymorphically typed programming languages (e.g., ML). The language λCIL is a typed lambda calculus with product, sum, intersection, and union types as well as function types annotated with flow labels. A novel formulation of intersection and union types supports encoding flow information in the typed program representation. This flow information can direct optimization.
---
paper_title: A modular, polyvariant and type-based closure analysis

paper_content:

We observe that the principal typing property of a type system is the enabling technology for modularity and separate compilation [10]. We use this technology to formulate a modular and polyvariant closure analysis, based on the rank 2 intersection types annotated with control-flow information.Modularity manifests itself in a syntax-directed, annotated-type inference algorithm that can analyse program fragments containing free variables: a principal typing property is used to formalise it. Polyvariance manifests itself in the separation of different behaviours of the same function at its different uses: this is formalised via the rank 2 intersection types. As the rank 2 intersection type discipline types at least all (core) ML programs, our analysis can be used in the separate compilation of such programs.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Principality and decidable type inference for finite-rank intersection types

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable α-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principality and type inference for intersection types using expansion variables

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: The Lambda Calculus: Its Syntax and Semantics

paper_content:

Towards the Theory. Introduction. Conversion. Reduction. Theories. Models. Conversion. Classical Lambda Calculus. The Theory of Combinators. Classical Lambda Calculus (Continued). The Lambda-Calculus. Bohm Trees. Reduction. Fundamental Theorems. Strongly Equivalent Reductions. Reduction Strategies. Labelled Reduction. Other Notions of Reduction. Theories. Sensible Theories. Other Lambda Theories. Models. Construction of Models. Local Structure of Models. Global Structure of Models. Combinatory Groups. Appendices: Typed Lambda Calculus. Illative Combinatory Logic. Variables. References.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Principality and decidable type inference for finite-rank intersection types

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable α-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principality and type inference for intersection types using expansion variables

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Unification with expansion variables

paper_content:

A sanitary waste collector has a disposable container forming a scoop. The container is loaded onto and carried by a rod and frame assembly. The eliminations of an animal may be captured directly into or be scooped into the container with the aid of a disposable scraper at the end of a separate spring loaded rod and handle assembly. When the container is filled it is sealed by pulling a pull ribbon attached to a folded flap at the bottom of the container and by pulling the flap over the front of and onto the top of the container and pressing the flap against an adhesive surface. The sealed container can drop out by inverting the rod and frame assembly.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: Principal type schemes for the strict type assignment system

paper_content:

We study the strict type assignment system, a restriction of the intersection type discipline (6), and prove that it has t he principal type property. We define, for a term M , the principal pair (of basis and type). We specify three operations on pairs, and prove that all pairs deducible for M can be obtained from the principal one by these operations, and that these map deducible pairs to deducible pairs. There are various ways to deal with the problem of handling types in programming languages, that can roughly be divided in the 'typed'- and 'untyped'-approache s. The 'typed'-approach can be found in pro- gramming languages that have explicit typing: objects in a program have types that are provided by the pro- grammer, and the type-algorithm incorporated in the compiler for the language checks if these are used con- sistently. The 'untyped'-approach is used in languages tha t allow programmers to write programs without any type-specification at all, and it is the task of the type-a lgorithm to infer types for objects and to check consistency. Many of the now existing type assignment systems for functional programming languages - that use the 'untyped'-approach - are based on (extensions o f) the Curry type assignment system (11, 12) for the pure, untyped lambda calculus (5). For example, the functional programming language ML (19) is in fact an extended lambda calculus and its type system is based on Curry's system. It is well known that in Curry's system, the problem of typeab ility Given a term M , are there B and σ such that B ⊢ M :σ (i.e. M can be typed with the type σ starting from a basis B)? is decidable. This system also has the principal type property: M is typeable if and only if there is a pair h P , πi of basis and type, called the principal pair for M , such that: 1. P ⊢ M :π, and 2. for every pair h B, σi such that B ⊢ M :σ, there exists an operation O (from a specified set of operations) such that O (h P , πi ) = h B, σi . The type π is then called the principal type for M. For Curry's system the operation O consists entirely of substitutions, i.e. operations that replace type-varia bles by types. (Principal type schemes for Curry's system are defined in (15).) The existence of a principal type for a typeable lambda term M shows an internal coherence between all types that can be assigned to M. Since substitution is an easy operation, in Curry's system the set {h B, σi | B ⊢ M :σ} can be computed in a simple way from the principal pair for M.
---
paper_title: Principal Types and Unification for Simple Intersection Type Systems

paper_content:

In this paper we introduce a decidable restriction of the intersection type discipline. The restriction is based on a uniform principle rather than on a notion of rank. For this system we give a type checking algorithm that we prove to be sound and complete. An extended language of types with labelled intersections and intersection schemes is needed to describe the principal type of terms which turns out to be unique module a set of equations between labels. The unification algorithm far labelled types, that extends first order unification, could be used as a basis to define inference algorithms for other (more powerful) systems with intersection.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: The Lambda Calculus: Its Syntax and Semantics

paper_content:

Towards the Theory. Introduction. Conversion. Reduction. Theories. Models. Conversion. Classical Lambda Calculus. The Theory of Combinators. Classical Lambda Calculus (Continued). The Lambda-Calculus. Bohm Trees. Reduction. Fundamental Theorems. Strongly Equivalent Reductions. Reduction Strategies. Labelled Reduction. Other Notions of Reduction. Theories. Sensible Theories. Other Lambda Theories. Models. Construction of Models. Local Structure of Models. Global Structure of Models. Combinatory Groups. Appendices: Typed Lambda Calculus. Illative Combinatory Logic. Variables. References.
---
paper_title: Game semantics and abstract machines

paper_content:

The interaction processes at work by M. Hyland and L. Ong (1994) (HO) and S. Abramsky et al. (1994) (AJM) new game semantics are two preexisting paradigmatic implementations of linear head reduction: respectively Krivine's abstract machine and Girard's interaction abstract machine. There is a simple and natural embedding of AJM-games to HO-games, mapping strategies to strategies and reducing AJM definability (or full abstraction) property to HO's one.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: Principal type schemes for the strict type assignment system

paper_content:

We study the strict type assignment system, a restriction of the intersection type discipline (6), and prove that it has t he principal type property. We define, for a term M , the principal pair (of basis and type). We specify three operations on pairs, and prove that all pairs deducible for M can be obtained from the principal one by these operations, and that these map deducible pairs to deducible pairs. There are various ways to deal with the problem of handling types in programming languages, that can roughly be divided in the 'typed'- and 'untyped'-approache s. The 'typed'-approach can be found in pro- gramming languages that have explicit typing: objects in a program have types that are provided by the pro- grammer, and the type-algorithm incorporated in the compiler for the language checks if these are used con- sistently. The 'untyped'-approach is used in languages tha t allow programmers to write programs without any type-specification at all, and it is the task of the type-a lgorithm to infer types for objects and to check consistency. Many of the now existing type assignment systems for functional programming languages - that use the 'untyped'-approach - are based on (extensions o f) the Curry type assignment system (11, 12) for the pure, untyped lambda calculus (5). For example, the functional programming language ML (19) is in fact an extended lambda calculus and its type system is based on Curry's system. It is well known that in Curry's system, the problem of typeab ility Given a term M , are there B and σ such that B ⊢ M :σ (i.e. M can be typed with the type σ starting from a basis B)? is decidable. This system also has the principal type property: M is typeable if and only if there is a pair h P , πi of basis and type, called the principal pair for M , such that: 1. P ⊢ M :π, and 2. for every pair h B, σi such that B ⊢ M :σ, there exists an operation O (from a specified set of operations) such that O (h P , πi ) = h B, σi . The type π is then called the principal type for M. For Curry's system the operation O consists entirely of substitutions, i.e. operations that replace type-varia bles by types. (Principal type schemes for Curry's system are defined in (15).) The existence of a principal type for a typeable lambda term M shows an internal coherence between all types that can be assigned to M. Since substitution is an easy operation, in Curry's system the set {h B, σi | B ⊢ M :σ} can be computed in a simple way from the principal pair for M.
---
paper_title: Principal type schemes for an extended type theory

paper_content:

We consider the extension of Curry's basic functionality theory presented by Barendregt et al. (to appear), and we define, for any term X, a principal type scheme (p.t.s.). We prove that all and the only type schemes deducible for X can be obtained from the p.t.s. of X by suitable operations.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Principality and decidable type inference for finite-rank intersection types

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable α-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principality and type inference for intersection types using expansion variables

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principal type schemes for the strict type assignment system

paper_content:

We study the strict type assignment system, a restriction of the intersection type discipline (6), and prove that it has t he principal type property. We define, for a term M , the principal pair (of basis and type). We specify three operations on pairs, and prove that all pairs deducible for M can be obtained from the principal one by these operations, and that these map deducible pairs to deducible pairs. There are various ways to deal with the problem of handling types in programming languages, that can roughly be divided in the 'typed'- and 'untyped'-approache s. The 'typed'-approach can be found in pro- gramming languages that have explicit typing: objects in a program have types that are provided by the pro- grammer, and the type-algorithm incorporated in the compiler for the language checks if these are used con- sistently. The 'untyped'-approach is used in languages tha t allow programmers to write programs without any type-specification at all, and it is the task of the type-a lgorithm to infer types for objects and to check consistency. Many of the now existing type assignment systems for functional programming languages - that use the 'untyped'-approach - are based on (extensions o f) the Curry type assignment system (11, 12) for the pure, untyped lambda calculus (5). For example, the functional programming language ML (19) is in fact an extended lambda calculus and its type system is based on Curry's system. It is well known that in Curry's system, the problem of typeab ility Given a term M , are there B and σ such that B ⊢ M :σ (i.e. M can be typed with the type σ starting from a basis B)? is decidable. This system also has the principal type property: M is typeable if and only if there is a pair h P , πi of basis and type, called the principal pair for M , such that: 1. P ⊢ M :π, and 2. for every pair h B, σi such that B ⊢ M :σ, there exists an operation O (from a specified set of operations) such that O (h P , πi ) = h B, σi . The type π is then called the principal type for M. For Curry's system the operation O consists entirely of substitutions, i.e. operations that replace type-varia bles by types. (Principal type schemes for Curry's system are defined in (15).) The existence of a principal type for a typeable lambda term M shows an internal coherence between all types that can be assigned to M. Since substitution is an easy operation, in Curry's system the set {h B, σi | B ⊢ M :σ} can be computed in a simple way from the principal pair for M.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: A New Presentation of the Intersection Type Discipline Through Principal Typings of Normal Forms

paper_content:

We introduce an intersection type system which is a restriction of the intersection type discipline. This restriction leads to a principal type property for normal forms in the classical sense, while retaining the expressivity of the classical discipline. We characterize the structure of principal types of normal forms and give an algorithm that reconstructs normal forms from types. Having shown the equivalence between principal types and normal forms, we define an expansion operation on types which allows us to recover all possible types for any normalizable $\lambda$-term. The contribution of this work is a new and simpler presentation of the intersection type discipline through a purely syntactic and completely characterized notion of principal types.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Implementing Compositional Analysis Using Intersection Types With Expansion Variables

paper_content:

Abstract A program analysis is compositional when the analysis result for a particular program fragment is obtained solely from the results for its immediate subfragments via some composition operator. This means the subfragments can be analyzed independently in any order. Many commonly used program analysis techniques (in particular, most abstract interpretations and most uses of the Hindley/Milner type system) are not compositional and require the entire text of a program for sound and complete analysis. System ::: I is a recent type system for the pure λ-calculus with intersection types and the new technology of expansion variables. System ::: I supports compositional analysis because it has the principal typings property and an algorithm based on the new technology of β-unification has been developed that finds these principal typings. In addition, for each natural number k, typability in the rank-k restriction of System ::: I is decidable, so a complete and terminating analysis algorithm exists for the rank-k restriction. This paper presents new understanding that has been gained from working with multiple implementations of System ::: I and β-unification-based analysis algorithms. The previous literature on System ::: I presented the type system in a way that helped in proving its more important theoretical properties, but was not as easy to follow as it could be. This paper provides a presentation of many aspects of System ::: I that should be clearer as well as a discussion of important implementation issues.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: Beta-Reduction As Unification

paper_content:

Abstract We define a unification problem ^UP with the property that, given a pure lambda-term M, we can derive an instance Gamma(M) of ^UP from M such that Gamma(M) has a solution if and only if M is beta-strongly normalizable. There is a type discipline for pure lambda-terms that characterizes beta-strong normalization; this is the system of intersection types (without a ``top'''' type that can be assigned to every lambda-term). In this report, we use a lean version LAMBDA of the usual system of intersection types. Hence, ^UP is also an appropriate unification problem to characterize typability of lambda-terms in LAMBDA. It also follows that ^UP is an undecidable problem, which can in turn be related to semi-unification and second-order unification (both known to be undecidable).
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Principality and decidable type inference for finite-rank intersection types

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable α-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: Principality and type inference for intersection types using expansion variables

paper_content:

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

paper_content:

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.
---
paper_title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

paper_content:

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
---
paper_title: Unification with expansion variables

paper_content:

A sanitary waste collector has a disposable container forming a scoop. The container is loaded onto and carried by a rod and frame assembly. The eliminations of an animal may be captured directly into or be scooped into the container with the aid of a disposable scraper at the end of a separate spring loaded rod and handle assembly. When the container is filled it is sealed by pulling a pull ribbon attached to a folded flap at the bottom of the container and by pulling the flap over the front of and onto the top of the container and pressing the flap against an adhesive surface. The sealed container can drop out by inverting the rod and frame assembly.
---

Title: Expansion: the Crucial Mechanism for Type Inference with Intersection Types: Survey and Explanation

Section 1: Background and Motivation
Description 1: This section discusses the importance of types in software, the need for type inference and polymorphism, and introduces ∀-quantification and intersection types along with their limitations and advantages.

Section 2: ∀-quantification, and its limitations
Description 2: This section provides an in-depth discussion on the use of ∀-quantification in type inference and the limitations it imposes on compiler optimizations and principal typings.

Section 3: Intersection types: some advantages, some issues
Description 3: This section introduces intersection types, their semantic basis, benefits, and issues, and discusses the advantages they provide for compiler optimizations and compositional analysis.

Section 4: Intersection types
Description 4: This section introduces the minimal intersection type system used throughout the paper, including better notation for typing judgements, choice of intersection type constructor, and reasons for using proof terms.

Section 5: Skeletons and typing judgments
Description 5: This section describes the role of skeletons in typing judgments and their necessity for capturing the structure of derivations with intersection types.

Section 6: Expansion
Description 6: This section introduces the concept of expansion, demonstrates its importance with examples, explains its historical and modern forms, and discusses expansion variables.

Section 7: A problematic type inference example
Description 7: This subsection presents an example that illustrates the challenges in type inference and the necessity of using intersection types.

Section 8: Expansion to the rescue!
Description 8: This subsection shows how expansion provides a solution to the type inference problem demonstrated in the previous section.

Section 9: What historical expansion is
Description 9: This subsection details the historical implementation of expansion, including its basis on the nucleus of typings and the rules governing its application.

Section 10: Modern expansion with expansion variables
Description 10: This subsection explains the modern approach to expansion using expansion variables, including the new typing rules and substitution applications.

Section 11: Principality and type inference for the BCD system
Description 11: This section discusses the BCD system of intersection types, its subtyping relation, and the methods for defining principal typings and type inference.

Section 12: Strict intersection types
Description 12: This section introduces strict intersection types, their differences from the BCD system, and their implications for type inference and program analysis.

Section 13: Expansion and "simple" intersection types
Description 13: This section compares simple intersection types with System P and discusses their relationship and similarities.

Section 14: Expansion and rank-2 intersection types
Description 14: This section discusses rank-2 intersection types, their restrictions, and their implications for type inference and evaluation.

Section 15: Limitations of historical expansion
Description 15: This section outlines the difficulties and limitations of historical expansion, including its non-local nature and complexity in handling additional type constructors.

Section 16: The omega expansion
Description 16: This section introduces the omega type, its role in intersection type systems, and its integration with expansion.

Section 17: Other significant issues
Description 17: This section discusses various issues related to expansion and expansion variables, including the composition of substitutions, the impact of algebraic laws on types, and type inference with constraints.

Section 18: Linearity and non-linearity
Description 18: This section elaborates on the differences between linear and non-linear types, their impact on type precision, and the implications for usage analysis and type inference.

Section 19: The history of expansion variables
Description 19: This section provides a historical overview of the development of expansion variables and their implementations in different type systems.

Section 20: Conclusion
Description 20: This section summarizes the importance of expansion for type inference with intersection types, discusses the benefits of expansion variables, and outlines ongoing and future work.

Section 21: Near future of expansion variables
Description 21: This section outlines the ongoing work with expansion variables, particularly with System E, and discusses future developments and challenges.

Section 22: Some interesting open challenges
Description 22: This section identifies open challenges in the field of expansion variables, including unification problems, denotational semantics, and integration with practical programming languages.