We investigate Cpo-algebraic completeness and compactness. This is a particularly well behaved setting. For example, we show that Cpo-algebraic completeness and parameterised Cpo-algebraic completeness coincide; whilst, for Cppo⊥-categories, we further show the coincidence of Cpo-algebraic completeness and parameterised Cpo-algebraic compactness. As a by-product, we identify a 2-category of kinds, called Kind, all of whose objects are parameterised Cpo-algebraically ω-compact categories. Kind is 2-cartesian-closed, op-closed, closed under the formation of categories of algebras and coalgebras with lax homomorphisms, and has a unique (up to isomorphism) uniform fixed-point operator. Thus, Kind is appropriate for interpreting type systems with kinds built by recursion from products, exponentials, algebras and coalgebras; but neither such a system nor its interpretation will be discussed here.

Cpo-Algebraic Completeness

Cpo-algebraic completeness is studied. First, we focus on those Cpo-categories for which the initial object embeds in every object of the category. The reason being that in this case the presence of colimits of ω-chains of embeddings guarantees algebraic ω-completeness which turns out to coincide with algebraic completeness. Further, an equational characterisation of initial algebras becomes available. Second, we explore categories of algebras and lax homomorphisms to finally show that algebraic completeness and parameterised algebraic completeness coincide.

Definition 7.1.1 In a Poset-category, an e-initial object is an initial object such that every morphism with it as source is an embedding. The dual notion is called a p-terminal object. An object which is both e-initial and p-terminal is called an ep-zero.

The denotational semantics approach to the semantics of programming languages understands the language constructions by assigning elements of mathematical structures to them. The structures form so-called categories of domains and the study of their closure properties is the subject of domain theory [Sco70,Sco82,Plo83a,GS90,AJ94].

Typically, categories of domains consist of suitably complete partially ordered sets together with continuous maps. But, what is a category of domains? Our aim in this thesis is to answer this question by axiomatising the categorical structure needed on a category so that it can be considered a category of domains. Criteria required from categories of domains can be of the most varied sort. For example, we could ask them to

• have fixed-point operators for endomorphisms and endofunctors;

• have a rich collection of type constructors: coproducts, products, exponentials, powerdomains, dependent types, polymorphic types, etc;

• have a Stone dual providing a logic of observable properties [Abr87, Vic89,Zha91];

• have only computable maps [Sco76,Smy77,McC84,Ros86,Pho90a].

The criteria adopted here will be quite modest but rich enough for the denotational semantics of deterministic programming languages. For us a category of domains will be a category with the structure necessary to support the interpretation of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types). And our axiomatic approach will aim not only at clarifying the categorical structure needed on a category for doing domain theory but also at relating such mathematical criteria with computational criteria.

This thesis is an investigation into axiomatic categorical domain theory as needed for the denotational semantics of deterministic programming languages.

To provide a direct semantic treatment of non-terminating computations, we make partiality the core of our theory. Thus, we focus on categories of partial maps. We study representability of partial maps and show its equivalence with classifiability. We observe that, once partiality is taken as primitive, a notion of approximation may be derived. In fact, two notions of approximation, contextual approximation and specialisation, based on testing and observing partial maps are considered and shown to coincide. Further we characterise when the approximation relation between partial maps is domain-theoretic in the (technical) sense that the category of partial maps Cpo-enriches with respect to it.

Concerning the semantics of type constructors in categories of partial maps, we present a characterisation of colimits of diagrams of total maps; study order-enriched partial cartesian closure; and provide conditions to guarantee the existence of the limits needed to solve recursive type equations. Concerning the semantics of recursive types, we motivate the study of enriched algebraic compactness and make it the central concept when interpreting recursive types. We establish the fundamental property of algebraically compact categories, namely that recursive types on them admit canonical interpretations, and show that in algebraically compact categories recursive types reduce to inductive types. Special attention is paid to Cpo-algebraic compactness, leading to the identification of a 2-category of kinds with very strong closure properties.

Everyone accepts that large programs should be organized as hierarchical modules. Standard ml's structures and signatures meet this requirement. Structures let us package up declarations of related types, values and functions. Signatures let us specify what components a structure must contain. Using structures and signatures in their simplest form we have treated examples ranging from the complex numbers in Chapter 2 to infinite sequences in Chapter 5.

A modular structure makes a program easier to understand. Better still, the modules ought to serve as interchangeable parts: replacing one module by an improved version should not require changing the rest of the program. Standard ml'sabstract types and functors can help us meet this objective too.

A module may reveal its internal details. When the module is replaced, other parts of the program that depend upon such details will fail. ml provides several ways of declaring an abstract type and related operations, while hiding the type's representation.

If structure B depends upon structure A, and we wish to replace A by another structure A′, we could edit the program text and recompile the program. That is satisfactory if A is obsolete and can be discarded. But what if A and A′ are both useful, such as structures for floating point arithmetic in different precisions?

ml lets us declare B to take a structure as a parameter.

In the previous chapters, with their spiraling build-up of repetition and variations, you may have felt like you were being subjected to the Lisp-equivalent of Ravel's Bolero. Even so, no doubt you noticed two motifs were missing: assignment and side effects. Some languages abhor both because of their nasty characteristics, but since Lisp dialects procure them, we really have to study them here. This chapter examines assignment in detail, along with other side effects that can be perpetrated. During these discussions, we'll necessarily digress to other topics, notably, equality and the semantics of quotations.

Coming from conventional algorithmic languages, assignment makes it more or less possible to modify the value associated with a variable. It induces a modification of the state of the program that must record, in one way or another, that such and such a variable has a value other than its preceding one. For those who have a taste for imperative languages, the meaning we could attribute to assignment seems simple enough. Nevertheless, this chapter will show that the presence of closures as well as the heritage of λ-calculus complicates the ideas of binding and variables.

The major problem in defining assignment (and side effects, too) is choosing a formalism independent of the traits that we want to define. As a consequence, neither assignment nor side effects can appear in the definition.

Once again, here's a chapter about compilation, but this time, we'll look at new techniques, notably, flat environments, and we have a new target language: C. This chapter takes up a few of the problems of this odd couple. This strange marriage has certain advantages, like free optimizations of the compilation at a very low level or freely and widely available libraries of immense size. However, there are some thorns among the roses, such as the fact that we can no longer guarantee tail recursion, and we have a hard time with garbage collection.

Compiling into a high-level language like C is interesting in more ways than one. Since the target language is so rich, we can hope for a translation that is closer to the original than would be some shapeless, linear salmagundi. Since C is available on practically any machine, the code we produce has a good chance of being portable. Moreover, any optimizations that such a compiler can achieve are automatically and implicitly available to us. This fact is particularly important in the case of C, where there are compilers that carry out a great many optimizations with respect to allocating registers, laying out code, or choosing modes of address—all things that we could ignore when we focused on only one source language.

On the other hand, choosing a high-level language as the target imposes certain philosophic and pragmatic constraints as well.

This book originated in lectures on Standard ml and functional programming. It can still be regarded as a text on functional programming — one with a pragmatic orientation, in contrast to the rather idealistic books that are the norm — but it is primarily a guide to the effective use of ml. It even discusses ml's imperative features.

Some of the material requires an understanding of discrete mathematics: elementary logic and set theory. Readers will find it easier if they already have some programming experience, but this is not essential.

The book is a programming manual, not a reference manual; it covers the major aspects of ml without getting bogged down with every detail. It devotes some time to theoretical principles, but is mainly concerned with efficient algorithms and practical programming.

The organization reflects my experience with teaching. Higher-order functions appear late, in Chapter 5. They are usually introduced at the very beginning with some contrived example that only confuses students. Higher-order functions are conceptually difficult and require thorough preparation. This book begins with basic types, lists and trees. When higher-order functions are reached, a host of motivating examples is at hand.

The exercises vary greatly in difficulty. They are not intended for assessing students, but for providing practice, broadening the material and provoking discussion.

Overview of the book. Most chapters are devoted to aspects of ml. Chapter 1 introduces the ideas behind functional programming and surveys the history of ml.

Functional programming has its merits, but imperative programming is here to stay. It is the most natural way to perform input and output. Some programs are specifically concerned with managing state: a chess program must keep track of where the pieces are! Some classical data structures, such as hash tables, work by updating arrays and pointers.

Standard ml's imperative features include references, arrays and commands for input and output. They support imperative programming in full generality, though with a flavour unique to ml. Looping is expressed by recursion or using a while construct. References behave differently from Pascal and C pointers; above all, they are secure.

Imperative features are compatible with functional programming. References and arrays can serve in functions and data structures that exhibit purely functional behaviour. We shall code sequences (lazy lists) using references to store each element. This avoids wasteful recomputation, which is a defect of the sequences of Section 5.12. We shall code functional arrays (where updating creates a new array) with the help of mutable arrays. This representation of functional arrays can be far more efficient than the binary tree approach of Section 4.15.

A typical ml program is largely functional. It retains many of the advantages of functional programming, including readability and even efficiency: garbage collection can be faster for immutable objects. Even for imperative programming, ml has advantages over conventional languages.