Difference between revisions of "Burton-style nondeterminism"

Introduction

In his paper Nondeterminism with Referential Transparency in Functional Programming Languages, F. Warren Burton describes a way to add nondeterminism to a functional language which preserves referential transparency through the use of abstract values contained in an (theroetically) 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?

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

Inspired by the functional pearl On generating unique names by Lennart Augustsson, Mikael Rittri and Dan Synek, we can simplify the original interface as presented by Burton:

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

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

contents (Node x _   _) = a
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)