title: More Haste, Less Speed: Lazy Versus Eager Evaluation

authors:
Richard S. Bird
Geraint Jones
Oege de Moor

abstract: Nicholas Pippenger has recently given a problem that, under two simple restrictions, can be solved in linear time by an impure Lisp program, but requires Ω( n log n ) steps to be solved by any eager pure Lisp program. By showing how to solve the problem in linear time with a lazy functional program, we demonstrate that – for some problems at least – lazy evaluators are strictly more powerful than eager ones.


venue: jfp

title: On Combinatory Complete Sets of Proper Combinators

authors:
Sabine Broda
Luís Damas

abstract: A combinatory system (or equivalently the set of its basic combinators) is called combinatorially complete for a functional system, if any member of the latter can be defined by an entity of the former system. In this paper the decision problem of combinatory completeness for finite sets of proper combinators is studied for three subsystems of the pure lambda calculus. Precise characterizations of proper combinator bases for the linear and the affine λ-calculus are given, and the respective decision problems are shown to be decidable. Furthermore, it is determined which extensions with proper combinators of bases for the linear λ-calculus are combinatorially complete for the λ I -calculus.


title: A Syntactic Method for Finding Least Fixed Points of Higher-Order Functions over Finite Domains

authors:
Tyng-Ruey Chuang
Benjamin Goldberg

abstract: This paper describes a method for finding the least fixed points of higher-order functions over finite domains using symbolic manipulation. Fixed point finding is an essential component in the calculation of abstract semantics of functional programs, providing the foundation for program analyses based on abstract interpretation. Previous methods for fixed point finding have primarily used semantic approaches, which often must traverse large portions of the semantic domain even for simple programs. This paper provides the theoretical framework for a syntax-based analysis that is potentially very fast. The proposed syntactic method is based on an augmented simply typed lambda calculus where the symbolic representation of each function produced in the fixed point iteration is transformed to a syntactic normal form. Normal forms resulting from successive iterations are then compared syntactically to determine their ordering in the semantic domain, and to decide whether a fixed point has been reached. We show the method to be sound, complete and compositional. Examples are presented to show how this method can be used to perform strictness analysis for higher-order functions over non-flat domains. Our method is compositional in the sense that the strictness property of an expression can be easily calculated from those of its sub-expressions. This is contrary to most strictness analysers, where the strictness property of an expression has to be computed anew whenever one of its subexpressions changes. We also compare our approach with recent developments in strictness analysis.


title: On the Effectiveness of Functional Language Features: NAS Benchmark FT

authors:
Jeffrey Hammes
Sumit Sur
A. P. Wim Böhm

abstract: In this paper we investigate the effectiveness of functional language features when writing scientific codes. Our programs are written in the purely functional subset of Id and executed on a one node Motorola Monsoon machine, and in Haskell and executed on a Sparc 2. In the application we study – the NAS FT benchmark, a three-dimensional heat equation solver – it is necessary to target and select one-dimensional sub-arrays in three-dimensional arrays. Furthermore, it is important to be able to share computation in array definitions. We compare first order and higher order implementations of this benchmark. The higher order version uses functions to select one-dimensional sub-arrays, or slices, from a three-dimensional object, whereas the first order version creates copies to achieve the same result. We compare various representations of a three-dimensional object, and study the effect of strictness in Haskell. We also study the performance of our codes when employing recursive and iterative implementations of the one-dimensional FFT, which forms the kernel of this benchmark. It turns out that these languages still have quite inefficient implementations, with respect to both space and time. For the largest problem we could run (32 3 ), Haskell is 15 times slower than Fortran and uses three times more space than is absolutely necessary, whereas Id on Monsoon uses nine times more cycles than Fortran on the MIPS R3000, and uses five times more space than is absolutely necessary. This code, and others like it, should inspire compiler writers to improve the performance of functional language implementations.


title: Thunks and the lambda-Calculus

authors:
John Hatcliff
Olivier Danvy

abstract: Thirty-five years ago, thunks were used to simulate call-by-name under call-by-value in Algol 60. Twenty years ago, Plotkin presented continuation-based simulations of call-by-name under call-by-value and vice versa in the λ-calculus. We connect all three of these classical simulations by factorizing the continuation-based call-by-name simulation [Cscr ]n with a thunk-based call-by-name simulation [Tscr ] followed by the continuation-based call-by-value simulation [Cscr ]v, extended to thunks.formula hereWe show that [Tscr ] actually satisfies all of Plotkin's correctness criteria for [Cscr ]n (i.e. his Indifference, Simulation and Translation theorems). Furthermore, most of the correctness theorems for [Cscr ]n can now be seen as simple corollaries of the corresponding theorems for [Cscr ]v and [Tscr ].


title: A Functional Description of TEX's Formula Layout

authors:
Reinhold Heckmann
Reinhard Wilhelm

abstract: While the quality of the results of T E X's mathematical formula layout algorithm is convincing, its original description is hard to understand since it is presented as an imperative program with complex control flow and destructive manipulations of the data structures representing formulae. In this paper, we present a re-implementation of T E X's formula layout algorithm in the functional language SML, thereby providing a more readable description of the algorithm, extracted from the monolithical T E X system.


title: The Zipper

abstract: Almost every programmer has faced the problem of representing a tree together with a subtree that is the focus of attention, where that focus may move left, right, up or down the tree. The Zipper is Huet's nifty name for a nifty data structure which fulfills this need. I wish I had known of it when I faced this task, because the solution I came up with was not quite so efficient or elegant as the Zipper.


title: Natural Expert: A Commercial Functional Programming Environment

authors:
Nigel W. O. Hutchison
Ute Neuhaus
Manfred Schmidt-Schauß
Cordelia V. Hall

abstract: N ATURAL E XPERT is a product that allows users to build knowledge-based systems. It uses a lazy functional language, N ATURAL E XPERT L ANGUAGE , to implement backward chaining and provide a reliable knowledge processing environment in which development can take place. Customers from all over the world buy the system and have used it to handle a variety of problems, including applications such as airplane servicing and bank loan assessment. Some of these are used 10,000 times or more per month.


title: Leftmost Outside-In Narrowing Calculi

authors:
Tetsuo Ida
Koichi Nakahara

abstract: We present narrowing calculi that are computation models of functional-logic programming languages. The narrowing calculi are based on the notion of the leftmost outside-in reduction of Huet and Lévy. We note the correspondence between the narrowing and reduction derivations, and define the leftmost outside-in narrowing derivation. We then give a narrowing calculus OINC that generates the leftmost outside-in narrowing derivations. It consists of several inference rules that perform the leftmost outside-in narrowing. We prove the completeness of OINC using an ordering defined over a narrowing derivation space. To use the calculus OINC as a model of computation of functional-logic programming, we extend OINC to incorporate strict equality. The extension results in a new narrowing calculus, s-OINC. We show also that s-OINC enjoys the same completeness property as OINC.


title: Extending a lambda-Calculus with Explicit Substitution which Preserves Strong Normalisation Into a Confluent Calculus on Open Terms

authors:
Fairouz Kamareddine
Alejandro Ríos

abstract: The last 15 years have seen an explosion in work on explicit substitution, most of which is done in the style of the λσ-calculus. In Kamareddine and Ríos (1995a), we extended the λ-calculus with explicit substitutions by turning de Bruijn's meta-operators into object-operators offering a style of explicit substitution that differs from that of λσ. The resulting calculus, λ s , remains as close as possible to the λ-calculus from an intuitive point of view and, while preserving strong normalisation (Kamareddine and Ríos, 1995a), is extended in this paper to a confluent calculus on open terms: the λ s e -caculus. Since the establishment of these results, another calculus, λζ, came into being in Muñoz Hurtado (1996) which preserves strong normalisation and is itself confluent on open terms. However, we believe that λ s e still deserves attention because, while offering a new style to work with explicit substitutions, it is able to simulate one step of classical β-reduction, whereas λζ is not. To prove confluence we introduce a generalisation of the interpretation method (cf. Hardin, 1989; Curien et al ., 1992) to a technique which uses weak normal forms (instead of strong ones). We consider that this extended method is a useful tool to obtain confluence when strong normalisation of the subcalculus of substitutions is not available. In our case, strong normalisation of the corresponding subcalculus of substitutions s e , is still a challenging open problem to the rewrite community, but its weak normalisation is established here via an effective strategy.


title: EQUALS - A Fast Parallel Implementation of a Lazy Language

authors:
Owen Kaser
C. R. Ramakrishnan
I. V. Ramakrishnan
R. C. Sekar

abstract: This paper describes E QUALS , a fast parallel implementation of a lazy functional language on a commercially available shared-memory parallel machine, the Sequent Symmetry. In contrast to previous implementations, we propagate normal form demand at compile time as well as run time, and detect parallelism automatically using strictness analysis. The E QUALS implementation indicates the effectiveness of NF-demand propagation in identifying significant parallelism and in achieving good sequential as well as parallel performance. Another important difference between E QUALS and previous implementations is the use of reference counting for memory management, instead of mark-and-sweep or copying garbage collection. Implementation results show that reference counting leads to very good scalability and low memory requirements, and offers sequential performance comparable to generational garbage collectors. We compare the performance of E QUALS with that of other parallel implementations (the 〈 v , G 〉-machine and GAML) as well as with the performance of SML/NJ, a sequential implementation of a strict language.


title: A New Method for Functional Arrays

authors:
Melissa E. O'Neill
F. Warren Burton

abstract: Arrays are probably the most widely used data structure in imperative programming languages, yet functional languages typically only support arrays in a limited manner, or prohibit them entirely. This is not too surprising, since most other mutable data structures, such as trees, have elegant immutable analogues in the functional world, whereas arrays do not. Previous attempts at addressing the problem have suffered from one of three weaknesses, either that they don't support arrays as a persistent data structure (unlike the functional analogues of other imperative data structures), or that the range of operations is too restrictive to support some common array algorithms efficiently, or that they have performance problems. Our technique provides arrays as a true functional analogue of imperative arrays with the properties that functional programmers have come to expect from their data structures. To efficiently support array algorithms from the imperative world, we provide O (1) operations for single-threaded array use. Fully persistent array use can also be provided at O (1) amortized cost, provided that the algorithm satisfies a simple requirement as to uniformity of access. For those algorithms which do not access the array uniformly or single-threadedly, array reads or updates take at most O (log n ) amortized time, where n is the size of the array. Experimental results indicate that the overheads of our technique are acceptable in practice for many applications.


title: Three Algorithms on Braun Trees

abstract: Among the many flavours of balanced binary trees, Braun trees (Braun and Rem, 1983) are perhaps the most circumscribed. For any given node of a Braun tree, the left subtree is either exactly the same size as the right subtree, or one element larger. Braun trees always have minimum height, and the shape of each Braun tree is completely determined by its size. In return for this rigor, algorithms that manipulate Braun trees are often exceptionally simple and elegant, and need not maintain any explicit balance information. Braun trees have been used to implement both flexible arrays (Braun and Rem, 1983; Hoogerwoord, 1992; Paulson, 1996) and priority queues (Paulson, 1996; Bird, 1996). Most operations involving a single element (e.g. adding, removing, inspecting or updating an element) take O (log n ) time, since the trees are balanced. We consider three algorithmically interesting operations that manipulate entire trees. First, we give an O (log 2 n ) algorithm for calculating the size of a tree. Second, we show how to create a tree containing n copies of some element x in O (log n ) time. Finally, we describe an order-preserving algorithm for converting a list to a tree in O ( n ) time. This last operation is not nearly as straightforward as it sounds!


title: Trust in the lambda-Calculus

authors:
Peter Ørbæk
Jens Palsberg

abstract: This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a confluent λ-calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information is presented as annotations of the underlying Curry types, and type inference is computable in O ( n 3 ) time.


title: First-Order Functional Languages and Intensional Logic

authors:
Panos Rondogiannis
William W. Wadge

abstract: The purpose of this paper is to demonstrate that first-order functional programs can be transformed into intensional programs of nullary variables, in a semantics preserving way. On the foundational side, the goal of our study is to bring new insights and a better understanding of the nature of functional languages. From a practical point of view, our investigation provides a formal basis for the tagging mechanism that is used in the implementation of first-order functional languages on dataflow machines.


title: Lazy Wheel Sieves and Spirals of Primes

abstract: The popular method of enumerating the primes is the Sieve of Eratosthenes . It can be programmed very neatly in a lazy functional language, but runs rather slowly. A little-known alternative method is the Wheel Sieve , originally formulated as a fast imperative algorithm for obtaining all primes up to a given limit, assuming destructive access to a bit-array. This article describes functional variants of the wheel sieve that enumerate all primes as a lazy list.


title: Deriving a Lazy Abstract Machine

abstract: We derive a simple abstract machine for lazy evaluation of the lambda calculus, starting from Launchbury's natural semantics. Lazy evaluation here means non-strict evaluation with sharing of argument evaluation, i.e. call-by-need. The machine we derive is a lazy version of Krivine's abstract machine, which was originally designed for call-by-name evaluation. We extend it with datatype constructors and base values, so the final machine implements all dynamic aspects of a lazy functional language.


title: Computational Types from a Logical Perspective

authors:
P. N. Benton
Gavin M. Bierman
Valeria de Paiva

abstract: Moggi's computational lambda calculus is a metalanguage for denotational semantics which arose from the observation that many different notions of computation have the categorical structure of a strong monad on a cartesian closed category. In this paper we show that the computational lambda calculus also arises naturally as the term calculus corresponding (by the Curry–Howard correspondence) to a novel intuitionistic modal propositional logic. We give natural deduction, sequent calculus and Hilbert-style presentations of this logic and prove strong normalisation and confluence results.


title: Meertens Number

abstract: Meertens number is a number with a very peculiar property. I had the idea in 1991, when I was invited to celebrate the occasion of Lambert Meertens' 25 years at the CWI, Amsterdam. Lambert has been a good friend and colleague for a number of years, and rather than bring the usual bottle of Glenlivet as a gift, I decided to give him a number.


title: Functional Unparsing

abstract: A string-formatting function such as printf in C seemingly requires dependent types, because its control string determines the rest of its arguments. Examples: formula here We show how changing the representation of the control string makes it possible to program printf in ML (which does not allow dependent types). The result is well typed and perceptibly more efficient than the corresponding library functions in Standard ML of New Jersey and in Caml.


title: Diets for Fat Sets

abstract: In this paper we describe the discrete interval encoding tree for storing subsets of types having a total order and a predecessor and a successor function. In the following, we consider for simplicity only the case for integer sets; the generalization is not difficult. The discrete interval encoding tree is based on the observation that the set of integers { i [mid ] a [les ] i [les ] b } can be perfectly represented by the closed interval [ a , b ]. The general idea is to represent a set by a binary search tree of integers in which maximal adjacent subsets are each represented by an interval. For example, inserting the sequence of numbers 6, 9, 2, 13, 8, 14, 10, 7, 5 into a binary search tree, respectively, into a discrete interval encoding tree results in the tree structures shown in figure 1. The efficiency of the interval representation, both in terms of space and time, improves with the density of the set, i.e. with the number of adjacencies between set elements. So what we propose is a ‘diet’ (discrete interval encoding tree) for ‘fat’ sets in the sense of ‘the same amount of information with less nodes’.


title: A Theory of Weak Bisimulation for Core CML

authors:
William Ferreira
Matthew Hennessy
Alan Jeffrey

abstract: Concurrent ML (CML) is an extension of Standard ML of New Jersey with concurrent features similar to those of process algebra. In this paper, we build upon John Reppy's reduction semantics for CML by constructing a compositional operational semantics for a fragment of CML, based on higher-order process algebra. Using the operational semantics we generalise the notion of weak bisimulation equivalence to build a semantic theory of CML. We give some small examples of proofs about CML expressions, and show that our semantics corresponds to Reppy's up to weak first-order bisimulation.


title: A Type-Based Escape Analysis for Functional Languages

abstract: An important issue faced by implementors of higher-order functional programming languages is the allocation and deallocation of storage for variables. The possibility of variables escaping their scope during runtime makes traditional stack allocation inadequate. We consider the problem of detecting when variables in such languages do not escape their scope, and thus can have their bindings allocated in an efficient manner. We use an annotated type system to infer information about the use of variables in a higher-order, strict functional language and combine this system with a translation to an annotated language which explicitly indicates which variables do not escape. The type system uses a notion of annotated types which extends the traditional simple type system with information about the extent of variables. To illustrate the use of this information we define an operational semantics for the annotated language which supports both stack and environment allocation of variable bindings. Only the stack allocated bindings need follow the protocol for stacks: their extent may not exceed their scope. Environment allocated bindings can have any extent, and their allocation has no impact on the stack allocated ones. We prove the analysis and translation correct with respect to this operational semantics by adapting a traditional type consistency proof to our setting. We have encoded the proof into the Elf programming language and typechecked it, providing a partially machine-checked proof.


title: Functional Runtime Systems Within the Lambda-Sigma Calculus

authors:
Thérèse Hardin
Luc Maranget

abstract: We define a weak λ-calculus, λσ w , as a subsystem of the full λ-calculus with explicit substitutions λσ [uArr ] . We claim that λσ w could be the archetypal output language of functional compilers, just as the λ-calculus is their universal input language. Furthermore, λσ [uArr ] could be the adequate theory to establish the correctness of functional compilers. Here we illustrate these claims by proving the correctness of four simplified compilers and runtime systems modelled as abstract machines. The four machines we prove are the Krivine machine, the SECD, the FAM and the CAM. Thus, we give the first formal proofs of Cardelli's FAM and of its compiler.


title: A Coherence Theorem for Martin-Löf's Type Theory

abstract: In type theory a proposition is represented by a type, the type of its proofs. As a consequence, the equality relation on a certain type is represented by a binary family of types. Equality on a type may be conventional or inductive. Conventional equality means that one particular equivalence relation is singled out as the equality, while inductive equality – which we also call identity – is inductively defined as the ‘smallest reflexive relation’. It is sometimes convenient to know that the type representing a proposition is collapsed, in the sense that all its inhabitants are identical. Although uniqueness of identity proofs for an arbitrary type is not derivable inside type theory, there is a large class of types for which it may be proved. Our main result is a proof that any type with decidable identity has unique identity proofs. This result is convenient for proving that the class of types with decidable identities is closed under indexed sum. Our proof of the main result is completely formalized within a kernel fragment of Martin-Löf's type theory and mechanized using ALF. Proofs of auxiliary lemmas are explained in terms of the category theoretical properties of identity. These suggest two coherence theorems as the result of rephrasing the main result in a context of conventional equality, where the inductive equality has been replaced by, in the former, an initial category structure and, in the latter, a smallest reflexive relation.


title: Structured Operational Semantics of a Fragment of the Language Scheme

authors:
Furio Honsell
Alberto Pravato
Simona Ronchi Della Rocca

abstract: In this paper we give a big-step Structured Operational Semantics (SOS), in the style of Plotkin, Kahn and Milner, of a significant fragment of the functional programming language Scheme , including quote, eval, quasiquote and unquote. The SOS formalism allows us to discuss incrementally the various features of the language and to keep a low mathematical overhead, thus producing a rigorous account of the semantics of a ‘real’ programming language, which nonetheless has a pedagogical value. More specifically, we formalize four strictly increasing fragments of Scheme, using a number of formal systems which express the evaluation of expressions, the display of output results, and the handling of errors.


title: Monadic Parsing in Haskell

authors:
Graham Hutton
Erik Meijer

abstract: This paper is a tutorial on defining recursive descent parsers in Haskell. In the spirit of one-stop shopping , the paper combines material from three areas into a single source. The three areas are functional parsers (Burge, 1975; Wadler, 1985; Hutton, 1992; Fokker, 1995), the use of monads to structure functional programs (Wadler, 1990, 1992a, 1992b), and the use of special syntax for monadic programs in Haskell (Jones, 1995; Peterson et al ., 1996). More specifically, the paper shows how to define monadic parsers using do notation in Haskell. Of course, recursive descent parsers defined by hand lack the efficiency of bottom-up parsers generated by machine (Aho et al ., 1986; Mogensen, 1993; Gill and Marlow, 1995). However, for many research applications, a simple recursive descent parser is perfectly sufficient. Moreover, while parser generators typically offer a fixed set of combinators for describing grammars, the method described here is completely extensible: parsers are first-class values, and we have the full power of Haskell available to define new combinators for special applications. The method is also an excellent illustration of the elegance of functional programming.


title: Polytypic Unification

authors:
Patrik Jansson
Johan Jeuring

abstract: Unification, or two-way pattern matching, is the process of solving an equation involving two first-order terms with variables. Unification is used in type inference in many programming languages and in the execution of logic programs. This means that unification algorithms have to be written over and over again for different term types. Many other functions also make sense for a large class of datatypes; examples are pretty printers, equality checks, maps etc. They can be defined by induction on the structure of user-defined datatypes. Implementations of these functions for different datatypes are closely related to the structure of the datatypes. We call such functions polytypic. This paper describes a unification algorithm parametrised on the type of the terms, and shows how to use polytypism to obtain a unification algorithm that works for all regular term types.


title: Functorial ML

authors:
C. Barry Jay
Gianna Bellè
Eugenio Moggi

abstract: We present an extension of the Hindley–Milner type system that supports a generous class of type constructors called functors, and provide a parametrically polymorphic algorithm for their mapping, i.e. for applying a function to each datum appearing in a value of constructed type. The algorithm comes from shape theory, which provides a uniform method for locating data within a shape. The resulting system is Church–Rosser and strongly normalizing, and supports type inference. Several different semantics are possible, which affects the choice of constants in the language, and are used to illustrate the relationship to polytypic programming.


title: Efficient Graph Algorithms Using Lazy Monolithic Arrays

abstract: Many, perhaps even most, algorithms that involve data structures are traditionally expressed by incremental updates of the data structures. In functional languages, however, incremental updates are usually both clumsy and inefficient, especially when the data structure is an array. In functional languages, we instead prefer to express such array algorithms using monolithic arrays – wholesale creation of the final answer – both for succinctness of expression, efficiency (only one array created) and (sometimes) implicit parallelism. The ease with which the solution can be reformulated of course depends on the problem, and varies from trivial (e.g. matrix multiplication), to challenging (e.g. solving linear equation systems using Gauss elimination, which in fact can be done by creating only two arrays, recursively defined, of which one is the answer). Other problems have been notoriously resistant to attack; these usually involve some unpredictable processing order of the elements. One such problem is graph marking, i.e. marking the nodes reachable from a set of roots. Hitherto, no functional method has been known except emulating the traditional imperative solution (King & Launchbury, 1995; Launchbury & Peyton Jones, 1995). The contribution of this paper is to show how this problem, and some related ones, can be solved using a novel array creation primitive, lazier than previous ones.


title: Dynamic Tabbing for Automatic Indentation with the Layout Rule

abstract: We show the design principles of an automatic indentation GNU Emacs mode for Haskell and Miranda(tm), functional languages using the ‘layout rule’ instead of the usual parenthetic structures for indentifying dependent program parts.


title: The Call-by-Need Lambda Calculus

authors:
John Maraist
Martin Odersky
Philip Wadler

abstract: We present a calculus that captures the operational semantics of call-by-need. The call-by-need lambda calculus is confluent, has a notion of standard reduction, and entails the same observational equivalence relation as the call-by-name calculus. The system can be formulated with or without explicit let bindings, admits useful notions of marking and developments, and has a straightforward operational interpretation.


title: Animated Fuzzy Logic

authors:
Gary Meehan
Mike Joy

abstract: In this paper we aim to give an introduction to fuzzy logic using the language Haskell to implement our solutions. We shall see how the high-level, declarative nature of a functional language allows us to implement easily and efficiently solutions to problems using fuzzy logic and, in particular, how the presence of functions as first-class values allows us to model the key concept of the fuzzy subset in a natural way.


title: Profiling Large-Scale Lazy Functional Programs

authors:
Richard G. Morgan
Stephen A. Jarvis

abstract: The LOLITA natural language processor is an example of one of the ever-increasing number of large-scale systems written entirely in a functional programming language. The system consists of over 47,000 lines of Haskell code (excluding comments) and is able to perform a wide range of tasks such as semantic and pragmatic analysis of text, information extraction and query analysis. The efficiency of such a system is critical; interactive tasks (such as query analysis) must ensure that the user is not inconvenienced by long pauses, and batch mode tasks (such as information extraction) must ensure that an adequate throughput can be achieved. For the past three years the profiling tools supplied with GHC and HBC have been used to analyse and reason about the complexity of the LOLITA system. There have been good results, however experience has shown that in a large system the profiling life-cycle is often too long to make detailed analysis possible, and the results are often misleading. In response to these problems a profiler has been developed which allows the complete set of program costs to be recorded in so-called cost-centre stacks. These program costs are then analysed using a post-processing tool to allow the developer to explore the costs of the program in ways that are either not possible with existing tools or would require repeated compilations and executions of the program. The modifications to the Glasgow Haskell compiler based on detailed cost semantics and an efficient implementation scheme are discussed. The results of using this new profiling tool in the analysis of a number of Haskell programs are also presented. The overheads of the scheme are discussed and the benefits of this new system are considered. An outline is also given of how this approach can be modified to assist with the tracing and debugging of programs.


title: Functional Pearl: Even Higher-Order Functions for Parsing

abstract: A higher-order function is a function that takes another function as an argument or returns another function as a result. More specifically, a first-order function takes and returns base types, such as integers or lists. A k th-order function takes or returns a function of order k −1. Currying often artificially inflates the order of a function, so we will ignore all inessential currying. (Whether a particular instance of currying is essential or inessential is open to debate, but we expect that our choices will be uncontroversial.) In addition, when calculating the order of a polymorphic function, we instantiate all type variables with base types. Under these assumptions, most common higher-order functions, such as map and foldr , are second-order, so beginning functional programmers often wonder: What good are functions of order three or above? We illustrate functions of up to sixth-order with examples taken from a combinator parsing library. Combinator parsing is a classic application of functional programming, dating back to at least Burge (1975). Most combinator parsers are based on Wadler's list-of-successes technique (Wadler, 1985). Hutton (1992) popularized the idea in his excellent tutorial Higher-Order Functions for Parsing . In spite of the title, however, he considered only functions of up to order three.


title: Expansion Postponement for Normalising Pure Type Systems

abstract: Expansion postponement is a tantalisingly simple conjecture about pure type systems which has so far resisted all attempts to prove it for any interesting class of systems. We prove the property for all normalising pure type systems, and discuss the connection with typechecking.


title: What is a Purely Functional Language?

abstract: Functional programming languages are informally classified into pure and impure languages. The precise meaning of this distinction has been a matter of controversy. We therefore investigate a formal definition of purity. We begin by showing that some proposed definitions which rely on confluence, soundness of the beta axiom, preservation of pure observational equivalences and independence of the order of evaluation, do not withstand close scrutiny. We propose instead a definition based on parameter-passing independence . Intuitively, the definition implies that functions are pure mappings from arguments to results; the operational decision of how to pass the arguments is irrelevant. In the context of Haskell, our definition is consistent with the fact that the traditional call-by-name denotational semantics coincides with the traditional call-by-need implementation. Furthermore, our definition is compatible with the stream-based, continuation-based and monad-based integration of computational effects in Haskell. Finally, we observe that call-by-name reasoning principles are unsound in compilers for monadic Haskell.


title: Why the Constant 'Undefined'? Logics of Partial Terms for Strict and Non-Strict Functional Programming Languages

abstract: In this article we explain two different operational interpretations of functional programs by two different logics. The programs are simply typed λ-terms with pairs, projections, if-then-else and least fixed point recursion. A logic for call-by-value evaluation and a logic for call-by-name evaluation are obtained as as extensions of a system which we call the basic logic of partial terms (BPT). This logic is suitable to prove properties of programs that are valid under both strict and non-strict evaluation. We use methods from denotational semantics to show that the two extensions of BPT are adequate for call-by-value and call-by-name evaluation. Neither the programs nor the logics contain the constant ‘undefined’.


title: Classical Logic, Continuation Semantics and Abstract Machines

authors:
Thomas Streicher
Bernhard Reus

abstract: One of the goals of this paper is to demonstrate that denotational semantics is useful for operational issues like implementation of functional languages by abstract machines. This is exemplified in a tutorial way by studying the case of extensional untyped call-by-name λ-calculus with Felleisen's control operator [Cscr ]. We derive the transition rules for an abstract machine from a continuation semantics which appears as a generalization of the ¬¬-translation known from logic. The resulting abstract machine appears as an extension of Krivine's machine implementing head reduction. Though the result, namely Krivine's machine, is well known our method of deriving it from continuation semantics is new and applicable to other languages (as e.g. call-by-value variants). Further new results are that Scott's D ∞ -models are all instances of continuation models. Moreover, we extend our continuation semantics to Parigot's λμ-calculus from which we derive an extension of Krivine's machine for λμ-calculus. The relation between continuation semantics and the abstract machines is made precise by proving computational adequacy results employing an elegant method introduced by Pitts.


title: From ML to Ada: Strongly-Typed Language Interoperability via Source Translation

authors:
Andrew P. Tolmach
Dino Oliva

abstract: We describe a system that supports source-level integration of ML-like functional language code with ANSI C or Ada83 code. The system works by translating the functional code into type-correct, ‘vanilla’ C or Ada; it offers simple, efficient, type-safe inter-operation between new functional code components and ‘legacy’ third-generation-language components. Our translator represents a novel synthesis of techniques including user-parameterized specification of primitive types and operators; removal of polymorphism by code specialization; removal of higher-order functions using closure datatypes and interpretation; and aggressive optimization of the resulting first-order code, which can be viewed as encoding the result of a closure analysis. Programs remain fully typed at every stage of the translation process, using only simple, standard type systems. Target code runs at speeds comparable to the output of current optimizing ML compilers, even though handicapped by a conservative garbage collector.


title: Algorithms + Strategy = Parallelism

authors:
Philip W. Trinder
Kevin Hammond
Hans-Wolfgang Loidl
Simon L. Peyton Jones

abstract: The process of writing large parallel programs is complicated by the need to specify both the parallel behaviour of the program and the algorithm that is to be used to compute its result. This paper introduces evaluation strategies : lazy higher-order functions that control the parallel evaluation of non-strict functional languages. Using evaluation strategies, it is possible to achieve a clean separation between algorithmic and behavioural code. The result is enhanced clarity and shorter parallel programs. Evaluation strategies are a very general concept: this paper shows how they can be used to model a wide range of commonly used programming paradigms, including divide-and-conquer parallelism, pipeline parallelism, producer/consumer parallelism, and data-oriented parallelism. Because they are based on unrestricted higher-order functions, they can also capture irregular parallel structures. Evaluation strategies are not just of theoretical interest: they have evolved out of our experience in parallelising several large-scale parallel applications, where they have proved invaluable in helping to manage the complexities of parallel behaviour. Some of these applications are described in detail here. The largest application we have studied to date, Lolita, is a 40,000 line natural language engineering system. Initial results show that for these programs we can achieve acceptable parallel performance, for relatively little programming effort.


title: The Dynamic Compilation of Lazy Functional Programs

abstract: Lazy functional languages seem to be unsuitable for programming embedded computers because their implementations require so much memory for program code and graph. In this paper we describe a new abstract machine for the implementation of lazy functional languages on embedded computers called the X-machine. The X-machine has been designed so that program code can be stored compactly as byte code, yet run quickly using dynamic compilation. Our first results are promising – programs typically require only 33% of the code space of an ordinary implementation, but run at 75% of the speed. Future work needs to concentrate on reducing the size of statically-allocated data and the run-time system, and on developing a more detailed understanding of throw-away compilation.


title: Type-checking injective pure type systems

abstract: Injective pure type systems form a large class of pure type systems for which one can compute by purely syntactic means two sorts elmt(Γ[mid ] M ) and sort(Γ[mid ] M ), where Γ is a pseudo-context and M is a pseudo-term, and such that for every sort s , formula here By eliminating the problematic clause in the (abstraction) rule in favor of constraints over elmt(.[mid ].) and sort(.[mid ].), we provide a sound and complete type-checking algorithm for injective pure type systems. In addition, we prove expansion postponement for a variant of injective pure type systems where the problematic clause in the (abstraction) rule is replaced in favor of constraints over elmt(.[mid ].) and sort(.[mid ].).


title: De Bruijn Notation as a Nested Datatype

authors:
Richard S. Bird
Ross Paterson

abstract: “I have no data yet. It is a capital mistake to theorise before one has data.” Sir Arthur Conan Doyle The Adventures of Sherlock Holmes de Bruijn notation is a coding of lambda terms in which each occurrence of a bound variable x is replaced by a natural number, indicating the ‘distance’ from the occurrence to the abstraction that introduced x . One might suppose that in any datatype for representing de Bruijn terms, the distance restriction on numbers would have to be maintained as an explicit datatype invariant. However, by using a nested (or non-regular) datatype, we can define a representation in which all terms are well-formed, so that the invariant is enforced automatically by the type system. Programming with nested types is only a little more difficult than programming with regular types, provided we stick to well-established structuring techniques. These involve expressing inductively defined functions in terms of an appropriate fold function for the type, and using fusion laws to establish their properties. In particular, the definition of lambda abstraction and beta reduction is particularly simple, and the proof of their associated properties is entirely mechanical.


title: Transparent Optimisation of Rewriting Combinators

abstract: The LCF system was the first mechanical theorem prover to be user-programmable via a metalanguage, ML, from which the functional programming language Standard ML has been developed. Paulson has demonstrated how a modular rewriting engine can be implemented in LCF. This provides both clarity and flexibility. This paper shows that the same modular approach (using higher-order functions) allows transparent optimisation of the rewriting engine; performance can be improved while few, if any, changes are required to code written using these functions. The techniques described have been implemented in the HOL system, a descendant of LCF, and some are now in daily use. Comparative results are given. Some of the techniques described, in particular ones to avoid processing parts of a data structure that do not need to be changed, may be of more general use in functional programming and beyond.


title: A Poor Man's Concurrency Monad

abstract: Without adding any primitives to the language, we define a concurrency monad transformer in Haskell. This allows us to add a limited form of concurrency to any existing monad. The atomic actions of the new monad are lifted actions of the underlying monad. Some extra operations, such as fork, to initiate new processes, are provided. We discuss the implementation, and use some examples to illustrate the usefulness of this construction.


title: A confluent lambda-calculus with a catch/throw mechanism

abstract: We derive a confluent λ-calculus with a catch/throw mechanism (called λ ct -calculus) from Parigot's λμ-calculus. We also present several translations from one calculus into the other which are morphisms for the reduction. We use them to show that the λ ct -calculus is a retract of λμ-calculus (these calculi are isomorphic if we consider only convertibility). As a by-product, we obtain the subject reduction property for the λ ct -calculus, as well as the strong normalization for λ ct -terms typable in the second order classical natural deduction.


title: The Semantics of Future and an Application

authors:
Cormac Flanagan
Matthias Felleisen

abstract: The future annotation of MultiLisp provides a simple method for taming the implicit parallelism of functional programs. Prior research on future has concentrated on implementation and design issues, and has largely ignored the development of a semantic characterization of future . This paper considers an idealized functional language with futures and presents a series of operational semantics with increasing degrees of intensionality. The first semantics defines future to be a semantically transparent annotation. The second semantics interprets a future expression as a potentially parallel task. The third semantics explicates the coordination of parallel tasks by introducing placeholder objects and touch operations. We use the last semantics to derive a program analysis algorithm and an optimization algorithm that removes provably redundant touch operations. Experiments with the Gambit compiler indicate that this optimization significantly reduces the overhead imposed by touch operations.


title: Parallelizing functional programs by generalization

authors:
Alfons Geser
Sergei Gorlatch

abstract: List homomorphisms are functions that are parallelizable using the divide-and-conquer paradigm. We study the problem of finding homomorphic representations of functions in the Bird–Meertens constructive theory of lists, by means of term rewriting and theorem proving techniques. A previous work proved that to each pair of leftward and rightward sequential representations of a function, based on cons - and snoc -lists, respectively, there is also a representation as a homomorphism. Our contribution is a mechanizable method to extract the homomorphism representation from a pair of sequential representations. The method is decomposed to a generalization problem and an inductive claim, both solvable by term rewriting techniques. To solve the former we present a sound generalization procedure which yields the required representation, and terminates under reasonable assumptions. The inductive claim is provable automatically. We illustrate the method and the procedure by the systematic parallelization of the scan -function (parallel prefix) and of the maximum segment sum problem.


title: A Pointless Derivation of Radix Sort

abstract: This paper is about point-free (or ‘pointless’) calculations – calculations performed at the level of function composition instead of that of function application. We address this topic with the help of an example, namely calculating the radix-sort algorithm from a more obvious specification of sorting. The message that we hope to send is that point-free calculations are sometimes surprisingly simpler than the corresponding point-wise calculations.


title: Compilation and Equivalence of Imperative Objects

authors:
Andrew D. Gordon
Paul D. Hankin
Søren B. Lassen

abstract: We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus. Our first two results are theorems asserting the equivalence of our substitution-based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.


title: Implementing Theorem Provers in a Purely Functional Style

abstract: This paper discusses the principles of implementing an LCF-style proof assistant using a purely functional metalanguage. Two approaches are described; in both, signatures are treated as ordinary values, rather than as mutable components within an abstract datatype. The first approach treats the object logic as a partial algebra and represents it as a partial datatype, that is, a datatype in which the domains of the constructors are restricted by predicate functions. This results in a compact, executable specification of the logic. The second approach uses an abstract type to allow an efficient representation of the logic, whilst keeping the same interface. A case study describes how these principles were put into practice in implementing a fairly complex dependently-sorted logic.


title: Higher-Order Narrowing with Definitional Trees

authors:
Michael Hanus
Christian Prehofer

abstract: Functional logic languages with a sound and complete operational semantics are mainly based on an inference rule called narrowing. Narrowing extends functional evaluation by goal solving capabilities, as in logic programming. Due to the huge search space of simple narrowing, steadily improved narrowing strategies have been developed in the past. Needed narrowing is currently the best narrowing strategy for first-order functional logic programs due to its optimality properties wrt the length of derivations and the number of computed solutions. In this paper, we extend the needed narrowing strategy to higher-order functions and λ-terms as data structures. By the use of definitional trees, our strategy computes only independent solutions. Thus, it is the first calculus for higher-order functional logic programming which provides for such an optimality result. Since we allow higher-order logical variables denoting λ-terms, applications go beyond current functional and logic programming languages. We show soundness and completeness of our strategy with respect to LNT reductions, a particular form of higher-order reductions defined via definitional trees. A general completeness result is only provided for terminating rewrite systems due to the lack of an overall theory of higher-order reduction which is outside the scope of this paper.


title: Proof-Directed Debugging

abstract: The close relationship between writing programs and proving theorems has frequently been cited as an advantage of functional programming languages. We illustrate the interplay between programming and proving in the development of a program for regular expression matching. The presentation is inspired by Lakatos's method of proofs and refutations in which the attempt to prove a plausible conjecture leads to a revision not only of the proof, but of the theorem itself. We give a plausible implementation of a regular expression matcher that contains a flaw that is uncovered in an attempt to prove its correctness. The failure of the proof suggests a revision of the specification, rather than a change to the code. We then show that a program meeting the revised specification is nevertheless sufficient to solve the original problem.


title: Parallelization of Divide-and-Conquer by Translation to Nested Loops

authors:
Christoph A. Herrmann
Christian Lengauer

abstract: We present a hierarchical classification of specializations of the divide-and-conquer paradigm. The aim is to identify a subclass of divide-and-conquer algorithms with an efficient parallel implementation which can be viewed as a static space-time mapping. The specializations impose a balanced call tree, a fixed degree of the problem division, and elementwise operations. The correctness of our compile-time transformations is proved by equational reasoning in Haskell; recursion and iteration are handled by induction. We demonstrate the practicality of the skeleton by some examples, one of which is Strassen's matrix multiplication.


title: Explaining Binomial Heaps

abstract: Functional programming languages are an excellent tool for teaching algorithms and data structures. This paper explains binomial heaps, a beautiful data structure for priority queues, using the functional programming language Haskell (Peterson and Hammond, 1997). We largely follow a deductive approach: using the metaphor of a tennis tournament we show that binomial heaps arise naturally through a number of logical steps. Haskell supports the deductive style of presentation very well: new types are introduced at ease, algorithms can be expressed clearly and succinctly, and Haskell's type classes allow to capture common algorithmic patterns. The paper aims at the level of an undergraduate student who has experience in reading and writing Haskell programs, and who is familiar with the concept of a priority queue.


title: Semantics of Linear/Modal Lambda Calculus

abstract: This paper was guest-edited by Harry Mairson and Bruce Kapron, for our intended Special Issue on Functional Programming and Computational Complexity. Other papers submitted for the special issue were either out-of-scope or otherwise unsuitable for JFP. Even though only one paper met their high standards, this did not make Harry and Bruce's job any easier, and we thank them for their efforts.In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. While this previous work was concerned with the syntactic metatheory of SLR in this paper we develop a semantics of SLR in terms of Chu spaces over a certain category of sheaves from which it follows that all expressible functions are indeed in PTIME. We notice a similarity between the Chu space interpretation and CPS translation which as we hope will have further applications in functional programming.


title: A Tutorial on the Universality and Expressiveness of Fold

abstract: In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the universal property of fold both as a proof principle that avoids the need for inductive proofs, and as a definition principle that guides the transformation of recursive functions into definitions using fold. Secondly, we show that even though the pattern of recursion encapsulated by fold is simple, in a language with tuples and functions as first-class values the fold operator has greater expressive power than might first be expected.


title: Automatic Verification of Functions with Accumulating Parameters

authors:
Andrew Ireland
Alan Bundy

abstract: Proof by mathematical induction plays a crucial role in reasoning about functional programs. A generalization step often holds the key to discovering an inductive proof. We present a generalization technique which is particularly applicable when reasoning about functional programs involving accumulating parameters. We provide empirical evidence for the success of our technique and show how it is contributing to the ongoing development of a parallelizing compiler for Standard ML.


title: Using randomization to make recursive matrix algorithms practical

authors:
Dinh Lê
Douglas Stott Parker Jr.

abstract: Recursive block decomposition algorithms (also known as quadtree algorithms when the blocks are all square) have been proposed to solve well-known problems such as matrix addition, multiplication, inversion, determinant computation, block LDU decomposition and Cholesky and QR factorization. Until now, such algorithms have been seen as impractical, since they require leading submatrices of the input matrix to be invertible (which is rarely guaranteed). We show how to randomize an input matrix to guarantee that submatrices meet these requirements, and to make recursive block decomposition methods practical on well-conditioned input matrices. The resulting algorithms are elegant, and we show the recursive programs can perform well for both dense and sparse matrices, although with randomization dense computations seem most practical. By ‘homogenizing’ the input, randomization provides a way to avoid degeneracy in numerical problems that permits simple recursive quadtree algorithms to solve these problems.


title: Functional Design and Implementation of Graphical User Interfaces for Theorem Provers

authors:
Christoph Lüth
Burkhart Wolff

abstract: The design of theorem provers, especially in the LCF-prover family, has strongly profited from functional programming. This paper attempts to develop a metaphor suited to visualize the LCF-style prover design, and a methodology for the implementation of graphical user interfaces for these provers and encapsulations of formal methods. In this problem domain, particular attention has to be paid to the need to construct a variety of objects, keep track of their interdependencies and provide support for their reconstruction as a consequence of changes. We present a prototypical implementation of a generic and open interface system architecture, and show how it can be instantiated to an interface for Isabelle, called IsaWin , as well as to a tailored tool for transformational program development, called TAS .


title: Power Series, Power Serious

abstract: Power series and stream processing were made for each other. Stream algorithms for power series are short, sweet, and compositional. Their neatness shines through in Haskell, thanks to pattern-matching, lazy lists, and operator overloading. In a short compass one can build working code from ground zero (scalar operations) up to exact calculation of generating functions and solutions of differential equations.


title: HOLCF=HOL+LCF

authors:
Olaf Müller
Tobias Nipkow
David von Oheimb
Oscar Slotosch

abstract: HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF supports standard domain theory (in particular fixpoint reasoning and recursive domain equations), but also coinductive arguments about lazy datatypes. This paper describes in detail how domain theory is embedded in HOL, and presents applications from functional programming, concurrency and denotational semantics.


title: Parallel Functional Programming on Recursively Defined Data via Data-Parallel Recursion

authors:
Susumu Nishimura
Atsushi Ohori

abstract: This article proposes a new language mechanism for data-parallel processing of dynamically allocated recursively defined data. Different from the conventional array-based data- parallelism, it allows parallel processing of general recursively defined data such as lists or trees in a functional way. This is achieved by representing a recursively defined datum as a system of equations, and defining new language constructs for parallel transformation of a system of equations. By integrating them with a higher-order functional language, we obtain a functional programming language suitable for describing data-parallel algorithms on recursively defined data in a declarative way. The language has an ML style polymorphic type system and a type sound operational semantics that uniformly integrates the parallel evaluation mechanism with the semantics of a typed functional language. We also show the intended parallel execution model behind the formal semantics, assuming an idealized distributed memory multicomputer.


title: Red-Black Trees in a Functional Setting

abstract: Everybody learns about balanced binary search trees in their introductory computer science classes, but even the stouthearted tremble at the thought of actually implementing such a beast. The details surrounding rebalancing are usually just too messy. To show that this need not be the case, we present an algorithm for insertion into red-black trees (Guibas and Sedgewick, 1978) that any competent programmer should be able to implement in fifteen minutes or less.


title: Higher-Order Functional Languages and Intensional Logic

authors:
Panos Rondogiannis
William W. Wadge

abstract: In this paper we demonstrate that a broad class of higher-order functional programs can be transformed into semantically equivalent multidimensional intensional programs that contain only nullary variable definitions. The proposed algorithm systematically eliminates user-defined functions from the source program, by appropriately introducing context manipulation (i.e. intensional) operators. The transformation takes place in M steps, where M is the order of the initial functional program. During each step the order of the program is reduced by one, and the final outcome of the algorithm is an M -dimensional intensional program of order zero. As the resulting intensional code can be executed in a purely tagged-dataflow way, the proposed approach offers a promising new technique for the implementation of higher-order functional languages.


title: Applications of Plotkin-Terms: Partitions and Morphisms for Closed Terms

authors:
Richard Statman
Henk Barendregt

abstract: This theoretical pearl is about the closed term model of pure untyped lambda-terms modulo β-convertibility. A consequence of one of the results is that for arbitrary distinct combinators (closed lambda terms) M , M ′, N , N ′ there is a combinator H such that formula here The general result, which comes from Statman (1998), is that uniformly r.e. partitions of the combinators, such that each ‘block’ is closed under β-conversion, are of the form { H −1 { M }} M ∈Λ Φ . This is proved by making use of the idea behind the so-called Plotkin-terms, originally devised to exhibit some global but non-uniform applicative behaviour. For expository reasons we present the proof below. The following consequences are derived: a characterization of morphisms and a counter-example to the perpendicular lines lemma for β-conversion.


title: Combinators for Program Generation

abstract: We present a general method to transform a compositional specification of a specializer for a functional programming language into a set of combinators that can be used to perform the same specialization more efficiently. The main transformation steps are the transition to higher-order abstract syntax and untagging. All transformation steps are proved correct. The resulting combinators can be implemented in any functional language, typed or untyped, pure or impure. They may also be considered as forming a domain-specific language for meta-programming. We demonstrate the generality of the method by applying it to several specializers of increasing strength. We demonstrate its efficiency by comparing it with a traditional specialization system based on self-application.


title: Compiling lazy functional programs for the Java Virtual Machine

abstract: In this paper, we show how lazy functional programs can be compiled for the Java Virtual Machine using a mapping between a version of the 〈 v , G 〉-machine and the Java Virtual Machine. This mapping is elegant – the description is entirely straightforward – and efficient – using it, both code size and execution speed are of the same order of magnitude as those obtained with a traditional functional language bytecode interpreter. In future, our work could serve as the basis of an interface between Haskell and Java.


title: Lambda terms for natural deduction, sequent calculus and cut elimination

authors:
Henk Barendregt
Silvia Ghilezan

abstract: It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λ N ) and the other to sequent calculus (λ L ). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a ‘cut-free’ fragment (λ L cf ). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms possess a normal form.


title: Domain-free pure type systems

authors:
Gilles Barthe
Morten Heine Sørensen

abstract: Pure type systems make use of domain-full λ-abstractions λx:D.M. We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free λ-abstractions λx.M. Domain-free pure type systems have a number of advantages over both pure type systems and so-called type assignment systems (they also have some disadvantages), and have been used in theoretical developments as well as in implementations of proof-assistants. We study the basic properties of domain-free pure type systems, establish their formal relationship with pure type systems and type assignment systems, and give a number of applications of these correspondences.


title: Type checking dependent (record) types and subtyping

abstract: In this work we put forward an algorithm for the mechanical verification of an extension of Martin-Löf's theory of types with dependent record types and subtyping. We first give a concise description of that theory and motivate its use for the formalization of algebraic constructions. Then we concentrate on the informal explanation and specification of a proof checker that we have implemented. The logical heart of this proof checker is a type checking algorithm for the forms of judgement of a particular formulation of the extended theory which incorporates a notion of parameter. The algorithm has been proven sound with respect to the latter calculus. We include a discussion on that proof in the present work.


title: Program equivalence in a linear functional language

abstract: Researchers have recently proposed that for certain applications it is advantageous to use functional languages whose type systems are based upon linear logic: so-called linear functional languages. In this paper we develop reasoning techniques for programs in a linear functional language, linPCF , based on their operational behaviour. The principal theorem of this paper is to show that contextual equivalence of linPCF programs can be characterised coinductively. This characterisation provides a tractable method for reasoning about contextual equivalence, and is used in three ways: [bull ] A number of useful contextual equivalences between linPCF programs is given. [bull ] A notion of type isomorphism with respect to contextual equivalence, called operational isomorphism, is given. In particular the types !ϕ[otimes ]!ψ and !(ϕ&ψ) are proved to be operationally isomorphic. [bull ] A translation of non-strict PCF into linPCF is shown to be adequate, but not fully abstract, with respect to contextual equivalence.


title: Automatic useless-code elimination for HOT functional programs

authors:
Ferruccio Damiani
Paola Giannini

abstract: In this paper we present two type inference systems for detecting useless-code in higher-order typed functional programs. Type inference can be performed in an efficient and complete way, by reducing it to the solution of a system of constraints. We also give a useless-code elimination algorithm which is based on a combined use of these type inference systems. The main application of the technique is the optimization of programs extracted from proofs in logical frameworks, but it could be used as well in the elimination of useless-code determined by program transformations.


title: Compilation of a specialized functional language for massively parallel computers

authors:
Pascal Fradet
Julien Mallet

abstract: We propose a parallel specialized language that ensures portable and cost-predictable implementations on parallel computers. The language is basically a first-order, recursion-less, strict functional language equipped with a collection of higher-order functions or skeletons. These skeletons apply on (nested) vectors and can be grouped into four classes: computation, reorganization, communication and mask skeletons. The compilation process is described as a series of transformations and analyses leading to SPMD -like functional programs which can be directly translated into real parallel code. The language restrictions enforce a programming discipline whose benefit is to allow a static, symbolic and accurate cost analysis. The parallel cost takes into account both load balancing and communications, and can be statically evaluated even when the actual size of vectors or the number of processors are unknown. It is used to automatically select the best data distribution among a set of standard distributions. Interestingly, this work can be seen as a cross-fertilization between techniques developed within the F ORTRAN parallelization, skeleton and functional programming communities.


title: Do we need dependent types?

authors:
Daniel Fridlender
Mia Indrika

abstract: This pearl is about some functions whose definitions seem to require a language with dependent types. We describe a technique for defining them in Haskell or ML, which are languages without dependent types. Consider, for example, the scheme defining zipWith in figure 1. When this scheme is instantiated with n equal to 1 we obtain the standard function map . In practice, other instances of the scheme are often useful as well. Figure 1 cannot be used as a definition of a function in Haskell because of the ellipses ‘...’. More importantly, the type of zipWith is parameterized by n , which seems to indicate the need for dependent types. However, as mentioned above, Haskell does not allow dependent types.


title: Theoretical Pearl: An adequate and efficient left-associated binary numeral system in the Lambda-calculus

abstract: This paper introduces a sequence of λ-expressions modeling the binary expansion of integers. We derive expressions computing the test for zero, the successor function, and the predecessor function, thereby showing the sequence to be an adequate numeral system, i.e. one in which all recursive functions are lambda-definable. These functions can be computed efficiently; To this end, we introduce a notion of complexity that is independent of the order of evaluation.


title: The lambda-se-calculus does not preserve strong normalisation

abstract: Kamareddine, F., & Ríos (1997) conjecture that the λ s e -calculus preserves the strong normalisation of the λ-calculus. We prove here that this conjecture is false.


title: Girard translation and logical predicates

abstract: We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete . The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this paper can be read as a tutorial on this proof technique for reasoning about relations between type theories.


title: Distributed communication in ML

abstract: We present our experience in implementing a group communication toolkit in Objective Caml, a dialect of the ML family of programming languages. We compare the toolkit both quantitatively and qualitatively to a predecessor toolkit which was implemented in C. Our experience shows that using the high-level abstraction features of ML gives substantial advantages. Some of these features, such as automatic memory management and message marshalling, allowed us to concentrate on those pieces of the implementation which required careful attention in order to achieve good performance. We conclude with a set of suggested changes to ML implementations.


title: Perfect trees and bit-reversal permutations

abstract: One well known algorithm is the Fast Fourier Transform (FFT). An efficient iterative version of the FFT algorithm performs as a first step a bit-reversal permutation of the input list. The bit-reversal permutation swaps elements whose indices have binary representations that are the reverse of each other. Using an amortized approach, this operation can be made to run in linear time on a random-access machine. An intriguing question is whether a linear-time implementation is also feasible on a pointer machine, that is, in a purely functional setting. We show that the answer to this question is in the affirmative. In deriving a solution, we employ several advanced programming language concepts such as nested datatypes, associated fold and unfold operators, rank-2 types and polymorphic recursion.


title: Generalizing generalized tries

abstract: A trie is a search tree scheme that employs the structure of search keys to organize information. Tries were originally devised as a means to represent a collection of records indexed by strings over a fixed alphabet. Based on work by C. P. Wadsworth and others, R. H. Connelly and F. L. Morris generalized the concept to permit indexing by elements built according to an arbitrary signature. Here we go one step further, and define tries and operations on tries generically for arbitrary datatypes of first-order kind, including parameterized and nested datatypes. The derivation employs techniques recently developed in the context of polytypic programming and can be regarded as a comprehensive case study in this new programming paradigm. It is well known that for the implementation of generalized tries, nested datatypes and polymorphic recursion are needed. Implementing tries for first-order kinded datatypes places even greater demands on the type system: it requires rank-2 type signatures and second-order nested datatypes. Despite these requirements, the definition of tries is surprisingly simple, which is mostly due to the framework of polytypic programming.


title: Container types categorically

authors:
Paul F. Hoogendijk
Oege de Moor

abstract: A program derivation is said to be polytypic if some of its parameters are data types. Often these data types are container types, whose elements store data. Polytypic program derivations necessitate a general, non-inductive definition of ‘container (data) type’. Here we propose such a definition: a container type is a relator that has membership. It is shown how this definition implies various other properties that are shared by all container types. In particular, all container types have a unique strength, and all natural transformations between container types are strong.


title: A visualisation of polymorphic type checking

authors:
Yang Jung
Greg Michaelson

abstract: The understanding of polymorphic typechecking and type errors is poorly supported by contemporary functional language implementations. Here, a novel visualisation of functions and their types is presented based on the generation of function specific icons with graphical type representations which change dynamically as functions are applied. This visualisation has been implemented for a Standard ML subset within a graphical environment in which function combinations are constrained by type matching.


title: A modular module system

abstract: A simple implementation of an SML-like module system is presented as a module parameterized by a base language and its type-checker. This implementation is useful both as a detailed tutorial on the Harper–Lillibridge–Leroy module system and its implementation, and as a constructive demonstration of the applicability of that module system to a wide range of programming languages.


title: Server side web scripting in Haskell

abstract: The Common Gateway Interface (CGI) for generating dynamic documents on web servers imposes much accidental complexity on the programmer. The Haskell/CGI library documented in this paper hides all this unpleasantness by using the common sense ‘design pattern’ of separating model and presentation. Low-level query string requests are represented by association lists, and primitive HTTP responses are easily constructed using a set of HTML generating combinators. The CGI programmer only needs to write a worker function that maps an abstract request into an abstract response. A (higher-order) wrapper function then transmutes the worker into a real low-level CGI script that deals with the exact format of concrete requests and responses as required by the CGI standard.


title: Uniform confluence in concurrent computation

abstract: Indeterminism is typical for concurrent computation. If several concurrent actors compete for the same resource then at most one of them may succeed, whereby the choice of the successful actor is indeterministic. As a consequence, the execution of a concurrent program may be nonconfluent. Even worse, most observables (termination, computational result, and time complexity) typically depend on the scheduling of actors created during program execution. This property contrast concurrent programs from purely functional programs. A functional program is uniformly confluent in the sense that all its possible executions coincide modulo reordering of execution steps. In this paper, we investigate concurrent programs that are uniformly confluent and their relation to eager and lazy functional programs. We study uniform confluence in concurrent computation within the applicative core of the π-calculus which is widely used in different models of concurrent programming (with interleaving semantics). In particular, the applicative core of the π-calculus serves as a kernel in foundations of concurrent constraint programming with first-class procedures (as provided by the programming language Oz). We model eager functional programming in the λ-calculus with weak call-by-value reduction and lazy functional programming in the call-by-need λ-calculus with standard reduction. As a measure of time complexity, we count application steps. We encode the λ-calculus with both above reduction strategies into the applicative core of the π-calculus and show that time complexity is preserved. Our correctness proofs employs a new technique based on uniform confluence and simulations. The strength of our technique is illustrated by proving a folk theorem, namely that the call-by-need complexity of a functional program is smaller than its call-by-value complexity.


title: A study of evaluation order semantics in expressions with side effects

authors:
Nikolaos Papaspyrou
Dragan Macos

abstract: The presence of side effects in even a very simple language of expressions gives rise to a number of semantic questions. The issue of evaluation order becomes a crucial one and, unless a specific order is enforced, the language becomes non-deterministic. In this paper we study the denotational semantics of such a language under a variety of possible evaluation strategies, from simpler to more complex, concluding with unspecified evaluation order, unspecified order of side effects and the mechanism of sequence points that is particular to the ANSI C programming language. In doing so, we adopt a dialect of Haskell as a metalanguage, instead of mathematical notation, and use monads and monad transformers to improve modularity. In this way, only small modifications are required for each transition. The result is a better understanding of different evaluation strategies and a unified way of specifying their semantics. Furthermore, a significant step is achieved towards a complete and accurate semantics for ANSI C.


title: Bee: an integrated development environment for the Scheme programming language

abstract: The Bee is an integrated development environment for the Scheme programming language. It provides the user with a connection between Scheme and the C programming language, a symbolic debugger, a profiler, an interpreter, an optimizing compiler that delivers stand alone executables, a source file browser, a project manager, user libraries and online documentation. This article details the facilities of the Bee, its user interface, and presents an overview of the implementation of its main components.


title: Combinators for breadth-first search

abstract: Every functional programmer knows the technique of “replacing failure by a list of successes” (Wadler, 1985), but wise programmers are aware also of the possibility that the list will be empty or (worse) divergent. In fact, the “lists of successes” technique is equivalent to the incomplete depth-first search strategy used in Prolog. At heart, the idea is quite simple: whenever we might want to use a ‘multi-function’ such as ‘ f ’ [ratio ][ratio ] α [Rarr ] β that can return many results or none, we replace it by a genuine function f [ratio ][ratio ] α → β stream that returns a lazy stream of results, and rely on lazy evaluation to compute the answers one at a time, and only as they are needed. For the sake of clarity, I will distinguish between the types of finite lists (α list ) and of potentially infinite, lazy streams (α stream ), though both may be implemented in the same way. Following the conventions used in ML, type constructors follow their argument types.


title: A functional reactive animation of a lift using Fran

abstract: This paper uses the Fran system for functional reactive animation to give a simulation of a lift – or elevator – with many floors. The paper first introduces a two-floor version, and then indicates in detail how this is extended to give a simulation with an arbitrary number of floors and featuring more realistic animated graphics. The paper introduces those aspects of Fran relevant to the simulation, making it a self-contained tutorial on parts of Fran and how it is applied in practice. The full code for the system is available on the World Wide Web.


title: Kleisli, a functional query system

abstract: Kleisli is a modern data integration system that has made a significant impact on bioinformatics data integration. This paper contains a brief introduction to the Kleisli system and an example to illustrate its uses in the bioinformatics arena. The primary query language provided by Kleisli is called CPL, which is a functional query language whose surface syntax is based on the comprehension syntax. Kleisli is itself implemented using the functional language SML. So this paper also describes the influence of functional programming research that benefits the Kleisli system, especially the less obvious ones at the implementation level. Availability. Kleisli has been commercialized under the name “KRIS”. It is available from Kris Technology Inc., 713 Santa Cruz Ave, #2, Menlo Park, CA 94025, USA. Direct email to info@kris-inc.com and web browser to http://www.kris-inc.com .


title: Pipelined functional tree accesses and updates: scheduling, synchronization, caching and coherence

authors:
Andrew J. Bennett
Paul H. J. Kelly
Ross A. Paterson

abstract: This paper is an exploration of the parallel graph reduction approach to parallel functional programming, illustrated by a particular example: pipelined, dynamically-scheduled implementation of search, updates and read-modify-write transactions on an in-store binary search tree. We use program transformation, execution-driven simulation and analytical modelling to expose the maximum potential parallelism, the minimum communication and synchronisation overheads, and to control the overall space requirement. We begin with a lazy functional program specifying a series of transactions on a binary tree, each involving several searches and updates, in a side-effect-free fashion. Transformation of the source code produces a formulation of the program with greater locality and larger grain size than can be achieved using naive parallelization methods, and we show that, with care, these tasks can be scheduled effectively. Even with a workload using random keys, significant spatial locality is found, and we evaluate a modified cache coherency protocol which avoids false sharing so that large cache lines can be used to minimise the number of messages required. As expected with a pipeline, the application should reach a steady state as soon as the first transaction is completed. However, if the network latency is too large, the rate of completion lags behind the rate at which work is admitted, and internal queues grow without bound. We determine the conditions under which this occurs, and show how it can be avoided while maximising speedup.


title: Exceptional Syntax Journal of Functional Programming

authors:
Nick Benton
Andrew Kennedy

abstract: From the points of view of programming pragmatics, rewriting and operational semantics, the syntactic construct used for exception handling in ML-like programming languages, and in much theoretical work on exceptions, has subtly undesirable features. We propose and discuss a more well-behaved construct.


title: Automated complexity analysis of Nuprl extracted programs Journal of Functional Programming

abstract: This paper describes the Automated Complexity Analysis Prototype (ACA p ) system for automated complexity analysis of functional programs synthesized with the Nuprl proof development system. We define a simple abstract cost model for N UPRL 's term language based on the current call-by-name evaluator. The framework uses abstract functions and abstract lists to facilitate reasoning about primitive recursive programs with first-order functions, lazy lists and a subclass of higher-order functions. The ACA p system automatically derives upper bounds on the time complexity of N UPRL extracts relative to a given profiling semantics. Analysis proceeds by abstract interpretation of the extract, where symbolic evaluation rules extend standard evaluation to terms with free variables. Symbolic evaluation of recursive programs generates systems of multi-variable difference equations, which are solved using the M ATHEMATICA computer algebra system. The use of the system is exemplified by analyzing a proof extract that computes the maximum segment sum of a list and a functional program that determines the minimum of a list via sorting. For both results, we compare call-by-name to call-by-value evaluation.


title: Unfolding pointer algorithms

abstract: A fair amount has been written on the subject of reasoning about pointer algorithms. There was a peak about 1980 when everyone seemed to be tackling the formal verification of the Schorr–Waite marking algorithm, including Gries (1979, Morris (1982) and Topor (1979). Bornat (2000) writes: “The Schorr–Waite algorithm is the first mountain that any formalism for pointer aliasing should climb”. Then it went more or less quiet for a while, but in the last few years there has been a resurgence of interest, driven by new ideas in relational algebras (Möeller, 1993), in data refinement Butler (1999), in type theory (Hofmann, 2000; Walker and Morrisett, 2000), in novel kinds of assertion (Reynolds, 2000), and by the demands of mechanised reasoning (Bornat, 2000). Most approaches end up being based in the Floyd–Dijkstra–Hoare tradition with loops and invariant assertions. To be sure, when dealing with any recursively-defined linked structure some declarative notation has to be brought in to specify the problem, but no one to my knowledge has advocated a purely functional approach throughout. Mason (1988) comes close, but his Lisp expressions can be very impure. Möller (1999) also exploits an algebraic approach, and the structure of his paper has much in common with what follows. This pearl explores the possibility of a simple functional approach to pointer manipulation algorithms.


title: Maximum marking problems

abstract: Here are two puzzles for you to solve. First, consider the binary tree in figure 1. Take a pencil (I am assuming that this is your personal copy of JFP!) and mark some of the nodes in such a way that the sum of the values of marked nodes is as large as possible. The catch is that you cannot mark all the nodes: if you mark a node, then you are not allowed to mark its parent. Equivalently, no two marked nodes can be contiguous in the tree. The second puzzle is similar though both the datatype and constraint are different. Consider the rose tree of figure 2 (a rose tree is a tree with arbitrary branching structure). Mark some of the nodes so that all marked nodes are now contiguous in the tree. For example, if you mark the root value 4 and the leaf value 1, then you must also mark the values 5 and −3 along the path from 4 to 1. Again the idea is to maximise the sum of the marked nodes. Of course, if all values were nonnegative, the best solution would be to mark all nodes. But they aren't and the maximum sum is obtained only by a judicious choice of marking. Answers to both puzzles are given at the end of the paper. The Maximum Marking Problem (MMP) is the problem of marking the entries of some given data structure in such a way that a given constraint is satisfied and the sum of the values associated with marked entries is as large as possible. By the end of this pearl, you will be convinced that there is a linear-time solution for both the puzzles described above.


title: Persistent triangulations Journal of Functional Programming

authors:
Guy E. Blelloch
Hal Burch
Karl Crary
Robert Harper
Gary L. Miller
Noel Walkington

abstract: Triangulations of a surface are of fundamental importance in computational geometry, computer graphics, and engineering and scientific simulations. Triangulations are ordinarily represented as mutable graph structures for which both adding and traversing edges take constant time per operation. These representations of triangulations make it difficult to support persistence , including ‘multiple futures’, the ability to use a data structure in several unrelated ways in a given computation; ‘time travel’, the ability to move freely among versions of a data structure; or parallel computation, the ability to operate concurrently on a data structure without interference. We present a purely functional interface and representation of triangulated surfaces, and more generally of simplicial complexes in higher dimensions. In addition to being persistent in the strongest sense, the interface more closely matches the mathematical definition of triangulations (simplicial complexes) than do interfaces based on mutable representations. The representation, however, comes at the cost of requiring O (lg n ) time for traversing or adding triangles (simplices), where n is the number of triangles in the surface. We show both analytically and experimentally that for certain important cases, this extra cost does not seriously affect end-to-end running time. Analytically, we present a new randomized algorithm for 3-dimensional Convex Hull based on our representations for which the running time matches the Ω( n lg n ) lower-bound for the problem. This is achieved by using only O ( n ) traversals of the surface. Experimentally, we present results for both an implementation of the 3-dimensional Convex Hull and for a terrain modeling algorithm, which demonstrate that, although there is some cost to persistence, it seems to be a small constant factor.


title: Algorithms with polynomial interpretation termination proof

authors:
Guillaume Bonfante
Adam Cichon
Jean-Yves Marion
Hélène Touzet

abstract: We study the effect of polynomial interpretation termination proofs of deterministic (resp. non-deterministic) algorithms defined by con uent (resp. non-con uent) rewrite systems over data structures which include strings, lists and trees, and we classify them according to the interpretations of the constructors. This leads to the definition of six function classes which turn out to be exactly the deterministic (resp. non-deterministic) polynomial time, linear exponential time and linear doubly exponential time computable functions when the class is based on con uent (resp. non-con uent) rewrite systems. We also obtain a characterisation of the linear space computable functions. Finally, we demonstrate that functions with exponential interpretation termination proofs are super-elementary.


title: Forms/3: A first-order visual language to explore the boundaries of the spreadsheet paradigm

authors:
Margaret M. Burnett
John Atwood
Rebecca Walpole Djang
James Reichwein
Herkimer J. Gottfried
Sherry Yang

abstract: Although detractors of functional programming sometimes claim that functional programming is too difficult or counter-intuitive for most programmers to understand and use, evidence to the contrary can be found by looking at the popularity of spreadsheets. The spreadsheet paradigm, a first-order subset of the functional programming paradigm, has found wide acceptance among both programmers and end users. Still, there are many limitations with most spreadsheet systems. In this paper, we discuss language features that eliminate several of these limitations without deviating from the first-order, declarative evaluation model. The language used to illustrate these features is a research language called Forms/3. Using Forms/3, we show that procedural abstraction, data abstraction and graphics output can be supported in the spreadsheet paradigm. We show that, with the addition of a simple model of time, animated output and GUI I/O also become viable. To demonstrate generality, we also present an animated Turing machine simulator programmed using these features. Throughout the paper, we combine our discussion of the programming language characteristics with how the language features prototyped in Forms/3 relate to what is known about human effectiveness in programming.


title: A predicative approach to the classification problem

authors:
Salvatore Caporaso
Emanuele Covino
Giovanni Pani

abstract: We harmonize many time-complexity classes DTIMEF ( f ( n )) ( f ( n ) [ges ] n ) with the PR functions (at and above the elementary level) in a transfinite hierarchy of classes of functions [Tscr ] α . Class [Tscr ] α is obtained by means of unlimited operators, namely: a variant Π of the predicative or safe recursion scheme, introduced by Leivant, and by Bellantoni and Cook, if α is a successor; and constructive diagonalization if α is a limit. Substitution ( SBST ) is discarded because the time complexity classes are not closed under this scheme. [Tscr ] α is a structure for the PR functions finer than [Escr ] α , to the point that we have [Tscr ] ε 0 = [Escr ] 3 (elementary functions). Although no explicit use is made of hierarchy functions, it is proved that f ( n ) ∈ [Tscr ] α implies f ( n ) [les ] n G α ( n ) , where G α belongs to the slow growing hierarchy (of functions) studied, in particular, by Girard and Wainer.


title: Normalization by evaluation with typed abstract syntax

authors:
Olivier Danvy
Morten Rhiger
Kristoffer Høgsbro Rose

abstract: In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers and addition, but only in this section.


title: Inductive graphs and functional graph algorithms

abstract: We propose a new style of writing graph algorithms in functional languages which is based on an alternative view of graphs as inductively defined data types. We show how this graph model can be implemented efficiently, and then we demonstrate how graph algorithms can be succinctly given by recursive function definitions based on the inductive graph view. We also regard this as a contribution to the teaching of algorithms and data structures in functional languages since we can use the functional-style graph algorithms instead of the imperative algorithms that are dominant today.


title: Manufacturing datatypes

abstract: This article describes a general framework for designing purely functional datatypes that automatically satisfy given size or structural constraints. Using the framework we develop implementations of different matrix types (for example, square matrices) and implementations of several tree types (for example, Braun trees and 2-3 trees). Consider representing square n × n matrices. The usual representation using lists of lists fails to meet the structural constraints: there is no way to ensure that the outer list and the inner lists have the same length. The main idea of our approach is to solve in a first step a related, but simpler problem, namely to generate the multiset of all square numbers. To describe this multiset we employ recursion equations involving finite multisets, multiset union, addition and multiplication lifted to multisets. In a second step we mechanically derive from these recursion equations datatype definitions that enforce the ‘squareness’ constraint. The transformation makes essential use of parameterized types.