Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler declarative specifications is not widely understood, due in part to the difficulty of the available introductions to the area. This tutorial paper offers an ‘end-to-end’ introduction to recursive types and subtyping algorithms, from basic theory to efficient implementation, set in the unifying mathematical framework of coinduction.

We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators.

Since its inception in 1987, Haskell has provided a focal point for research in lazy functional programming. During this time the language has continually evolved, as a result of both theoretical advances and practical experience. Haskell has proved to be a powerful tool for many kinds of programming tasks, and an excellent vehicle for many aspects of computing pedagogy and research. The recent definition of Haskell 98 provides a long-awaited stable version of the language, but there are many exciting possibilities for future versions of Haskell.

We present CMS, a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions. The calculus allows expression of a large variety of existing mechanisms for combining software components, including parameterized modules similar to ML functors, extension with overriding as in object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming. We first present an untyped version of the calculus and then a type system; we prove confluence, progress, and subject reduction properties. Then, we define a derived calculus of mixin modules directly in terms of CMS and show how to encode other primitive calculi into CMS (the lambda calculus and the Abadi-Cardelli object calculus). Finally, we consider the problem of introducing a subtype relation for module types.

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.

This paper presents STAL, a variant of Typed Assembly Language with constructs and types to support a limited form of stack allocation. As with other statically-typed low-level languages, the type system of STAL ensures that a wide class of errors cannot occur at run time, and therefore the language can be adapted for use in certifying compilers where security is a concern. Like the Java Virtual Machine Language (JVML), STAL supports stack allocation of local variables and procedure activation records, but unlike the JVML, STAL does not pre-suppose fixed notions of procedures, exceptions, or calling conventions. Rather, compiler writers can choose encodings for these high-level constructs using the more primitive RISC-like mechanisms of STAL. Consequently, some important optimizations that are impossible to perform within the JVML, such as tail call elimination or callee-saves registers, can be easily expressed within STAL.

This paper serves as a self-contained, tutorial introduction to combinatory models of the untyped lambda calculus. We focus particularly on the interpretation of free variables. We argue that free variables should not be interpreted as elements in a model, as is usually done, but as indeterminates. We claim that the resulting interpretation is more natural and leads to a closer correspondence between models and theories. In particular, it solves the problem of the notorious ζ-rule, which asserts that equations should be preserved under binders, and which fails to be sound for the usual interpretation.

Type classes are a novel combination of parametric polymorphism and constrained types. Although most implementations restrict type classes to be single-parameter, the generalization to multi-parameter type classes has gained increasing attention. A problem with multi-parameter type classes is the increased possibilities they introduce for ambiguity in inferred types, impacting their usefulness in many practical situations. A new type-checking strategy, domain-driven unifying resolution, is identified as an approach to solve these problems. Domain-driven unifying resolution is simple, efficient, and practically useful. However, even with severe restrictions on instance definitions, it is not possible to guarantee that type-checking with unifying resolution terminates. This is in contrast with the naive generalization of single parameter resolution strategies. Domain-driven unifying resolution is guaranteed to terminate if the type class constraints are satisfiable; however satisfiability is undecidable even with severe restrictions on instance definitions. These results shed some light on ambiguity problems with multi-parameter type classes.

This paper gives a static semantics for Haskell 98, a non-strict purely functional programming language. The semantics formally specifies nearly all the details of the Haskell 98 type system, including the resolution of overloading, kind inference (including defaulting) and polymorphic recursion, the only major omission being a proper treatment of ambiguous overloading and its resolution. Overloading is translated into explicit dictionary passing, as in all current implementations of Haskell. The target language of this translation is a variant of the Girard–Reynolds polymorphic lambda calculus featuring higher order polymorphism and explicit type abstraction and application in the term language. Translated programs can thus still be type checked, although the implicit version of this system is impredicative. A surprising result of this formalization effort is that the monomorphism restriction, when rendered in a system of inference rules, compromises the principal type property.

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed π-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and de-allocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our π-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the π-calculus with effects. We propose new equational laws for letregion, analogous to scope mobility laws in the π-calculus, and show them sound in our semantics.

Server applications, and in particular network-based server applications, place a unique combination of demands on a programming language: lightweight concurrency, high I/O throughput, and fault tolerance are all important. This paper describes a prototype web server written in Concurrent Haskell (with extensions), and presents two useful results: firstly, a conforming server could be written with minimal effort, leading to an implementation in less than 1500 lines of code, and secondly the naive implementation produced reasonable performance. Furthermore, making minor modifications to a few time-critical components improved performance to a level acceptable for anything but the most heavily loaded web servers.

DrScheme is a programming environment for Scheme. It fully integrates a graphics-enriched editor, a parser for multiple variants of Scheme, a functional read-eval-print loop, and an algebraic printer. The environment is especially useful for students, because it has a tower of syntactically restricted variants of Scheme that are designed to catch typical student mistakes and explain them in terms the students understand. The environment is also useful for professional programmers, due to its sophisticated programming tools, such as the static debugger, and its advanced language features, such as units and mixins. Beyond the ordinary programming environment tools, DrScheme provides an algebraic stepper, a context-sensitive syntax checker, and a static debugger. The stepper reduces Scheme programs to values, according to the reduction semantics of Scheme. It is useful for explaining the semantics of linguistic facilities and for studying the behavior of small programs. The syntax checker annotates programs with font and color changes based on the syntactic structure of the program. On demand, it draws arrows that point from bound to binding occurrences of identifiers. It also supports α-renaming. Finally, the static debugger provides a type inference system that explains specific inferences in terms of a value-flow graph, selectively overlaid on the program text.

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling and attened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of run-time constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place, thereby avoiding certain beta-expansions required by other frameworks.

Binary search trees are old hat, aren't they? Search trees are routinely covered in introductory computer science classes and they are widely used in functional programming courses to illustrate the benefits of algebraic data types and pattern matching. And indeed, the operation of insertion enjoys a succinct and elegant functional formulation. Figure 1 contains the six-liner given in the language Haskell 98.

Alas, both succinctness and elegance are lost when it comes to implementing the dual operation of deletion, also shown in figure 1. Two additional helper functions are required causing the code size to double in comparison with insertion.

Dependent types reflect the fact that validity of data is often a relative notion by allowing prior data to affect the types of subsequent data. Not only does this make for a precise type system, but also a highly generic one: both the type and the program for each instance of a family of operations can be computed from the data which codes for that instance. Recent experimental extensions to the Haskell type class mechanism give us strong tools to relativize types to other types. We may simulate some aspects of dependent typing by making counterfeit type-level copies of data, with type constructors simulating data constructors and type classes simulating datatypes. This paper gives examples of the technique and discusses its potential.

We systematically develop a functional program that solves the countdown problem, a numbers game in which the aim is to construct arithmetic expressions satisfying certain constraints. Starting from a formal specification of the problem, we present a simple but inefficient program that solves the problem, and prove that this program is correct. We then use program fusion to calculate an equivalent but more efficient program, which is then further improved by exploiting arithmetic properties.

Higher-order languages such as Haskell encourage the programmer to build abstractions by composing functions. A good compiler must inline many of these calls to recover an efficiently executable program. In principle, inlining is dead simple: just replace the call of a function by an instance of its body. But any compiler-writer will tell you that inlining is a black art, full of delicate compromises that work together to give good performance without unnecessary code bloat. The purpose of this paper is, therefore, to articulate the key lessons we learned from a full-scale “production” inliner, the one used in the Glasgow Haskell compiler. We focus mainly on the algorithmic aspects, but we also provide some indicative measurements to substantiate the importance of various aspects of the inliner.

This paper presents a new two-stage CPS algorithm. The first stage plants trivial partial continuations via a recursive-descent traversal and the second stage is a rewrite system that transforms all nontail calls into tail calls. The algorithm combines the metaphors of the Plotkin-style CPS transformation along with reduction in the λ-calculus.

We define a family of embedded domain specific languages for generating HTML and XML documents. Each language is implemented as a combinator library in Haskell. The generated HTML/XML documents are guaranteed to be well-formed. In addition, each library can guarantee that the generated documents are valid XML documents to a certain extent (for HTML only a weaker guarantee is possible). On top of the libraries, Haskell serves as a meta language to define parameterized documents, to map structured documents to HTML/XML, to define conditional content, or to define entire web sites. The combinator libraries support element-transforming style, a programming style that allows programs to have a visual appearance similar to HTML/XML documents, without modifying the syntax of Haskell.