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:
| (i) |
the sharing of computation provided by the lazy evaluation mechanism of the underlying host language, and
|
| (ii) |
the addition of non-deterministic choice needed to handle the natural concurrency that reactive applications entail.
|
We demonstrate that this combination of features in a higher-order functional language can be tamed to provide a tractable
semantic theory and induction principles suitable for reasoning about contextual equivalence of Fudgets.