Difference between revisions of "Burton-style nondeterminism"

From HaskellWiki
Jump to: navigation, search
m (Correccted Hancock-style interface >_<)
(Superfluous sections relocated)
 
Line 1: Line 1:
[[Category:Code]]
 
[[Category:Nondeterminism]]
 
 
 
== Introduction ==
 
== Introduction ==
   
Line 48: Line 45:
 
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 <code>Decision</code> values.
 
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 <code>Decision</code> values.
   
== Extra parameters and arguments ==
 
 
[[Category:Code]]
 
 
[[Category:Nondeterminism]]
While they acknowledge Burton's technique does maintain referential transparency, in their paper [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.49.695&rep=rep1&type=pdf 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 <code>Prelude</code> for Haskell. Using the [https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/bang-patterns.html bang-patterns] extension:
 
 
<haskell>
 
instance Monad ((->) (Tree a)) where
 
return x = \_ -> x
 
m >>= k = \t -> case m (left t) of !x -> f x (right t)
 
</haskell>
 
 
making use of the fact that the partially-applied function type <code>forall a . (->) a</code> is monadic.
 
 
== Further developments ==
 
 
In Simon Peyton Jones's book [[Books|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 <tt>tvname</tt>) for a type checker, using the type <tt>name_supply</tt>:
 
 
<blockquote><tt>
 
next_name :: name_supply -> tvname<br>
 
deplete :: name_supply -> name_supply<br>
 
split :: name_supply -> (name_supply, name_supply)<br>
 
</tt></blockquote>
 
 
A similar interface is easily obtained from Burton's:
 
 
<haskell>
 
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)
 
</haskell>
 
 
which can still be supported if needed:
 
 
<haskell>
 
left, right :: Tree a -> Tree a
 
left = fst . subtrees
 
right = snd . subtrees
 
</haskell>
 
 
This change also simplifies the monad instance:
 
 
<haskell>
 
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
 
</haskell>
 
 
== The end of trees ==
 
 
This new nondeterminism interface:
 
 
<haskell>
 
-- decision-value ADT
 
data Decision
 
choice :: Decision -> a -> a -> a
 
 
contents :: Tree Decision -> Decision
 
subtrees :: Tree Decision -> (Tree Decision, Tree Decision)
 
</haskell>
 
 
can be further simplified with a suitable type synonym:
 
 
<haskell>
 
type Decisor = Tree Decision
 
 
contents :: Decisor -> Decision
 
subtrees :: Decisor -> (Decisor, Decisor)
 
</haskell>
 
 
and some name changes:
 
 
<haskell>
 
consult :: Decisor -> Decision
 
eschew :: Decisor -> (Decisor, Decisor)
 
</haskell>
 
 
to the point of being an ADT in and of itself:
 
 
<haskell>
 
data Decisor -- abtract, possibly builtin
 
consult :: Decisor -> Decision
 
eschew :: Decisor -> (Decisor, Decisor)
 
</haskell>
 
 
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.
 
 
   
[[User:Atravers|Atravers]] 14:17, 10 March 2021 (UTC)
+
<!-- [[User:Atravers|Atravers]] 14:17, 10 March 2021 (UTC) -->

Latest revision as of 11:57, 27 March 2021

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.