[mercury-users] disadvantage of not using "any" mode?

[Fergus Henderson]

On 22-Oct-2003, Aditya Raj PATHANIA <adityarp at students.cs.mu.OZ.AU> wrote:
> 
> > The most important point is that for constrained variables, you should
> > use the inst "any".
> 
> i wanted to know if this is critical

The short answer is yes.

The slightly longer answer is yes, unless you are extremely careful and
know a lot about how the Mercury implementation works -- but in that case
the care required is probably much more work than using "any" insts, so
you're still better off using "any" insts.

If you don't use "any" insts for constrained variables, then you are
lying to the compiler, and it will eventually get its revenge.
To see how, read the description below of what can go wrong in label/1
if you don't use an "any" inst.

> :- solver type indexical_var
>    ---> indexical_var(c_pointer).
> 
> :- pred min(indexical_var,int).
> :- mode min(in,out) is det.
> :- pred max(indexical_var,int).
> :- mode max(in,out) is det.

Presumably these predicates return the current minimum/maximum value
for your indexical variables?

If so, those two predicates should be declared impure,
or given determinism `cc_multi'.

To see why, consider the goal

	min(X, Min),
	X `gt` 42

and the same goal re-ordered:

	X `gt` 42,
	min(X, Min)

These two should be logically equivalent, but for the second one
we will definitely get Min >= 43, whereas for the first one we
might get e.g. Min = 0.

> :- pred leq(indexical_var,int).
> :- mode leq(in,in) is nondet.
> :- pred gt(indexical_var,int).
> :- mode gt(in,in) is nondet.

"is nondet" won't work here -- since all arguments have mode "in",
the compiler will prune away any solutions after the first one.

> :- pred label(indexical_var,int,list(indexical_var),list(indexical_var)).
> :- mode label(in,in,in,out) is nondet.
> :- pragma promise_pure(label/4).
> 
> label(V,Min,Vs0,Vs) :-
> 		(
> 		  leq(V,Min),
> 		  list__append([V],Vs0,NVs0),
> 		  list__append([V],Vs,NVs),
> 		  labeling(NVs0,NVs)
> 		;
> 		  gt(V,Min),
> 		  list__append([V],Vs0,NVs0),
> 		  list__append([V],Vs,NVs),
> 		  labeling(NVs0,NVs)
> 		).

The last three lines of that disjunction is the same for both
branches, so you can make the code simpler by doing some common
subexpression elimination:

	label(V,Min,Vs0,Vs) :-
		(
			leq(V,Min)
		;
			gt(V,Min)
		),
 		list__append([V],Vs0,NVs0),
 		list__append([V],Vs,NVs),
 		labeling(NVs0,NVs).

The compiler might perform such a transformation as part of its
optimizations.

Next, consider the disjunction that remains after this transformation.
If you don't use `any' insts, then this disjunction has no output
variables.  So the compiler can assume that it has at most one solution!
That is, if the call to leq/2 succeeds, the compiler can optimize away
the call to gt/2.  This is obviously not what you want.  The problem
is that you lied to the compiler (in the mode declarations for procedures
implemented using the C interface), and it may make an optimization based on
the assumption that your declarations were true, and this optimization may
therefore break your program.

P.S.
There's no need to call list__append here.
You can just use unification:

	label(V, Min, Vs0, Vs) :-
		(
			leq(V, Min)
		;
			gt(V, Min)
		),
		labeling([V | Vs0], [V | Vs]).

-- 
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-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------