[m-dev.] For discussion: impedance mismatch with solver/non-solver types

[Ralph Becket]

I've been converting some of the HAL benchmarks to Mercury using the new
solver types.  Not surprisingly, a number of bugs have come to light.
One that concerns me most concerns the interaction between solver types
and non-solver types.

Say I define a solver type herbrand_list(T) with pseudo-data constructor
functions nil and cons:

% Construct a nil cell.
:- func nil = (herbrand_list(T)::out(any)) is det.

% Construct a cons cell.
:- func cons(T::in, herbrand_list(T)::in(any)) =
		(herbrand_list(T)::out(any)) is det.

First, consider a situation where Xs : herbrand_list(int) :: any,
Y : int :: ground, Ys : herbrand_list(int) :: free.  (I'm using `:' to
mean `with_type` and `::' to mean `with_inst`.)  A goal

	Xs = cons(Y, Ys)

will be scheduled by the compiler as

	initialise_herbrand_list_var(Ys),
	Tmp1 = cons(Y, Ys),	% using mode cons(in, in(any)) = out(any)
	unify(Xs, Tmp1)

Now consider the situation where Xs and Ys start as above, but Y ::
free.  In this case the compiler can't schedule the goal because
there's no way to make Y ground to schedule a call to cons.

Hmm, we think, and set about implementing a second mode for cons:

:- mode cons(T::out, herbrand_list(T)::out(any)) =
		(herbrand_list(T)::in(any)) is semidet.

An implementation for this mode would have to throw an exception when
the RHS is a var (i.e. an initialised, unbound variable) since there's
no way to succeed and assign a meaningful value to the T result.

Worse, the compiler would use this mode to schedule our goal rather than
constructing-then-unifying as it did before we introduced the new mode
for cons.  This would be a disaster if there does exist a scheduling of
the goal and its surrounding conjuncts that guarantees not to lead to an
exception (although there is currently no way of telling the compiler
such things).

Not adding a mode like the above, on the other hand, means we can't use
unification expressions to deconstruct herbrand_list(T) values.

This issue is relevant to solver implementors in general and, in
particular, affects the support for Herbrand (i.e. Prolog) types I have
been contemplating.

Two partial solutions come to mind, neither of which strikes me as
ideal.

(1) Stick to the construct-then-unify approach.  Provide separate "ask"
functions/predicates for deconstruction.  This is bad because it makes
code less "reversible".  I don't have enough knowledge of solver
implementation to say whether it's any use or not.  My impression is
that solver implementations are highly dependent upon mode-specific
code.  It would be wonderful to find a way to minimise the need for such
sordidness.

(2) Adopt the convention that all values you can put into/extract from a
solver type value must themselves be solver type values.  This preserves
much code reorderability at the cost of requiring conversion functions
everywhere at the interface between solver and non-solver values.
Sounds like a nightmare to me.

On the whole I prefer option (1) (it's less work :-), but the whole
thing feels bad.  Surely there must be a better solution...

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