Expansion is an operation on typings (pairs of type environments and result types) in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a λ-term in systems with intersection types. This paper aim

Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason

Reducibility, despite being quite mysterious and inflexible, has been used to prove a number of properties of the λ-calculus and is well known to offer general proofs which can be applied to a number of instantiations. In this paper, we look at two r

A mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or developed type inference for first-class mixin modules, nor has anyone added Milner's let-polymorphism to such a system.This paper proves that typability is NP-complete for the naive approach followed by previous mixin module type systems. Because a λ-calculus extended with record concatenation is a simple restriction of our mixin module calculus, we also prove the folk belief that typability is NP-complete for the naive early type systems for record concatenation.To allow feasible type inference, we present Martini, a new system of simple types for mixin modules with principal typings. Martini is conceptually simple, with no subtyping and a clean and balanced separation between unification-based type inference with type and row variables and constraint solving for safety of linking and field extraction. We have implemented a type inference algorithm and we prove its complexity to be O(n2), or O(n) given a fixed bound on the number of field labels. To prove the complexity, we need to present an algorithm for row unification that may have been implemented by others, but which we could not find written down anywhere. Because Martini has principal typings, we successfully extend it with Milner's let-polymorphism.

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.

This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than standard call-by-value recursive definitions. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be faithful.

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.

The CIL compiler for core Standard ML compiles whole ML programs using a novel typed intermediate language that supports the generation of type-safe customized data representations. In this paper, we present empirical data comparing the relative efficacy of several different flow-based customization strategies for function representations. We develop a cost model to interpret dynamic counts of operations required for each strategy. In this cost model, customizing the representation of closed functions gives a 12-17% improvement on average over uniform closure representations, depending on the layout of the closure. We also present data on the relative effectiveness of various strategies for reducing representation pollution, i.e., situations where flow constraints require the representation of a value to be less efficient than it would be in ideal circumstances. For the benchmarks tested and the types of representation pollution detected by our compiler, the pollution removal strategies we consider often cost more in overhead than they gain via enabled customizations. Notable exceptions are selective defunctionalization, a function representation strategy that often achieves significant customization benefits via aggressive pollution removal, and a simple form of flow-directed inlining, in which pollution removal allows multiple functions to be inlined at the same call site.

Cyclic data structures can be tricky to create and manipulate in declarative programming languages. In a declarative setting, a natural way to view cyclic structures is as denoting regular trees, those trees which may be infinite but have only a finite number of distinct subtrees. This paper shows how to implement the unfold (anamorphism) operator in both eager and lazy languages so as to create cyclic structures when the result is a regular tree as opposed to merely infinite lazy structures. The usual fold (catamorphism) operator when used with a strict combining function on any infinite tree yields an undefined result. As an alternative, this paper defines and show how to implement a cycfold operator with more useful semantics when used with a strict function on cyclic structures representing regular trees. This paper also introduces an abstract data type (cycamores) to simplify the use of cyclic structures representing regular trees in both eager and lazy languages. Implementions of cycamores in both SML and Haskell are presented.

We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ1 Λ τ2 to be used in some places at type τ1 and in other places at type τ2. A finite-rank intersection type system bounds how deeply the Λ can appear in type expressions. Such type systems enjoy strong normalization, subject reduction, and computable type inference, and they support a pragmatics for implementing parametric polymorphism. As a consequence, they provide a conceptually simple and tractable alternative to the impredicative polymorphism of System F and its extensions, while typing many more programs than the Hindley-Milner type system found in ML and Haskell.While type inference is computable at every rank, we show that its complexity grows exponentially as rank increases. Let K(0, n) = n and K(t + 1, n) = 2K(t,n); we prove that recognizing the pure λ-terms of size n that are typable at rank k is complete for DTIME[K(k−1, n)]. We then consider the problem of deciding whether two λ-terms typable at rank k have the same normal form, generalizing a well-known result of Statman from simple types to finite-rank intersection types. We show that the equivalence problem is DTIME[K(K(k − 1, n), 2)]-complete. This relationship between the complexity of typability and expressiveness is identical in wellknown decidable type systems such as simple types and Hindley-Milner types, but seems to fail for System F and its generalizations. The correspondence gives rise to a conjecture that if Τ is a predicative type system where typability has complexity t(n) and expressiveness has complexity e(n), then t(n) = Ω(log* e(n)).

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.

We present a new framework for transforming data representations in a strongly typed intermediate language. Our method allows both value producers (sources) and value consumers (sinks) to support multiple representations, automatically inserting any required code. Specialized representations can be easily chosen for particular source/sink pairs.The framework is based on these techniques:1. Flow annotated types encode the "flows-from" (source) and "flows-to" (sink) information of a flow graph.2. Intersection and union types support (a) encoding precise flow information, (b) separating flow information so that transformations can be well typed, (c) automatically reorganizing flow paths to enable multiple representations.As an instance of our framework, we provide a function representation transformation that encompasses both closure conversion and inlining. Our framework is adaptable to data other than functions.

Two notions of reduction for terms of the /spl lambda/-calculus are introduced and the question of whether a /spl lambda/-term is /spl beta/-strongly normalizing is reduced to the question of whether a /spl lambda/-term is merely normalizing under one of the notions of reduction. This gives a method to prove strong /spl beta/-normalization for typed /spl lambda/-calculi. Instead of the usual semantic proof style based on Tait's realizability or Girard's "candidats de reductibilite", termination can be proved using a decreasing metric over a well-founded ordering. This proof method is applied to the simply-typed /spl lambda/-calculus and the system of intersection types, giving the first non-semantic proof for a polymorphic extension of the /spl lambda/-calculus.

The problems of typability and type checking exist for the Girard/Reynolds second-order polymorphic typed /spl lambda/-calculus (also known as "system F") when it is considered in the "Curry style" (where types are derived for pure /spl lambda/-terms). Until now the decidability of these problems for F itself has remained unknown. We first prove that type checking in F is undecidable by a reduction from semi-unification. We then prove typability in F is undecidable by a reduction from type checking. Since the reduction from typability to type checking in F is already known, the two problems in F are equivalent (reducible to each other). The results hold for both the usual /spl lambda/K-calculus and the more restrictive /spl lambda/I-calculus.>