1,066 papers · page 46 of 54
A major problem for writing extensible software arises when recursively defined datatypes and operations on these types have to be extended simultaneously without modifying existing code. This paper introduces Extensible Algebraic Datatypes with defaults, which promote a simple p…
We present an operational semantics for parallel lazy evaluation that accurately models the parallel behaviour of the non-strict parallel functional language GpH. Parallelism is modelled synchronously, that is, single reductions are carried out separately then combined before pro…
This paper generalises the flattening transformation - a technique for the efficient implementation of nested data parallelism - and reconciles it with main stream functional programming. Nested data parallelism is significantly more expressive and convenient to use than the flat…
We describe an efficient technique for incorporating Baker's incremental garbage collection algorithm into the Spineless Tagless G-machine on stock hardware. This algorithm eliminates the stop/go execution associated with bulk copying collection algorithms, allowing the system to…
Quick Check is a tool which aids the Haskell programmer in formulating and testing properties of programs. Properties are described as Haskell functions, and can be automatically tested on random input, but it is also possible to define custom test data generators. We present a n…
I present a type-preserving translation that eliminates subtyping and bounded quantification without introducing any run-time costs. This translation is based on Mitchell and Pierce's encoding of bounded quantification using intersection types. I show that, previous negative obse…
We present the μ -calculus, a syntax for λ-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus LK, a key classical logical system in proof theory. Under t…
We show that a non-duplicating CPS transformation has no effect on control-flow analysis and that it has a positive effect on binding-time analysis: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, and a monovaria…
We show that standard formulations of intersection type systems are unsound in the presence of computational effects, and propose a solution similar to the value restriction for polymorphism adopted in the revised definition of Standard ML. It differs in that it is not tied to le…
Monads have become a popular tool for dealing with computational effects in Haskell for two significant reasons: equational reasoning is retained even in the presence of effects; and program modularity is enhanced by hiding "plumbing" issues inside the monadic infrastructure. Unf…
Cheap eagerness is an optimization where cheap and safe expressions are evaluated before it is known that their values are needed. Many compilers for lazy functional languages implement this optimization, but they are limited by a lack of information about the global flow of cont…
Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler declarative specifications is not widely understood, due in part to the difficulty…
The past three decades have seen a plethora of language features for large-scale software composition. Some of these are fairly simple, others quite sophisticated. Each embodies an implicit claim that its particular combination of features is both necessary and sufficient for som…
In a paper about pretty printing J. Hughes introduced two fundamental techniques for deriving programs from their specification, where a specification consists of a signature and properties that the operations of the signature are required to satisfy. Briefly, the first technique…
We propose regular expression types as a foundation for XML processing languages. Regular expression types are a natural generalization of Document Type Definitions (DTDs), describing structures in XML documents using regular expression operators (i.e., *, ?, |, etc.) and support…
Financial and insurance contracts do not sound like promising territory for functional programming and formal semantics, but in fact we have discovered that insights from programming languages bear directly on the complex subject of describing and valuing a large class of contrac…
This paper describes FC++: a rich library supporting functional programming in C++. Prior approaches to encoding higher order functions in C++ have suffered with respect to polymorphic functions from either lack of expressiveness or high complexity. In contrast, FC++ offers full …
Every programmer has blind spots. Breadth-first numbering is an interesting toy problem that exposes a blind spot common to many---perhaps most---functional programmers.
This paper shows how to systematically extend an arbitrary type system with dependency information, and how soundness and non-interference proofs for the new system may rely upon, rather than duplicate, the soundness proof of the original system. This allows enriching virtually a…
While developing the software of a browser-operated educational CD-ROM, we had to face a number of problems. This paper presents these problems and the solutions we found. Amusingly, most of our solutions rely on continuations. Are browsers and multimedia the future of continuati…