Erratic Fudgets:

A Semantic Theory for an Embedded Coordination Language

Andrew Moran       David Sands       Magnus Carlsson



Abstract

The powerful abstraction mechanisms of functional programming languages provide the means to develop domain-specific programming languages within the language itself. Typically, this is realised by designing a set of combinators (higher-order reusable programs) for an application area, and by constructing individual applications by combining and coordinating individual combinators. This paper is concerned with a successful example of such an embedded programming language, namely Fudgets, a library of combinators for building graphical user interfaces in the lazy functional language Haskell. The Fudget library has been used to build a number of substantial applications, including a web browser and a proof editor interface to a proof checker for constructive type theory. This paper develops a semantic theory for the non-deterministic stream processors that are at the heart of the Fudget concept. The interaction of two features of stream processors makes the development of such a semantic theory problematic:

We demonstrate that this combination of features in a higher-order functional language can be tamed to provide a tractable semantics theory and induction principles suitable for reasoning about contextual equivalence of Fudgets.

To appear at COORDINATION '99.

Paper available in PS and DVI (the DVI version lacks some figures).