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

[oleg at pobox.com]

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)