[m-dev.] Solver types in Mercury - meeting notes and comments
Ralph Becket
rafe at cs.mu.OZ.AU
Fri Feb 13 09:36:21 AEDT 2004
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
--------------------------------------------------------------------------
More information about the developers
mailing list