[mercury-users] Hi, and determinism

[Dan Sheppard]

Hello. I'm a PhD student using mercury in anger in my project on an
entirely un-programming-language-related area. Currently I've about
5000 lines or so of code. I've just joined the list, so excuse me if
the following has been discussed before. I think the problem is real,
but I can't myself think of a solution.

People who disliked Prolog used to criticise its propensity to say
"no" when anything whatever was wrong, or to unexpecetdly produce a
vast array of solutions differing only in (say) some irrelevent list
ordering. This trick it had of being unexpectedly non-deterministic,
in mercury terminology either being semidet when it appeared det, or
nondet when it appeared det or semidet would be confusing and annoying
to programmers.

One of the wonderful things about mercury is the way you can nail down
what you want the determinism to be, and it will that check this is
achieved. No doubt this is useful for compiler optimisations and the
like but, most importantly for me, it means that there's guaranteed to
be no creeping nondeterminism where it shouldn't be.

Now out of all the modes available to a mercury programmer, two are by
far the most common, det and semidet. Others, almost always nondet,
multi, or cc_*, are used sparingly and carefully, often in prototyping
or particular solution-seeking predicates, surrounded by a soulutions
or aggregate, or in a semidet with only `in' variables.

What remains is a vast body of code which is mainly det, but also much
of which is semidet. 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.

Secondly, consider the following, where data is some datatype which is
being modified by calls to data_modify.

:- pred data_modify(T::in,data(T)::in,data(T)::out) is semidet.

:- pred correct(list(T)::in,data(T)::in,data(T)::out) is semidet.
correct([],X,X). % This is the base case for the iteration
correct([H|T],Ba,Bc) :-
	data_modify(H,Ba,Bb),
	correct(T,Bb,Bc).

Now in this example things can be solved by using unique modes, or DCG
predicates, but it's easy to think of problems where this is not the
case, and I'm trying to keep things simple. Now correct `itself' is
det, it can only fail if data_modify fails, it propogates failures but
does not `generate' them itself. Now imagine I'd forgotten the base
case for the iteration (the line with the comment on it). Now correct
could (in fact always would) fail. This would be detected if I could
have declared correct as det.

Now it seems kind of mean that this kind of error can be detected at
compile time if "correct" calls only-det things (meaning it can be
declared det) but not if it calls semidet things (meaning it must be
semidet) despite the predicate itself being of the same structure.

What I'm after is some kind of new mode, which means det unless any
particular identified semidet things it evaluates fail. Failure
because data_modify fails, but not because correct has no term for the
base case. Perhaps it could be indicated by the programmer in some way
what is expected to fail within a predicate. I'm not sure if this
could be meaningfully done, it would be interesting to find out from
the more language-design inclined of you. (I can see many problems
with this idea, but there might be known solutions to them).

I try to avoid cascades of semidet predicates for these two reason
(which are really a minor recurrance of the prolog "no" problem), I
wonder if there's some other way of dealing with them? Perhaps there
are programming styles within the existing language I have failed to
notice which would help alleviate these problem?

I hope this wasn't too boring or vague, thanks for a cool language,
Dan.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------