[m-dev.] Summary of solver types discussion in today's meeting

[Ralph Becket]

To start off, I'll just recap the existing proposal for adding solver
types to Mercury with a couple of documented examples.  Point (4) at the
end records an important point brought up at the meeting.

(1) Example: constrained ints.

The cint solver type would be defined as follows

	:- solver type cint ---> int(int)
		where	constrained is var(id `with_inst` ground),
			initialisation is init_cint,
			equality is equal_cint.

- id is an identifier type for some variable managed by the cint solver
  implementation;
- the `constrained is var(...)' adds var(...) as a (specially treated)
  data constructor to cint;
- the `initialisation is init_cint' tells the compiler to insert calls
  to the user-provided predicate init_cint/1 to initialise free
  variables whose inst needs to be any (e.g. as in(any) arguments to a
  call).  The implementation of init_any/1 should, in this example,
  somehow construct a new solver variable, give it an id X, and return a
  var(X) result.

This is almost the same as having written

	:- type cint ---> int(int) ; var(id)
		where	equality is equal_cint.

with the following exceptions: 

(a) A solver type value with inst any *may* (if it is not currently
`fixed') unify with two different values, X and Y, but where X and Y do
not themselves unify.  (Inst any is the same as inst ground for
non-solver type values.)

(b) Construction and deconstruction of the `constrained' data
constructor must be performed via the two compiler generated functions

		% Used for deconstruction.
		%
	:- impure func match_var(id::out(ground)) = (cint::in(any))
		is semidet.

		% Used for construction.
		%
	:- impure func make_var(id::in(ground)) = (cint::out(any))
		is det.

The `_var' parts of the function names and the argument modes are taken
from the `constrained is var(...)' declaration.

These functions are needed because Mercury (currently) has no syntax for
impure unifications nor for mode constraints on arguments.

These functions are impure because they allow us to decide (amongst
other things) whether two values with the same denotation actually have
different representations or vice versa.  This sort of thing wrecks
logic (cf. Prolog's non-logical predicates.)

Operationally, match_var and make_var are just the same as
deconstruction and construction with var(...) - indeed, after type and
mode checking, the compiler replaces them with unifications with var so
that switch detection and determinism analysis work as expected on
var(...) values.

For example, our unification predicate might look something like this:

	:- pred equal_cint(cint::in(any), cint::in(any)) is semidet.
	:- pragma promise_pure(equal_cint/2).
	
	equal_cint(int(K), int(K)).
	equal_cint(int(K), Y) :-
		impure Y = match_var(IdY),
		...
	equal_cint(X, int(K)) :-
		impure X = match_var(IdX),
		...
	equal_cint(X, Y) :-
		impure X = match_var(IdX),
		impure Y = match_var(IdY),
		...

The `deconstructions' of X and Y can't be written inline like the
pattern matching for const/1 because we have to use the impure semidet
function match_var/1.

However, after type checking and mode analysis, the compiler will have
converted the above to

	:- pred equal_cint(cint::in(any), cint::in(any)) is semidet.
	:- pragma promise_pure(equal_cint/2).
	
	equal_cint(X, Y) :-
		(
			X = const(K),
			Y = const(K)
		;
			X = const(K),
			Y = var(IdY),	% Impure
			...
		;
			X = var(IdX),	% Impure
			Y = const(K),
			...
		;
			X = var(IdX),	% Impure
			Y = var(IdY),	% Impure
			...
		).

and this will be identified as a switch as we would like.

(2) Example: constrained complex numbers.

	:- solver type ccomplex ---> complex(float, float)
		where	constrained is
				c(cfloat `with_inst` any,
				  cfloat `with_inst` any),
			initialisation is init_ccomplex,
			equality is equal_ccomplex.

Now, we might write

	:- pred equal_ccomplex(ccomplex::in(any), ccomplex::in(any))
			is semidet.
	:- pragma promise_pure(equal_ccomplex/2).

	equal_ccomplex(complex(Re, Im), complex(Re, Im)).
	equal_ccomplex(complex(Re, Im), Y) :-
		impure Y = match_c(CRe, CIm),
		CRe = Re,
		CIm = Im.
	equal_ccomplex(X, complex(Re, Im)) :-
		impure X = match_c(CRe, CIm),
		CRe = Re,
		CIm = Im.
	equal_ccomplex(X, Y) :-
		impure X = match_c(CReX, CImX),
		impure Y = match_c(CReY, CImY),
		CReX = CReY,
		CImX = CImY.

...and all is well with the world.

(3) Example: using an externally defined solver type.

Say we are wrapping an externally defined solver type foo (e.g. written
in C) and providing no extra data constructors, then we can write

	:- solver type cfoo
		where	constrained is foo(external_solver_type),
			initialisation is external_initialiser_pred,
			equality is external_equality_pred.

Here, although there is no `---> <<data constructors>>' part to the
definition, the type is still a discriminated union, but with just one
data constructor - foo/1 in this case.  Otherwise, everything is the
same as in the other examples.

(4) `where ... constrained is foo(...), ground is foo(<<inst>>, ...), ...'

It is not necessarily the case that a ground value (i.e. one for which
the set of unifiable values forms an equivalence class) has to have a
ground representation.  Consider the case of a constrained polar
coordinate type (r, theta): such a value that has unified with the
rectangular coordinate (0, 0) can take on any value of theta (theta need
not be ground, even).

The importance of the `ground is ...' part is to define the insts for
the fields of the constrained data constructor when it is known to be
ground.  This is an operational concern.

Denotationally, deciding semantic groundness is an impure operation that
must be defined by the author of the constrained type module, if such a
thing is provided at all.

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