[mercury-users] determinism suprises

[Fergus Henderson]

On 07-Dec-2000, William Lee Irwin III <wli at holomorphy.com> wrote:
> I was recently surprised to find a couple of "catches" with respect
> to determinism.
> 
> First, I had a predicate on an algebraic data type with a situation
> like this:
> 
> :- interface.
> :- type algtype ---> left ; right.
> :- pred some_pred(algtype).
> :- mode some_pred(in) is det.
> :- mode some_pred(out) is multi.
> :- implementation.
> some_pred(_).
> 
> This led to what I found to be a surprising instantiation error.
> algtype.m:008: In clause for `some_pred(out)':
> algtype.m:008:   mode error: argument 1 did not get sufficiently instantiated.
> algtype.m:008:   Final instantiatedness of `HeadVar__1' was `free',
> algtype.m:008:   expected final instantiatedness was `ground'.

Yes, the compiler won't try to nondeterministically generate values
based on the type.  You have to explicitly bind them yourself.

> The workaround I ended up using was:
> some_pred(left).
> some_pred(right).

That's probably the right approach in this case.

The reason that we don't do this automatically is not because we
haven't thought of it (we have) or because it would be hard to
implement (it wouldn't); rather, it is because we think it would make
the behaviour of the code harder to understand and would only rarely
be the right thing to do.  For the rare cases where it is the right
thing to do, you can easily write it explicitly as you have done.
This makes it much easier for someone reading your code to understand
how the code works.

> ... which gets hairy for types with more alternatives and explodes
> combinatorially with various ways of combining types.

The generator for a given type should be no more complicated than the
type definition; indeed, you can easily convert a type definition into
a generator.  You can use a type class for this, so that you can
handle polymorphic types like maybe(T):

	:- typeclass gen(T) where [
		pred gen(T),
		mode gen(out),
		mode gen(in)
	].

	:- instance gen(maybe(T)) <= gen(T) where [
		pred(gen/1) is gen_maybe
	].

	:- pred gen_maybe(maybe(T)) <= gen(T).
	:- mode gen_maybe(out) is multi.
	:- mode gen_maybe(in) is det.
	gen_maybe(no).
	gen_maybe(yes(X)) :- gen(X).

Mixing different types is straight-forward:

	:- type foo ---> bar ; baz(algtype) ; quux(bool, algtype).

	:- pred gen_foo(foo).
	:- mode gen_foo(out) is multi.
	:- mode gen_foo(in) is det.
	gen_foo(bar).
	gen_foo(baz(X)) :- gen(X).
	gen_foo(quux(Y, Z)) :- gen(Y), gen(Z).

	:- instance gen(foo) where [
		pred(gen/1) is gen_foo
	].

But for types with an infinite number of alternatives (e.g. lists,
integer), or even just a very large number of alternatives (e.g. int),
it is almost always a bad idea to nondeterministically generate values
based on the type.

> Another "catch" I found was the following:
> 
> :- pred color(squareindex, color).
> :- mode color(in, out) is det.
> :- mode color(in, in) is semidet.
> :- mode color(out, in) is multi.
> color({File, Rank}, Color) :-
>    file_parity(File, FileParity),
>    rank_parity(Rank, RankParity),
>    add_parity(FileParity, RankParity, Residue),
>    parity_to_color(Residue, Color).
> 
> Now, file_parity, rank_parity, and parity_to_color have all the
> necessary modes and determinisms to allow all of color's modes and
> determinisms given the appropriate ordering of conjunctions, but I
> still found that the reordering was not done for each mode:
> 
> board.m:018: In `color(out, in)':
> board.m:018:   error: determinism declaration not satisfied.
> board.m:018:   Declared `multi', inferred `nondet'.
> board.m:167:   call to `parity_to_color(in, in)' can fail.
...
> It looks like only one ordering of the
> conjunction is being used for all modes, although my expectation was
> that the code would be reordered for each mode to satisfy its
> determinism.  Is this a reasonable expectation?

A different ordering of the conjunction will be used for each mode,
but conjunctions are only reordered to satisfy the modes, not to
satisfy the determinism.

Could you post the code, or at least the mode declarations,
for the predicates that this one calls?

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