Burton-style nondeterminism

Introduction

In his paper Nondeterminism with Referential Transparency in Functional Programming Languages, F. Warren Burton describes a way to add nondeterminism arising from the ordering of external events to a functional language. Burton's technique uses abstract values contained in an (theoretically) infinite structured value (which Burton simply refers to as pseudodata).

Definitions

For the structured values, Burton defines a tree type:

data Tree a = Node { contents :: a,
                     left     :: Tree a,
                     right    :: Tree a  }

to convey the abstract values of type Decision.

A program would receive an initial tree-of-decisions as a parameter. Using left and right, subtrees would be dispersed throughout the program (again as arguments) as needed, to eventually be used with contents to retrieve the abstract Decisions for use by choice:

choice :: Decision -> a -> a -> a

which is the only operation available in the Decision ADT.

Referential transparency?

Burton states how this technique preserves referential transparency on page 2:

In practice these values will be determined at run time (when used as arguments to a special function choice), but once fixed will never change.

From this we can make two observations:

• The effects involved in determining a Decision value only occur once: when it is initially used;

• Once it has been determined, a Decision value won't change: it remains constant, even if reused.

When looked at in this way, Burton's technique has a striking resemblance to lazy evaluation:

• the evaluation of a thunk (suspended expression) only occurs when it is initially used;

• once its result has been determined, it won't change: it replaces the original thunk.

The practical difference between Burton's technique and lazy evaluation is that (some of) the effects involved in the former are visible outside functional programs which use Decision values.