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

[Fergus Henderson]

On 13-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> 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.

That's why I think the distinction is necessary!

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

In the declarative semantics, what is the set of (ground) values for t?

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

I'm asking about the declarative semantics, not the representation.

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

You are using functional notation for `cf', as if it was a function from
int to cfloat, but `cf' is in fact not a mathematical function from int
to cfloat.  It is a function from int to "cfloat representation", but if
you consider the result type of `cf' to be just cfloat, then it no longer
has all of the properties expected of mathematical function, and so using
functional notation for it is going to break some of the nice logical
properties that we want to be able to rely on.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------