[mercury-users] uniqueness

[Mark Brown]

Hi Valery,

On 12-Jun-2006, valery at freesurf.fr <valery at freesurf.fr> wrote:
> Hello,
> 
> In my first attemps to use Mercury, I run into some problems related to
> uniqueness. It's no surprise, it was the same with Clean !
> 
> :- pragma promise_pure(main/2).
> main(!IO) :-
>   N = 3,
>   B = new(N, N, 0),
>   mark((1, 2), 1, B, B1), % problem 1
> %  (
> %    in_bounds(B1, X, Y),
> %    format("(%d, %d) -> %d\n", [i(X), i(Y), i(B1 ^ elem(X, Y))], !IO) %
> problem 2
> %  ),
>   format("%d\n", [i(B1 ^ elem(1, 2))], !IO),
>   impure report_stats.
> 
> :- type board == array2d(int).
> :- type point ---> (int, int).
> 
> :- pred mark(point::in, int::in, board::array2d_di, board::array2d_uo) is
> det.
> mark((X, Y), V, B0, B) :- B = B0 ^ elem(X, Y) := V.
> 
> :- pred is_free(point::in, board::in) is semidet.
> is_free((X, Y), B) :- B ^ elem(X, Y) = 0.
> 
> 1/ When I try to use the state variable syntax, that is, I replace "B, B1"
> with "!B", the compiler chokes.

You need to explicitly introduce new state variables, either in the head
of the clause or via an explicit existential quantifier.  For example:

	main(!IO) :-
		some [!B] (
			N = 3,
			!:B = new(N, N, 0),
			mark((1, 2), 1, !B),
			...
		).

> 
> 2/ The commented out portion is rejected as well. I suspect this is
> because nondeterministic predicates are not allowed to perform IO, but the
> error message doesn't state it clearly.

I guess that in_bounds/3 is nondet, and the error message you will get
would be along the lines of "main/2 is declared det, inferred nondet"
which pretty much covers the problem in its general form.

If the error message is still confusing you, feel free to post it here
and ask for an explanation.

> What is the common idiom to output
> the contents of a collection ?

If the collection type provides a foldl/4 predicate then typically you
could print the contexts in the following way:

	foldl(output_element, Collection, !IO)

where output_element would have a definition like:

	output_element(Element, !IO) :-
		... write one element of the collection ...

If the collection doesn't have a foldl predicate but does have something
like the nondet mode of member (that is, it nondeterministically produces
each element in the collection), then you can create a list of the elements
using solutions/2 and then output them with list.foldl/4.

> 
> 3/ More generally, I need to model states more complex than a single
> array, like several arrays plus a couple of integers. As I understand the
> documentation, this is not yet possible, because uniqueness is limited to
> IO and the array hacks.

The current limitations are that nested uniqueness doesn't work, and that
`ui' modes don't work.  For the former, I think you can work around the
problem buy using `unsafe_promise_unique' as appropriate.  For the latter,
you can use the same technique (read: hack) that the array.m library module
uses -- use an inst whose name suggests that it should be unique, but whose
definition is really just the same as ground.  You will lose some static
checking, and you should also avoid using `--optimise-duplicate-calls'
since the compiler may incorrectly optimise array updates otherwise.

A better alternative may be to use version_arrays, which don't need to be
unique.  See the comments at the top of version_array.m.

> Is uniqueness for user defined types planned for
> near future ?

Unfortunately, a proper solution to this problem is a Large Amount Of Work,
so this won't be fixed in the near future.  It's still in the longer term
plans, though.

Cheers,
Mark.

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