[mercury-users] Hi, and determinism

[Fergus Henderson]

On 28-Jan-2001, Dan Sheppard <dans at chiark.greenend.org.uk> wrote:
> 
> Now I come to my most common two runtime
> programming errors in mercury. Both take place in semidet
> predicates. In most cases where one variable is accidentally used in
> the place of another this is caught by the compiler, either through
> the strict and flexible type-system, or through attempts to unify two
> possibly-unequal ground variables in a det predicate. However, in a
> semidet predicate, the possibility exists of silent failable
> unifications.

The technique that Tom mentioned helps reduce the frequency of such
problems.  But you have to remember to use it!
One of these cases bit us in the ICFP competition last year.
We had some code

	:- pred inside_sphere(point, trans).
	:- mode inside_sphere(in, in) is semidet.

	inside_sphere(Point, Trans) :-
		Point = point_to_object_space(Trans, Point),
		mag2(Point) =< 1.0.

which should have been

	inside_sphere(Point0, Trans) :-
		Point = point_to_object_space(Trans, Point0),
		mag2(Point) =< 1.0.

If we'd had more time, we probably would have used different types for
the two different coordinate types (world space coordinates and object
space coordinates), instead of using a single `point' type, and then the
type checker would have caught this one.

Also, if we'd use the return-a-bool style, we might written that as

	:- func inside_sphere(point, trans) = bool.
	inside_sphere(Point, Trans) = Result :-
		Point = point_to_object_space(Trans, Point),
		Result = (if mag2(Point) =< 1.0 then yes else no).
		
and then the determinism checker would have caught it.

But in the haste of the competition, we didn't do either of those, and
instead spent a surprising amount of time trying to find this problem.

I think it might be a good idea for us to allow `==' as a synonym for `=',
and add an option to the compiler which warns about all semidet unifications
which are not written using `=='.  If that works well in practice, we could
make that behaviour the default.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  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
--------------------------------------------------------------------------