[Haskell] Re: A MonadPlusT with fair operations and pruning

[oleg at pobox.com]

on Jun 22 Andrew Bromage wrote about the usefulness of 
soft-cuts and "don't care" non-determinism in non-deterministic
computations in Haskell.
> http://www.haskell.org/pipermail/haskell/2005-June/016037.html

Thank you very much for your explanation, it was helpful indeed. You
noted, 
> Some of the interesting examples in Prolog are moot in Haskell by virtue
> of the fact that Haskell is "strongly moded"

And hence was our quandary. Even the leanTAP theorem prover looked too
simple in Haskell to serve as a good example of advanced
non-determinism. Your Tic-Tac-Toe example is thus even more
appreciated. We have extended your code to boards of arbitrary NxN
size (with M consecutive marks needed for winning). There is also a
function for a human to play against the machine. We added some limits
on the breadth and the depth of the search -- to keep both the
reasonable response time and the pride. All in all, playing on the 5x5
board (with 4 marks needed for winning) is fairly entertaining. The
archive LogicT.tar.gz mentioned previously now contains the
tic-tac-toe code. The paper has been updated with its description.

BTW,
> best p b
...
>     | otherwise
>         = ifte (once (do
>             m <- choose [1..9]
>             b' <- move m p b
>             guard (win p b)
>             return (Win, b')))
>           return
>           return
>             (ifte (once (do
>                     m <- choose [1..9]
>                     b' <- move m (otherPlayer p) b
>                     guard (win (otherPlayer p) b')
>                     return m))
>              (\m -> do
>                 b' <- move m p b
>                 (w,_) <- best (otherPlayer p) b'
>                 return (w,b'))

The last statement should probably be `return (otherState w,b')',
right?

on Jan 5 2005, Andrew Bromage wrote on Haskell-Cafe:

> Logical if-then-else has this signature:
>
>     mif :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b
>
> Intuitively, this takes three arguments: the "condition", the "then"
> case and the "else" case.  This obeys the "obvious" laws of if-then-else:
>
>     mif (return a) t e = t a
>     mif (mzero) t e = e
>     mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e)

Chung-chieh Shan has pointed out a problem with the last law: Let us
consider the following instance of that law. We use Prolog, which
implements soft-cuts (aka mif aka ifte) natively. In Prolog, 
`mif test t e' is written as `test *-> t ; e' 
He chose t === true, e === true, e' === fail, t' === X = 1, 
c === (X=1 ; X=2)

mif (mif c t' e') t e 
 translates to

((X=1 ; X=2) *-> X=1 ; fail) *-> true; true.

and gives one answer, 1.

mif c (\x -> mif (t' x) t e) (mif e' t e)
 translates to

(X=1 ; X=2) *-> ( X=1 *-> true ; true) ; (fail *-> true; true).

and gives two answers, 1 and 2.

So, it seems the law has to be formulated in a more complex way,

 mif (mif c t' e') t e = 
   mif (once c) (const $ mif (c >>= t') t e) (mif e' t e)

with a surprising occurrence of `once'. That formulation isn't
particularly useful for a backtracking _transformer_. In any case, we
haven't encountered a need to simplify "mif (mif c t' e') t e"
algebraically. It is interesting to see when such a law may be
required.