[m-dev.] Suggestion for a new "where" operator

[Fergus Henderson]

On 05-Aug-2003, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> On Mon, Aug 04, 2003 at 05:36:54PM +1000, Peter Moulder wrote:
> >   - Interactions with `not', especially "hidden" not's such as with
> >     `\='.  One needs to know that the extra goals come inside the scope
> >     of that `not'.  I feel this leads to counter-intuitive behaviour of
> >     `=' vs `\=' when the inserted goals can fail.
> 
> OK, this requires care.  Take 3 \= (X where p(3, X)) when p(in,out)
> is semidet.  This could sensibly mean:
> 
> 	p(3, X),
> 	3 \= X
> 
> or
> 
> 	\+ p(3, 3)
> 
> But this must have already been addressed for handling semidet
> functions.  It should be handled however Mercury handles
> 
> 	3 \= p(3)
> 
> when p/1 is a semidet function.

`<Expr1> \= <Expr2>' is defined to be an abbreviation for
`not (<Expr1> = <Expr2>)'.  This is regardless of whether
<Expr2> contains `where' expressions or semidet functions
or anything else.  So the second interpretation is the correct one.

> >   - If the inserted goals can fail or produce multiple solutions, then
> >     EXPR = EXPR can fail.  (IIRC, one reason that Mercury doesn't
> >     support multi/nondet functions was to avoid cases where EXPR = EXPR
> >     fails.)
> 
> How can EXPR = EXPR fail?

Yes, that's not the reason why Mercury doesn't support multi/nondet functions.
The reason is that if functions were allowed to be nondet in their forwards
mode, `X = f, p(X, X)' could mean something different than `p(f, f)'.

> Alright, so require (... where ...)  to have at most 1 solution.
> That's in keeping with the idea that (... where ...) is a functional
> form that behaves the way function application behaves.

Yes, I agree.  Although the requirement should be the same as for functions:
it should only be prevented from having more than one solution in
the forwards mode (the one in which the result of the where expression
has an output mode and all of the other non-local variables have an
input mode).  If some of the non-local variables other than
those in the result have output modes, it should be OK for the where
expression to be nondeterministic.

This determinism requirement is necessary for consistency with the way
we treat functions.  Unfortunately, however, it will make the proposal
a bit more difficult to implement.  In particular, we will need to keep
track in the HLDS of which goals came from a `where' expression, so that
determinism analysis can check their determinism.

That in turn also means that we should not allow mode reordering to
break up where expressions.

> >   - The order of the goals can be significant (e.g. performance, or
> >     completeness guarantees with fully-strict), yet it isn't always
> >     obvious what the order will be.  Unlike `@' and function calls,
> >     `where' presumably allows state variable transformations, where
> >     mistakes in understood ordering affect program logic.
> 
> Good point.  Best not allow state variables in where expressions,
> again in keeping with the (... where ...) is a functional form
> principle.

For the purposes of state variables, I think we should treat a where
expression `<Expr> where <Goal>' the same way as a function call with
a lambda expression, `<Expr> = f((pred) is semidet :- <Goal>)'.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------