One of the main goals in preparing this book for publication was to preserve the thesis, as much as possible, in the form that it was originally submitted. With this in mind, we have restricted ourselves to making only very minor changes to the body of the thesis, for example, correcting typographical errors.

On the other hand, we have continued to work with the ideas presented here, to find new applications and to investigate some of the areas identified as topics for further research. In this short chapter, we domment briefly on some examples of this, illustrating both the progress that has been made and some of the new opportunities for further work that have been exposed.

We should emphasize once again that this is the only chapter that was not included as part of the original thesis.

Constructor classes

The initial ideas for a system of constructor classes as sketched in Section 9.2 have been developed in (Jones, 1993b), and full support for these ideas is now included in the standard Gofer distribution (versions 2.28 and later). The two main technical extensions in the system of constructor classes to the work described here are:

• The use of kind inference to determine suitable kinds for all the user-defined type constructors appearing in a given program.

• The extension of the unification algorithm to ensure that it calculates only kind-preserving substitutions. This is necessary to ensure soundness and is dealt with by ensuring that constructor variables are only ever bound to constructors of the corresponding kind. Fortunately, this has a very simple and efficient implementation.

While the results of the preceding chapter provide a satisfactory treatment of type inference with qualified types, we have not yet made any attempt to discuss the semantics or evaluation of overloaded terms. For example, given a generic equality operator (==) of type ∀a.Eq a ⇒ a → a → Bool and integer valued expressions E and F, we can determine that the expression E == F has type Bool in any environment which satisfies Eq Int. However, this information is not sufficient to determine the value of E == F; this is only possible if we are also provided with the value of the equality operator which makes Int an instance of Eq.

Our aim in the next two chapters is to present a general approach to the semantics and implementation of objects with qualified types based on the concept of evidence. The essential idea is that an object of type π ⇒ σ can only be used if we are also supplied with suitable evidence that the predicate π does indeed hold. In this chapter we concentrate on the role of evidence for the systems of predicates described in Chapter 2 and then, in the following chapter, extend the results of Chapter 3 to give a semantics for OML.

As an introduction, Section 4.1 describes some simple techniques used in the implementation of particular forms of overloading and shows why these methods are unsuitable for the more general systems considered in this thesis.

This chapter, describes GTC, an alternative approach to the use of type classes that avoids the problems associated with context reduction, while retaining much of the flexibility of HTC. In addition, GTC benefits from a remarkably clean and efficient implementation that does not require sophisticated compile-time analysis or transformation. As in the previous chapter we concentrate more on implementation details than on formal properties of GTC.

An early description of GTC was distributed to the Haskell mailing list in February 1991 and subsequently used as a basis for Gofer, a small experimental system based on Haskell and described in (Jones, 1991c). The two languages are indeed very close, and many programs that are written with one system in mind can be used with the other with little or no changes. On the other hand, the underlying type systems are slightly different: Using explicit type signature declarations it is possible to construct examples that are well typed in one but not in the other.

Section 8.1 describes the basic principles of GTC and its relationship to HTC. The only significant differences between the two systems are in the methods used to simplify the context part of an inferred type. While HTC relies on the use of context reduction, GTC adopts a weaker form of simplification that does not make use of the information provided in instance declarations.

Section 8.2 describes the implementation of dictionaries used in the current version of Gofer. As an alternative to the treatment of dictionaries as tuples of values in the previous chapter, we give a representation which guarantees that the translation of each member function definition requires at most one dictionary parameter.

The principal aim of this chapter is to show how the concept of evidence can be used to give a semantics for OML programs with implicit overloading.

Outline of chapter

We begin by describing a version of the polymorphic λ-calculus called OP that includes the constructs for evidence application and abstraction described in the previous chapter (Section 5.1). One of the main uses of OP is as the target of a translation from OML with the semantics of each OML term being defined by those of its translation. In Section 5.2 we show how the OML typing derivations for a term E can be interpreted as OP derivations for terms with explicit overloading, each of which is a potential translation for E. It is immediate from this construction that every well-typed OML term has a translation and that all translations obtained in this way are well-typed in OP.

Given that each OML typing typically has many distinct derivations it follows that there will also be many distinct translations for a given term and it is not clear which should be chosen to represent the original term. The OP term corresponding to the derivation produced by the type inference algorithm in Section 3.4 gives one possible choice but it seems rather unnatural to base a definition of semantics on any particular type inference algorithm. A better approach is to show that any two translations of a term are semantically equivalent so that an implementation is free to use whichever translation is more convenient in a particular situation while retaining the same, well-defined semantics.

This chapter expands on the implementation of type classes in Haskell using dictionary values as proposed by Wadler and Blott (1989) and sketched in Section 4.5. For brevity, we refer to this approach to the use of type classes as HTC. The main emphasis in this chapter is on concrete implementation and we adopt a less rigourous approach to formal properties of HTC than in previous chapters. In particular, we describe a number of optimisations that are necessary to obtain an efficient implementation of HTC - i.e. to minimise the cost of overloading. We do not consider the more general problems associated with the efficient implementation of non-strict functional languages like Haskell which are beyond the scope of this thesis.

Section 7.1 describes an important aspect of the system of type classes in Haskell which means that only a particularly simple form of predicate expression can be used in the type signature of an overloaded function. The set of predicates in a Haskell type signature is usually referred to as the context and hence we will use the term context reduction to describe the process of reducing the context to an acceptable form. Context reduction usually results in a small context, acts as a partial check of satisfiability and helps to guarantee decidability of predicate entailment. Unfortunately, it can also interfere with the use of data abstraction and limits the possibilities for extending the Haskell system of type classes.

The main ideas used in the implementation of HTC are described in Section 7.2 including the treatment of default definitions which were omitted from our previous descriptions.

In this thesis we have developed a general formulation of overloading based on the use of qualified types. Applications of qualified types can be described by choosing an appropriate system of predicates and we have illustrated this with particular examples including Haskell type classes, explicit subtyping and extensible records. We have shown how these ideas can be extended to construct a system that combines ML-style polymorphism and overloading in an implicitly typed programming language. Using the concept of evidence we have extended this work to describe the semantics of overloading in this language, establishing sufficient conditions to guarantee that the meaning of a given term is well-defined. Finally, we have described techniques that can be used to obtain efficient concrete implementations of systems based on this framework.

From a theoretical perspective, some of the main contributions of this thesis are:

• The formulation of a general purpose system that can be used to describe a number of different applications of overloading.

• The extension of standard results, for example the existence of principal types, to the type system of OML.

• A new approach to the proof of coherence, based on the use of conversions.

From a practical perspective, we mention:

• The implementation of overloading using the template-based approach, and the closely related implementation of type class overloading in Gofer.

• A new implementation for extensible records, based on the use of evidence.

• The use of information about satisfiability of predicate sets to obtain more informative inferred types.

The key feature of a system of qualified types that distinguishes it from other systems based solely on parametric polymorphism is the use of a language of predicates to describe sets of types (or more generally, relations between types). Exactly which sets of types and relations are useful will (of course) vary from one application to another and it does not seem appropriate to base a general theory on any particular choice. Our solution, outlined in this chapter, is to work in a framework where the properties of a (largely unspecified) language of predicates are described in terms of an entailment relation that is expected to satisfy a few simple laws. In this way, we are able to treat the choice of a language of predicates as a parameter for each of the type systems described in subsequent chapters. This approach also has the advantage that it enables us to investigate how the properties of particular type systems are affected by properties of the underlying systems of predicates.

The basic notation for predicates and entailment is outlined in Section 2.1. The remaining sections illustrate this general framework with applications to: Haskell-style type classes (Section 2.2), subtyping (Section 2.3) and extensible records (Section 2.4). Although we consider each of these examples independently, this work opens up the possibility of combining elements of each in a single concrete programming language.

Basic definitions

For much of this thesis we deal with an abstract language of predicates on types.

Type systems for programming languages

Many programming languages rely on the use of a system of types to distinguish between different kinds of value. This in turn is used to identify two classes of program; those which are well-typed and accepted by the type system, and those that it rejects. Many different kinds of type system have been considered but, in each case, the principal benefits are the same:

• The ability to detect program errors at compile time: A type discipline can often help to detect simple program errors such as passing an inappropriate number of parameters to a function.

• Improved performance: If, by means of the type system, it is possible to ensure that the result of a particular calculation will always be of a certain type, then it is possible to omit the corresponding runtime checks that would otherwise be needed before using that value. The resulting program will typically be slightly shorter and faster.

• Documentation: The types of the values defined in a program are often useful as a simple form of documentation. Indeed, in some situations, just knowing the type of an object can be enough to deduce properties about its behaviour (Wadler, 1989).

The main disadvantage is that no effective type system is complete; there will always be programs that are rejected by the type system, even though they would have produced welldefined results if executed without consideration of the types of the terms involved.

Topology, or the theory of topological spaces, is a thoroughly developed and established branch of mathematics. Its concepts and results are used in almost all areas. In the introduction to his famous treatise General Topology (Kelley [1955]), Kelley states that he almost labelled it: “What every young analyst should know”. In fact, topology is useful in many areas not apparently related to analysis, such as logic and program semantics. As we shall see, Scott–Ershov domains viewed as topological spaces look quite different from the space of, say, real numbers.

The raison d'être of topological spaces is that the continuous functions live on them, that is continuity is a topological concept. More precisely, the topologies on spaces X and Y determine the continuous functions from X into Y. Conversely, given a class of functions from a set X into a set Y we may want to find topologies on X and on Y so that the functions that are continuous with respect to these make up the given class of functions. For example, we have already decided for good reasons which functions between domains are to be continuous. Scott has found a topology on domains for these functions, appropriately called the Scott topology. Ershov's concept of a domain was actually formalized as a topological notion, that is, a domain or, in his terminology, an f0-space is a topological space with certain strong properties (see Exercise 10.7.4).

Power domains were introduced by Plotkin [1976] in order to give a semantics for non-deterministic or parallel programs. Assume that each run or possible outcome of a class of non-deterministic programs has an interpretation in a fixed domain D. Then an interpretation of a non-deterministic program in this class would be the set of interpretations of all possible outcomes of the program. Thus an appropriate domain to interpret this class of non-deterministic programs should be something analogous to the power set of D, let us call it a power domain of D. In this chapter we shall introduce three concepts of power domains, due to Smyth [1978], Hoare and Plotkin [1976], respectively. It turns out that Scott–Ershov domains are closed under Smyth's and Hoare's power domain operations but unfortunately not under Plotkin's. The class of countably based algebraic cpo's (we call these quasidomains) is closed under Plotkin's power domain construction. However, as we observed in Chapter 3, this class is not satisfactory for semantics, since it is not closed under the formation of function space. Therefore we introduce the class of SFP-objects, a subclass of the quasidomains, which is closed under all three power domain constructions as well as under the formation of function space. In fact the category of SFP-objects is the largest full subcategory of the category of quasidomains which is cartesian closed. Thus every countably based Scott–Ershov domain is an SFP-object but there are SFP-objects that are not domains.

In this chapter we investigate some ways domains can be used in order to study other mathematical structures of interest. In Sections 8.1 and 8.2 we consider ultrametric spaces and algebras and show how these can be topologically embedded into domains in a simple way. In Section 8.3 we consider the problem of abstracting the “total” elements of a domain from the partial ones. Then, in Section 8.4, this is used to show how the Kleene–Kreisel continuous functionals are represented in the partial continuous functionals.

Section 8.1 Metric and Ultrametric Spaces

In a general topological space, open sets are used to separate points or sets of points from each other. In many concrete spaces of interest one can do much more in that there is a natural function or metric which to each pair of points assigns a distance between the points, a non-negative real number. It was Fréchet [1906] who abstracted the properties needed from natural metrics on concrete spaces, such as the Euclidean spaces, in order to develop an abstract theory of metric spaces. Chronologically, the theory of metric spaces preceded the general theory of topological spaces introduced by Hausdorff, so that the abstraction to metric spaces was a first important step in obtaining general topological spaces. On the other hand, the metric spaces form an important subclass of the topological spaces.

Metric spaces have been used with success by several authors in order to give semantics for certain programming language constructs.

The λ-calculus was originally introduced as a tool for the study of functionality and higher order logic. Later it was shown that the number-theoretic functions representable in the λ-calculus were precisely those represented in radically different approaches to the notion of computability such as Turing machines or the schemes defining the partial recursive functions we have seen previously. Thus as a tool for studying computability, the λ-calculus is completely general. It also inspired early work on the programming language LISP and can itself be viewed as a high level programming language. Though entirely too cumbersome for everyday programming needs there are well known methods for representing programs, written in standard imperative programming languages like FORTRAN, as λ-terms (see Tennant [1981]). One reason for doing so is in order to understand these programs as functions in the standard mathematical sense of the word. Once these terms are then modelled or interpreted in a mathematical structure like a Scott–Ershov domain one can claim to have understood them in terms of the functions they are names for or denote, hence the terminology denotational semantics. Although the study of the denotational semantics for programming languages falls outside the scope of this book, we will summarize in this chapter the results showing that the λ-calculus itself can be modelled using domains. In doing so we hope that we will have provided at least the basic material needed to make the transition from the mathematical theory of domains to the topic of program semantics.