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

[Ralph Becket]

Fergus Henderson, Thursday, 12 February 2004:
> On 12-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> 
> > SOLVER TYPES
> ...
> > 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.
> 
> It's not just inst casting that is required.  You need to do type casting
> at the same time.  For a solver type, there is an important distinction
> between the set of (ground) values of the solver type, and the set of
> representations (values of the solver's *representation* type), which
> may represent constrained non-ground values.

It's not obvious to me that the distinction is necessary; it's the
equality semantics that matter.  For instance, say I have a Herbrand
type and I reserve a particular data constructor v(int) to denote (bound
or unbound) variables, using ints as variable identifiers.  The truth of
v(3) = v(4), say, depends upon the constraint store, not on the integer
identifiers alone.

> > 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.)
> 
> Good question.  But I'm still waiting for the answer :)
> I would like to know the declarative semantics, not just the
> operational semantics.  In particular, what is the set of (ground) values
> for the type, and what are the equality axioms?

The type t is, with one exception, an ordinary type with user-defined
equality.  The equality axioms are those of user-defined equality.
What's special about t is that a deconstruction of v(X) with inst any
leaves X with inst i (and vice versa for constructions of v/1).  But
insts are concerned with operational semantics and shouldn't affect the
denotational semantics.

[Correction s/\<float\>/int/ made to included text below.]
> > :- solver type cfloat ---> cf(int `with_inst` ground)
> > 	where initialisation is init_cfloat, equality is equal_cfloat.
> 
> What is the set of ground values for this type?

At the representation level, {cf(I) | I is a ground int}

Whether two members of this set compare as equal or equal to a
particular integer depends upon the constraint store, which in turn
depends upon the constraints that have been posted on a given execution
path.

Let me put it this way: the way Mercury variables are currently handled
in the back end, for instance, is just one way of doing it.  We *could*
give each Mercury program variable some arbitrary unique identifier and
then just keep track of what, if anything, is bound to each variable
using an identifier-to-value mapping at runtime.  The change in
underlying representation would not affect the semantics of the program.

But I have a nagging feeling I'm not quite getting the point you're
making...  If so, can you post a small, detailed example to help clarify
the argument?

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