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 preserves referential transparency through the use of 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?

How this technique preserves referential transparency is briefly mentioned at the start of page 2 of Burton's paper:

[...] 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.

Extra parameters and arguments

While they acknowledge Burton's technique does maintain referential transparency, in their paper On the Expressiveness of Purely Functional I/O Systems Paul Hudak and Raman S. Sundaresh also raise one possible annoyance - the need to manually disperse subtrees as additional arguments or parameters within programs.

As it happened, the first hints of a solution was already present when Burton's paper was first published, and now forms part of the standard Prelude for Haskell. Using the bang-patterns extension:

instance Monad ((->) (Tree a)) where
    return x = \_ -> x
    m >>= k  = \t -> case m (left t) of !x -> f x (right t)

making use of the fact that the partially-applied function type forall a . (->) a is monadic.

Further developments

In Simon Peyton Jones's book The implementation of functional programming languages (section 9.6 on page 188 of 458), Peter Hancock provides a simple interface for generating new type varibles (of type tvname) for a type checker, using the type name_supply:

next_name :: name_supply -> tvname
deplete :: name_supply -> name_supply
split :: name_supply -> (name_supply, name_supply)

A similar interface is easily obtained from Burton's:

data Tree a = Node a (Tree a) (Tree a)

contents :: Tree a -> a
subtrees :: Tree a -> (Tree a, Tree a)

contents (Node x _   _) = x
subtrees (Node _ t1 t2) = (t1, t2)

which can still be supported if needed:

left, right :: Tree a -> Tree a
left  = fst . subtrees
right = snd . subtrees

This change also simplifies the monad instance:

instance Monad ((->) (Tree a)) where
    return x = \_ -> x
    m >>= k  = \t -> let !(t1, t2) = subtrees t in
                     let !x        = m t1 in
                     f x t2

The end of trees

This new nondeterminism interface:

 -- decision-value ADT
data Decision 
choice :: Decision -> a -> a -> a

contents :: Tree Decision -> Decision
subtrees :: Tree Decision -> (Tree Decision, Tree Decision)

can be further simplified with a suitable type synonym:

type Decisor = Tree Decision

contents :: Decisor -> Decision
subtrees :: Decisor -> (Decisor, Decisor)

and some name changes:

consult  :: Decisor -> Decision
eschew   :: Decisor -> (Decisor, Decisor)

to the point of being an ADT in and of itself:

data Decisor  -- abtract, possibly builtin
consult  :: Decisor -> Decision
eschew   :: Decisor -> (Decisor, Decisor)

The choice to use trees has been reduced to an implementation detail, oblivious to those using this interface - its behaviour just needs to stay consistent with the original interface as described by Burton.

Atravers 14:17, 10 March 2021 (UTC)