[m-dev.] call for opinions on promise_same_solutions syntax

[Zoltan Somogyi]

Recently I proposed that we should have a new construct to handle situations
such as the one below:

	:- type set(T)
		--->	set_as_234_tree(tree234(T))
		where equality is ...

	:- pred one_member(set(T)::in, T::out) is nondet.

	one_member(Set, Item) :-
		Set = set_as_234_tree(Tree),
		tree234.member(Tree, Item).

Here, the code of one_member is not valid Mercury. Tree234.member is nondet,
which means the deconstruction of Set *cannot* be in a first solution context,
but since the type of Set has user-defined equality (UDE), it *must* be in a
first solution context. The only way around this is do things such as

	one_member(Set, Item) :-
		promise_equivalent_solutions [P] (
			Set = set_as_234_tree(Tree),
			P = tree234.member(Tree)
		),
		P(Item).

or

	one_member(Set, Item) :-
		promise_equivalent_solutions [List] (
			Set = set_as_234_tree(Tree),
			tree234.keys(Tree, List)
		),
		member(List, Item).

neither of which is attractive. The solution we came up with is a new kind
of scope in which some deconstruction goals are marked as not having to be
in a first solution context even if they involve types with UDE, this being
justified by the programmer's promise that the values of the output variables
of the scope don't depend on which of the many possible concrete values
corresponding to the abstract values of the deconstructed variables are
actually stored in those variables.

The HLDS has already been modified to represent these new goals, by the
addition of a promise_same_solutions scope type (actually as a variation
on the existing promise_equivalent_solutions scope type), and a new marker
for the deconstruction goals. The question now is what the syntax should be.

Here are three possible schemes, and how one_member would look with each
schema.

	Schema 1
	given (
		Abstract1 = f(Concrete1),
		Abstract2 = f(Concrete2)
	) promise_same_solutions [Vars] (
		...
	)

	one_member(Set, Item) :-
		given Set = set_as_234_tree(Tree)
		promise_same_solutions [Item] tree234.member(Tree, Item).

	Schema 2
	promise_same_solutions [Vars] (
		deconstruct Abstract1 = f(Concrete1),
		deconstruct Abstract2 = f(Concrete2),
		...
	)

	one_member(Set, Item) :-
		promise_same_solutions [Item]
			deconstruct Set = set_as_234_tree(Tree),
			tree234.member(Tree, Item)
		).

	Schema 3
	promise_same_solutions [Vars] (
		deconstruct (
			Abstract1 = f(Concrete1),
			Abstract2 = f(Concrete2)
		),
		...
	)

	one_member(Set, Item) :-	% same as with schema 2.
		promise_same_solutions [Item]
			deconstruct Set = set_as_234_tree(Tree),
			tree234.member(Tree, Item)
		).

In schema 1, given would be an binary prefix operator whose second operand
has to be a promise_same_solutions goal, and whose first operand could be
either a unification or a conjunction of unifications.

With schemas 2 and 3, you need only an ordinary prefix operator, not a
binary prefix operator. In both schemas, the new deconstruct operator
would only be allowed to appear in promise_same_solutions scopes.
In schema 2, its operand would have to be a unification goal, and it would
be allowed to appear more than once in a promise_same_solutions scope.
In schema 2, its operand could also be a conjunction of unifications, and
it would not be allowed to appear more than once in a promise_same_solutions
scope. You could also have a schema 4 in which the operand could be either
a unification or a conjunction of unifications, and it could also appear
more than once.

Any preferences on what schema we should follow? My vote, Ralph's and Julien's
is for schema 2. It is syntactically less complex than schema 1, and compared
with schema 3 and 4, its advantage is that it uses the deconstruct operator
in a similar way to how we already use the impure and semipure operators.

Any preferences on alternate keywords to use? I think promise_same_solutions
should stay as close as possible to promise_equivalent_solutions, which it
is a variant of. However, I am much less sure about "deconstruct". Since the
goals it marks form the domain of the promise_same_solutions scope, some
variation on promise_same_solutions_domain would be nice, but only if it is
much shorter. Ralph and Julien and I kicked around "promise_domain" and
"domain", but finally came down with a weak preference for "deconstruct".
Any concurring or dissenting opinions?

On a distinct but related matter, we currently consider any predicate
defined by mode-specific clauses to be impure unless promised to be pure
with a ":- pragma promise_pure" declaration. The problem with this is that
":- pragma promise_pure" is also used to promise away actual impurity
in the clauses themselves. I think we should provide a new pragma that
promises merely that the mode-specific clauses are equivalent *without*
promising anything about the purity of those clauses. How about
":- pragma promise_equivalent_clauses"? And if we have this new pragma
and the promise_pure scopes I added a while ago, do we need the old
meaning of promise_pure anymore? If not, we could start the long process
of deprecating it; not too many people will be affected. (This is related
because the output variables listed in promise_same_solutions scopes
are often mode specific, so the clauses they appear in must be mode specific
too.)

Zoltan.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------