Re: [Haskell] Re: A MonadPlusT with fair operations and pruning
G'day all. (Moving the discussion to haskell-cafe.) Quoting oleg@pobox.com:
The last statement should probably be `return (otherState w,b')', right?
Yes, I think so.
mif (mif c t' e') t e translates to
((X=1 ; X=2) *-> X=1 ; fail) *-> true; true.
Using the predicate: test(X) :- ( ( ( X = 1 ; X = 2 ) *-> X = 1 ; fail ) *-> true ; true ). Testing it with SWI-Prolog gives me: ?- test(X). X = 1 ; No and: ?- X = 2, test(X). X = 2 ; No and: ?- X = 3, test(X). X = 3 ; No The problem is that soft cut isn't a logical construct unless the program is well-moded. Using Mercury with the above code plus the following declarations: :- pred test(int). :- mode test(in) is semidet. :- mode test(out) is nondet. gives one appropriate answer: the "in" mode succeeds on all integers, but the "out" mode doesn't compile since X isn't bound inside the predicate. Another appropriate answer is the NU-Prolog approach, which suspends negations until they are appropriately bound. I haven't tested it, but NU-Prolog _should_ do the equivalent of this: ?- test(X). X = 1 ; X = X ; No (Read this as "X can be either 1 or anything".) You can also get an appropriate answer if your Prolog supports constraint programming, and you prime X before calling test/1. I also haven't tested this. Now Haskell programs are always well-moded, so let's see if it's an issue here. The "in" mode looks something like this: test_in :: Int -> Logic () test_in x = mif (mif (guard (x == 1) `mplus` guard (x == 2)) (\_ -> guard (x == 1)) mfail ) (\_ -> mtrue) mtrue This succeeds for all values of x. The "out" mode looks like this: test_out :: Logic Int test_out x = mif (mif (return 1 `mplus` return 2) (\_ -> guard (x == 1)) mfail ) (\x -> return x) ??? What to replace "???" with is left as an exercise for the reader. By the way, the moral of this story is that despite both being declarative, functional programming is much, much simpler than logic programming because the dataflow is simpler. In summary, I think that whether the extra law is needed or not depends on how logical your logic variables are.
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.
I think you need it if you're deriving using the John Hughes method. If you didn't need it, all the better for you. Cheers, Andrew Bromage
Regarding the law of mif (aka ifte, aka soft-cut, aka logical conditional) mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e) You're right of course: mode matters for the predicates that involve negation, such as mif. However, I believe that the mode is orthogonal to the discussion of the mif law. The following is a better example. Again we will be using Prolog (with the built-in soft-cut). This time, we eschew any variable binding within our conditionals, in fact, any variables at all. Truth and failure is all we need. We chose c === (true; true), t' === e' === fail, t === e === true. Thus, mif (mif c t' e') t e translates to {X =1 is there so that Prolog will print something} X = 1, (((true; true) *-> fail; fail) *-> true; true). and returns one answer, 1. mif c (\x -> mif (t' x) t e) (mif e' t e) translates to X = 1, ((true; true) *-> (fail *-> true; true) ; (fail *-> true; true)). and returns two answers, 1 and 1. Indeed, using the semantics of the soft cut, we find that the first translation reduces to X = 1, true. whereas the second one reduces to X = 1, (true; true)
G'day all. Quoting oleg@pobox.com:
We chose c === (true; true), t' === e' === fail, t === e === true. Thus,
Good point. It becomes even more obvious when you have a monad transformer. If e === (lift m), then this:
mif (mif c t' e') t e
translates to (lift m), but this:
mif c (\x -> mif (t' x) t e) (mif e' t e)
translates to lift m `mplus` lift m, which is definitely different, since m may alter the transformed monad. Cheers, Andrew Bromage
participants (2)
-
ajb＠spamcop.net -
oleg＠pobox.com