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

[ajb at spamcop.net]

G'day all.

(Moving the discussion to haskell-cafe.)

Quoting oleg at 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