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 Decision
s 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.