There is both a great unity and a great diversity in presentations of logic. The diversity is staggering indeed – propositional logic, first-order logic, higher-order logic belong to one classification; linear logic, intuitionistic logic, classical logic, modal and temporal logics belong to another one. Logical deduction may be presented as a Hilbert style of combinators, as a natural deduction system, as sequent calculus, as proof nets of one variety or other, etc. Logic, originally a field of philosophy, turned into algebra with Boole, and more generally into meta-mathematics with Frege and Heyting. Professional logicians such as Gödel and later Tarski studied mathematical models, consistency and completeness, computability and complexity issues, set theory and foundations, etc. Logic became a very technical area of mathematical research in the last half century, with fine-grained analysis of expressiveness of subtheories of arithmetic or set theory, detailed analysis of well-foundedness through ordinal notations, logical complexity, etc. Meanwhile, computer modelling developed a need for concrete uses of logic, first for the design of computer circuits, then more widely for increasing the reliability of sofware through the use of formal specifications and proofs of correctness of computer programs. This gave rise to more exotic logics, such as dynamic logic, Hoare-style logic of axiomatic semantics, logics of partial values (such as Scott's denotational semantics and Plotkin's domain theory) or of partial terms (such as Feferman's free logic), etc. The first actual attempts at mechanisation of logical reasoning through the resolution principle (automated theorem proving) had been disappointing, but their shortcomings gave rise to a considerable body of research, developing detailed knowledge about equational reasoning through canonical simplification (rewriting theory) and proofs by induction (following Boyer and Moore successful integration of primitive recursive arithmetic within the LISP programming language). The special case of Horn clauses gave rise to a new paradigm of non-deterministic programming, called Logic Programming, developing later into Constraint Programming, blurring further the scope of logic. In order to study knowledge acquisition, researchers in artificial intelligence and computational linguistics studied exotic versions of modal logics such as Montague intentional logic, epistemic logic, dynamic logic or hybrid logic. Some others tried to capture common sense, and modeled the revision of beliefs with so-called non-monotonic logics. For the careful crafstmen of mathematical logic, this was the final outrage, and Girard gave his anathema to such “montres à moutardes”.

 Contents  i

 Preface  vii

1.1 Program Structure  3

1.2 The Haskell Kernel  4

1.3 Values and Types  4

1.4 Namespaces  5

This special issue of the Journal of Functional Programming follows up on the First International ACM SIGPLAN Workshop on the Semantics, Applications, and Implementation of Program Generators (SAIG 2000). The special issue contains eight full length papers, which were received based on an open call for papers. Six of these papers are substantially extended revisions of papers presented at the workshop itself.

We study the problem of certifying programs combining imperative and functional features within the general framework of type theory. Type theory is a powerful specification language which is naturally suited for the proof of purely functional programs. To deal with imperative programs, we propose a logical interpretation of an annotated program as a partial proof of its specification. The construction of the corresponding partial proof term is based on a static analysis of the effects of the program which excludes aliases. The missing subterms in the partial proof term are seen as proof obligations, whose actual proofs are left to the user. We show that the validity of those proof obligations implies the total correctness of the program. This work has been implemented in the Coq proof assistant. It appears as a tactic taking an annotated program as argument and generating a set of proof obligations. Several nontrivial algorithms have been certified using this tactic.

We propose regular expression pattern matching as a core feature of programming languages for manipulating XML. We extend conventional pattern-matching facilities (as in ML) with regular expression operators such as repetition (*), alternation (|), etc., that can match arbitrarily long sequences of subtrees, allowing a compact pattern to extract data from the middle of a complex sequence. We then show how to check standard notions of exhaustiveness and redundancy for these patterns. Regular expression patterns are intended to be used in languages with type systems based on regular expression types. To avoid excessive type annotations, we develop a type inference scheme that propagates type constraints to pattern variables from the type of input values. The type inference algorithm translates types and patterns into regular tree automata, and then works in terms of standard closure operations (union, intersection, and difference) on tree automata. The main technical challenge is dealing with the interaction of repetition and alternation patterns with the first-match policy, which gives rise to subtleties concerning both the termination and precision of the analysis. We address these issues by introducing a data structure representing these closure operations lazily.

We study a typing scheme derived from a semantic situation where a single category possesses several closed structures, corresponding to different varieties of function type. In this scheme typing contexts are trees built from two (or more) binary combining operations, or in short, bunches. Bunched typing and its logical counterpart, bunched implications, have arisen in joint work of the author and David Pym. The present paper gives a basic account of the type system, and then focusses on concrete models that illustrate how it may be understood in terms of resource access and sharing. The most basic system has two context-combining operations, and the structural rules of Weakening and Contraction are allowed for one but not the other. This system includes a multiplicative, or substructural, function type −∗ alongside the usual (additive) function type $\rightarrow$; it is dubbed the $\alpha\lambda$-calculus after its binders, $\alpha$ for the $\alpha$dditive binder and $\lambda$ for the multiplicative, or $\lambda$inear, binder. We show that the features of this system are, in a sense, complementary to calculi based on linear logic; it is incompatible with an interpretation where a multiplicative function uses its argument once, but perfectly compatible with a reading based on sharing of resources. This sharing interpretation is derived from syntactic control of interference, a type-theoretic method of controlling sharing of storage, and we show how bunch-based management of Contraction can be used to provide a more flexible type system for interference control.

2.1 Notational Conventions  7

2.2 Lexical Program Structure  8

2.3 Comments  9

2.4 Identifiers and Operators  10

2.5 Numerical Literals  11

2.6 Character and String Literals  12

2.7 Layout  13

Functional languages are particularly well-suited to the interpretive implementations of Domain-Specific Embedded Languages (DSELs). We describe an implemented technique for producing optimizing compilers for DSELs, based on Kamin's idea of DSELs for program generation. The technique uses a data type of syntax for basic types, a set of smart constructors that perform rewriting over those types, some code motion transformations, and a back-end code generator. Domain-specific optimization results from chains of domain-independent rewrites on basic types. New DSELs are defined directly in terms of the basic syntactic types, plus host language functions and tuples. This definition style makes compilers easy to write and, in fact, almost identical to the simplest embedded interpreters. We illustrate this technique with a language Pan for the computationally intensive domain of image synthesis and manipulation.

Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.

This paper presents a novel approach for integrating arrays with access time ${\cal O}$(1) into functional languages. It introduces n-dimensional arrays combined with a type system that supports hierarchies of array types with varying shape information as well as a shape-invariant form of array comprehension called WITH-loop. Together, these constructs allow for a programming style similar to that of array programming languages such as APL. We use Single Assignment C (SAC), a functional C-variant aimed at numerical applications that is based on the proposed design, to demonstrate that programs written in that style can be compiled to code whose runtime performance is competitive with that of hand-optimized Fortran programs. However, essential prerequisites for such performance figures are a shape inference system integrated in the type system as well as several high-level optimizations. Most notably of these is With Loop Folding, an optimization technique for eliminating intermediate arrays.

Education matters. The lack of education on functional programming languages and techniques is visible on a daily basis. Our students, co-workers, friends, and colleagues just don't know enough about these ideas and therefore often fail to implement the best possible solutions for their programming problems.

The purpose of Educational Pearls is to address the education problem of our community from many different angles. It will include contributions on curricula issues, educational software support, and educational experiences. They will help teachers, professors, researchers, and software developers to promote functional programming languages and techniques in their respective contexts.

Fusion is the process of removing intermediate data structures from modularly constructed functional programs. Short cut fusion is a particular fusion technique which uses a single, local transformation rule to fuse compositions of list-processing functions. Short cut fusion has traditionally been treated purely syntactically, and justifications for it have appealed either to intuition or to “free theorems” – even though the latter have not been known to hold in languages supporting higher-order polymorphic functions and fixpoint recursion. In this paper we use Pitts' recent demonstration that contextual equivalence in such languages is parametric to provide the first formal proof of the correctness of short cut fusion for them. In particular, we show that programs which have undergone short cut fusion are contextually equivalent to their unfused counterparts.

First-order unification algorithms (Robinson, 1965) are traditionally implemented via general recursion, with separate proofs for partial correctness and termination. The latter tends to involve counting the number of unsolved variables and showing that this total decreases each time a substitution enlarges the terms. There are many such proofs in the literature (Manna & Waldinger, 1981; Paulson, 1985; Coen, 1992; Rouyer, 1992; Jaume, 1997; Bove, 1999). This paper shows how a dependent type can relate terms to the set of variables over which they are constructed. As a consequence, first-order unification becomes a structurally recursive program, and a termination proof is no longer required. Both the program and its correctness proof have been checked using the proof assistant LEGO (Luo & Pollack, 1992; McBride, 1999).

TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties.

Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability theory and numerical analysis, are well-founded but difficult to implement: the development of a statistical data analysis program for any given application is time-consuming and requires substantial knowledge and experience in several areas. In this paper, we describe AUTOBAYES, a program synthesis system for the generation of data analysis programs from statistical models. A statistical model specifies the properties for each problem variable (i.e. observation or parameter) and its dependencies in the form of a probability distribution. It is a fully declarative problem description, similar in spirit to a set of differential equations. From such a model, AUTOBAYES generates optimized and fully commented C/C++ code which can be linked dynamically into the Matlab and Octave environments. Code is produced by a schema-guided deductive synthesis process. A schema consists of a code template and applicability constraints which are checked against the model during synthesis using theorem proving technology. AUTOBAYES augments schema-guided synthesis by symbolic-algebraic computation and can thus derive closed form solutions for many problems. It is well-suited for tasks like estimating best-fitting model parameters for the given data. Here, we describe AUTOBAYES's system architecture, in particular the schema-guided synthesis kernel. Its capabilities are illustrated by a number of advanced textbook examples and benchmarks.

3.1 Errors  19

3.2 Variables, Constructors, Operators, and Literals  20

3.3 Curried Applications and Lambda Abstractions  21

3.4 Operator Applications  21

3.5 Sections  22

3.6 Conditionals  23

3.7 Lists  23

3.8 Tuples  24

3.9 Unit Expressions and Parenthesized Expessions  25

3.10 Arithmetic Sequences  25

3.11 List Comprehensions  25

3.12 Let Expressions  27

3.13 Case Expressions  27

3.14 Do Expressions  29

3.15 Datatypes with Field Labels  29

3.16 Expression Type Signatures  32

3.17 Pattern Matching  32

This paper presents Biglook, a widget library for an extended version of the Scheme programming language. It uses classes of a Clos-like object layer to represent widgets and Scheme closures to handle graphical events. Combining functional and object-oriented programming styles yields an original application programming interface that advocates a strict separation between the implementation of the graphical interfaces and the user-associated commands, enabling compact source code. The Biglook implementation separates the Scheme programming interface and the native back-end. This permits different ports for Biglook. The current version uses GTK+ and Swing graphical toolkits, while the previous release used Tk.

We show that a non-duplicating transformation into Continuation-Passing Style (CPS) has no effect on control-flow analysis, a positive effect on binding-time analysis for traditional partial evaluation, and no effect on binding-time analysis for continuation-based partial evaluation: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, a monovariant binding-time analysis yields less precise results on a direct-style program than on its CPS counterpart, and an enhanced monovariant binding-time analysis yields equivalent results on a direct-style program and on its CPS counterpart. Our proof technique amounts to constructing the CPS counterpart of flow information and of binding times. Our results formalize and confirm a folklore theorem about traditional binding-time analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that the benefit does not arise from a standard refinement of program analysis, as, for instance, duplicating continuations. The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.

A combinator expression is flat if it can be written without parentheses, that is, if all applications nest to the left, never to the right. This note explores a simple method for flattening combinator expressions involving arbitrary combinators.