[Haskell-cafe] How to implement `amb' operator?

[Andy Moran]

[ Was sent only to participants, but I meant to send it to the list ]

On Wednesday 07 April 2004 06:04 am, Brandon Michael Moore wrote:

> Keith is talking about a "comitted choice" style of nondeterminism, where
> one of the arguments is picked and the computation continues from there.
>
> If you want a computation with backtracking, or a list of all possibly
> results then you should use the list monad, or another monad that
> supports nondetermanism.

An important feature of amb is known as "bottom-avoidance", and you can get
that with Keith's scheme (although it won't be terribly fair; see mailing
list discussions about the fairness or lack thereof of the GHC RTS
scheduler), but you can't get it with backtracking (indeed, backtracking is
entirely deterministic).

Of course, Keith's scheme forces you to work within the IO monad, as well
 it should.  If we allowed amb to have the type

   amb :: a -> a -> a

then all of the transformations carried out within GHC's mid-stage would
need to be re-examined for their correctness (in the context of a semantics
that understood sharing, as non-determinism makes sharing observable).
It's possible that many would still be valid, but it's by no means clear.
To my knowledge, no-one has developed a correct semantics for sharing and
amb that enables proof of simple transformations like let-floating or
lambda-floating or even call-by-need beta reduction, let alone some of the
more complex ones like deforestation (which requires a theory that can
handle recursion well).

Cheers,

Andy

--
Andy Moran                                         Ph. (503) 626 6616, x113
Galois Connections Inc.                                 Fax. (503) 350 0833
12725 SW Millikan Way, Suite #290                     http://www.galois.com
Beaverton, OR 97005                                        moran at galois.com