[mercury-users] Hi, and determinism

[Peter Schachte]

> 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).

Tom and Fergus already suggested solutions to this problem, both of which
entail separating into different predicates/functions the part of the
computation that can fail (or can have multiple solutions) from the part
that is expected to be an exhaustive and exclusive switch on the
constructors of the type, which can then be declared det.  I don't like
these idioms very much because I feel they make the code a bit artificial
and a but bulkier than necessary.  I'd like to suggest an alternative
solution:  a explicit case facility.  It's really only the basic idea that
I'm interested, but in the interests of concreteness, I'll go ahead and
propose a syntax, but if someone has a better syntax, great.

I would propose that your example predicate could instead be written:

	correct(L,Ba,Bc) :-
		case L of
		    (	[] -> Ba = Bc
		    ;   [H|T] ->
			data_modify(H,Ba,Bb),
			correct(T,Bb,Bc)
		    ).

The case construct would be such that no matter the declared determinism of
the predicate it appears in, all the constructors of the type must be
covered by exactly one case.  If not, it is a compile-time error, so if the
base case were omitted, an error would be reported.  Note also that this
feature works no matter what mode correct is called in.  If it is somehow
used to generate L, that's fine, and it'll still get a warning if a case is
missing or repeated.

There are many refinements and extensions of this basic facility that might
be useful.  There should be a functional version of it, so `correct' could
also be written as a function:

	correct(L,B) =
		case L of
		    (	[] -> B
		    ;   [H|T] ->			
			correct(T, data_modify(H, B))
		    ).

It would probably be good to allow alternatives for the cases:

	:- type foo ---> a(int) ; b(int) ; c ; d.

	... case Foo of
		(   (a(X) ; b(X) ) -> some_really_long_body
		;   (c ; d) -> whatever
		)

Comments welcome, particularly from proponents of the approach of splitting
the predicate/function in two to take advantage of the determinism system.


-- 
Peter Schachte <schachte at cs.mu.OZ.AU>  Intellectual brilliance is no
http://www.cs.mu.oz.au/~schachte/      guarentee against being dead wrong.
Phone:  +61 3 8344 9166                    -- David Fasold 
Fax:    +61 3 9348 1184                
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------