[m-dev.] Solver types in Mercury - meeting notes and comments

[Ralph Becket]

This is partly a review of the HAL/Mercury meeting held on Thursday 12
February on adding solver types to Mercury, and partly personal
comment/suggestion.

I'll start with an outline of the problem, move on to a suggestion as to
the syntax and semantics, then discuss initialisation and unification,
and finish with some examples.

[I'm not going to discuss comparison much, if at all, since it's rather
similar to unification in terms of the machinery involved.  Also, I have
probably put `is semidet' where there should be `is cc_multi' for the
equality predicates and missed off the odd promise_only_solution
wrapper, but hey, that's minor detail.  I hope!]

SOLVER TYPES

Solver types are things like constrained integers, constrained complex
numbers, Herbrand types and so forth.

The problem with solver types is that the solver machinery should not be
exposed to users, but clearly has to be exposed in the implementation.

The current suggestion is that a solver type should be treated as a du
type with an extra "reserved" constructor that is used to hide the
internal representation used by the solver implementation.

One issue is that while users of a solver type will see its values as
having inst any, the solver implementation will need more refined inst
information.  Some inst casting is required and there is a question as
to how and where this should happen.

SUGGESTION

This was not discussed in the meeting, but I think it summarises where
we had got to in our thinking when the meeting broke up.

Consider the solver type t which I'll define using some hypothetical
syntax:

:- solver type t ---> v(u `with_inst` i) ; a ; b(t) ; c(int) ; d(cfloat)
	where initialisation is init_t, equality is equal_t.

What does this mean?  (I'll come to the `where ...' part in a bit.)

The `solver' annotation tells the compiler that the first constructor
(v/1 in this case) is there for the low-level solver machinery and
should be handled specially, as I'll explain next.

THE ANY AND GROUND INSTS

The `any' inst for a value of type t stands for

	bound(v(i) ; a ; b(any) ; c(ground) ; d(any))

(the type `cfloat' is another solver type - for constrained reals - and
consequently is mapped to inst any here.)

The `ground' inst for a value of type t stands for

	bound(a ; b(ground) ; c(ground) ; d(ground))

INST CASTING

A construction of a value of type t will result in a value with inst
any.

A deconstruction of a value of type t follows the usual rules, except
for the first constructor which is treated specially.

A successful deconstruction v(X) = Y (where Y starts with inst any) will
result in X having inst i (because the v/1 constructor is handled
specially).

Conversely, the construction X = v(Y) requires that Y have inst i and
will succeed with X having inst any.

INITIALISATION

A predicate init_t must be supplied by the programmer with the signature

:- pred init_t(t::out(any)) is det.

Calls to init_t will be introduced during goal scheduling wherever a
procedure call or construction requires a free variable to be
initialised to have inst any.

UNIFICATION

A predicate equal_t must be supplied by the programmer with the
signature

:- pred equal_t(t::in(any), t::in(any)) is semidet.

This is defined as per ordinary user-defined equality.

VISIBILITY

Ordinary visibility rules are all that are necessary: I think the
existing module system supports all the information hiding we need.

(Should one so desire, one could even export the data constructors for
solver types, just keeping the "implementation type(s)" abstract and
therefore not allowing users to directly construct solver type values
that they should be using the solver interface for.)


EXAMPLE: CONSTRAINED FLOATS - IMPLEMENTATION

:- module cfloat.
:- interface.

:- solver type cfloat.

:- func cfloat(float::in) = (cfloat::out(any)) is det.
:- pred (cfloat::in(any)) =< (cfloat::in(any)) is semidet.
...

:- implementation.

:- solver type cfloat ---> cf(float `with_inst` ground)
	where initialisation is init_cfloat, equality is equal_cfloat.

:- pred init_cfloat(cfloat::out(any)) is det.
:- pragma promise_pure(init_cfloat/1).

init_cfloat(cf(Id)) :-
	impure <<construct a new, initialised constrained integer,
		give it an float identifier, and assign it to Id>>.

:- pred equal_cfloat(cfloat::in(any), cfloat::in(any)) is semidet.
:- pragma promise_pure(equal_cfloat/2).

equal_cfloat(cf(X), cf(Y)) :-
	% X has inst ground because of deconstruction of cfloat/1
	% Y has inst ground because of deconstruction of cfloat/1
	impure <<solver implementation of equality of cfloats with ids
		X and Y>>.

:- promise_pure(cfloat/1).

cfloat(K) = v(Id) :-
	impure <<construct a new cfloat, give it an identifier, assign
		that to Id, and ensure that the new cfloat is bound to K>>.

:- promise_pure((=<)/2).

cf(X) =< cf(Y) :-
	% X has inst ground because of deconstruction of cfloat/1
	% Y has inst ground because of deconstruction of cfloat/1
	impure <<constrain the cfloat with id X to be =< the cfloat with
		id Y>>.

EXAMPLE: CONSTRAINED FLOATS - USE

The goal

	% X and Z have type cfloat and inst any
	%
	some [Y] (
		X =< Y,
		Y =< Z,
		member(K, [4.0, 5.0, 6.0]),
		Y = cfloat(K)
	)

is translated by the compiler into

	% X and Z have type cfloat and inst any
	%
	some [Y] (
		init_cfloat(Y),		% Initialise Y
		X =< Y,
		Y =< Z,
		member(K, [4.0, 5.0, 6.0]),
		Tmp = cfloat(K),
		equal_cfloat(Y, Tmp)	% User-defined equality pred for cfloat
	)



EXAMPLE: CONSTRAINED COMPLEX NUMBERS - IMPLEMENTATION

:- module ccomplex.
:- interface.

:- solver type ccomplex.

:- func ccomplex(cfloat::in(any), cfloat::in(any)) = (ccomplex::out(any))
		is det.
:- pred (ccomplex::in(any)) =< (ccomplex::in(any)) is semidet.
...

:- implementation.

	% There are two arguments for the `special' constructor, cc, and
	% we need to specify insts for both of them.
	%
:- solver type ccomplex ---> cc(cfloat `with_inst` any, cfloat `with_inst` any)
	where initialisation is init_ccomplex, equality is equal_ccomplex.

:- pred init_ccomplex(ccomplex::out(any)) is det.

init_ccomplex(cc(_Re, _Im)).
	% The compiler will transform this into something of the form
	%
	% 	init_ccomplex(cc(Re, Im)) :-
	% 		init_cfloat(Re),
	% 		init_cfloat(Im).

:- pred equal_ccomplex(ccomplex::in(any), ccomplex::in(any)) is semidet.

equal_ccomplex(cc(Re, Im), cc(Re, Im)).
	% The compiler will transform this into something of the form
	%
	% 	equal_ccomplex(cc(ReL, ImL), cc(ReR, ImR)) :-
	% 		equal_cfloat(ReL, ReR),
	% 		equal_cfloat(ImL, ImR).

ccomplex(Re, Im) = cc(Re, Im).

cc(ReL, ImL) =< cc(ReR, ImR) :-
	ReL =< ReR,
	( if ReL = ReR then ImL =< ImR else true ).
	%
	% The compiler will transform this into something of the form
	%
	%	cc(ReL, ImL) =< cc(ReR, ImR) :-
	%		ReL =< ReR,
	%		( if cfloat_equal(ReL, ReR) then ImL =< ImR
	%					    else true ).



EXAMPLE: HERBRAND TYPES - IMPLEMENTATION

The definition

:- herbrand type church ---> z ; s(church).

is syntactic sugar for

:- solver type church
	--->	var(wamvar(church) `with_inst` ground)
	;	z
	;	s(church)
	where initialisation is init_church, equality is equal_church.

where wamvar/1 is a built-in type and init_church and equal_church are
automatically constructed as follows:

:- pred init_church(church::out(any)) is det.
:- pragma promise_pure(init_church/1).

init_church(V) :-
	impure init_wamvar(V).

:- pred equal_church(church::in(any), church::in(any)) is semidet.
:- pragma promise_pure(equal_church/2).

equal_church(L, R) :-
	( if L = var(_) then
		L1 = deref_wamvar(L),
		( if   semipure unbound_wamvar(L1)
		  then impure bind_wamvar(L1, R)
		  else equal_church(L1, R)
		)
	  else if R = var(V0) then
		( if   semipure unbound_wamvar(R)
		  then impure bind_wamvar(R, L)
		  else semipure R1 = deref_wamvar(R),
		       equal_church(R1, L)
		)
	  else
	  	(	L = z,	  R = z
		;	L = s(C), R = s(C)
		)
	).

where init_wamvar/1, deref_wamvar/1, unbound_wamvar/1 and bind_wamvar/2
are all private builtins implementing WAM style reference chains.

COMMENTS

If the above scheme works then implementation is quite straightforward.

Comments and questions welcome.

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