[m-dev.] Solver types reloaded

[Ralph Becket]

The old proposition was that we write something like

:- solver type t
	--->	varrep(varrep_type `with_inst` varrep_inst)
	;	f(...)
	;	g(...)
	where initialisation is init_t, equality is equal_t, etc.

and that

- a construction X = varrep(R) would require R to have inst varrep_inst
  and would result in X having inst any;

- a deconstruction varrep(R) = X would require X to have inst any and
  would result in R having inst varrep_inst.

One major problem with this idea is that, as Fergus pointed out, it
breaks referential transparency by conflating solver *values* with
*representations of solver values*.  Logic requires that if S is the set
of values that unify with X, then for all Y and Z in S, it must be the
case that Y and Z also unify with each other.  This doesn't work in the
above suggestion for varrep(_) that are as-yet unbound (i.e. are in the
solver equivalent of being `free').



The new proposition.

After a meeting with Fergus and Zoltan, we came up with the following
suggestion (as before, the syntax is up for argument once we have the
denotational and operational semantics nailed down.)

The new proposition is that t would be defined thus:

:- solver type t
	--->	f(...)
	;	g(...)
	where	constrained is varrep(varrep_type `with_inst` varrep_inst),
		initialisation is init_t,
		equality is equal_t,
		etc.

The `constrained is varrep(varrep_type `with_inst` varrep_inst)'
fragment defines the reserved tag constructor.  This constructor
definition is just like other constructors in that it may include
multiple, optionally named, fields, although the inst for non-free
values of each field must also be provided.

[Why would we want to specify the insts for these fields?  The canonical
justification is if we wanted to define a constrained complex number
type as a pair of constrained floats.  In this case the subfields
for the real and imaginary components would need to have inst any rather
than ground.  This information has to appear somewhere.]

Note that the discriminated union part of the definition `---> f(...) ;
g(...)' is optional.  If it is omitted, then the type t has just a
single constructor, varrep.  This may be useful for types like cint and
cfloat where other constructors are not needed.

The varrep constructor is not usable directly by the solver implementor,
however.  Instead, the implementor must use the two compiler generated
functions

	% Used for deconstruction.
	%
:- impure func match_varrep(varrep_type :: out(varrep_inst)) = (t :: in(any))
		is semidet.

	% Used for construction.
	%
:- impure func make_varrep(varrep_type :: in(varrep_inst)) = (t :: out(any))
		is det.

These functions are impure because they should not be reordered with
respect to pure goals that may or may not affect the constraint store.
(See the referential transparency problem described for the old
proposition.)  Since they are impure, they have no declarative semantics
and the problem with referential transparency goes away: it's the solver
implementor's responsibility to ensure purity and include the
appropriate promise_pure declarations; we don't need to damage the
semantics of pure Mercury to support solver types.

A pass in the compiler, occurring after mode analysis and before switch
detection (and hence also before determinism analysis) converts calls to
match_varrep and make_varrep into the corresponding unifications with
the constructor varrep.  This means that match_varrep can appear as a
unification branch in switches.

The discussion continued on to cover issues of groundness and
floundering, but as I've been working since 7am I think I'll summarise
those items tomorrow morning!  (And I'll be providing sample code using
the new proposition.)

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