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.