[m-rev.] for review: add `any_is_bound' pragma

[Fergus Henderson]

On 18-Jul-2003, David Overton <dmo at cs.mu.OZ.AU> wrote:
> On Fri, Jul 18, 2003 at 02:08:11PM +1000, Fergus Henderson wrote:
> > 
> > How common is that?
> > You could always use an inst cast in such situations.
> > Is the problem common enough that it's really worth
> > extending the language to solve it?
> 
> It's quite a common problem.

OK.

> > > An extension to this that we would like is for it to be possible to
> > > declare an abstract type to be a solver type, but have its
> > > implementation to be an ordinary "non-solver" discriminated union type
> > > (or foreign type).  E.g.
> > > 
> > > 	:- interface.
> > > 	:- solver type foo.
> > > 
> > > 	:- implementation.
> > > 	:- type foo ---> ....
> > 
> > What's the difference in semantics between that and
> > 
> >  	:- interface.
> >  	:- solver type foo.
> >  
> >  	:- implementation.
> >  	:- solver type foo ---> ....
> 
> With the former, the type foo will appear to be a solver type from
> outside the module, but just a normal type from within the module.
> (i.e. outside the module `any' is different to `bound(...)', but inside
> the module they are the same).  This is useful for implementing
> constraint solvers using a ground representation.

I don't think that is the right way to implement constraint solvers
using a ground representation.  There is a fundamental difference
between a value and its representation(s).  Conversion between the
two needs to be explicit for the logic to make logical sense.
If you don't make that explicit, then either the module system
affects the declarative semantics in a very complicated way
(which is undesirable since it makes reasoning about programs
more difficult, and causes problems for intermodule optimization etc.),
or the logic will become inconsistent.

If you want to implement constraint solvers using a ground representation,
it would be better to leave the type definition abstract (rather than
giving a definition which would be lying to the compiler), and provide
a conversion routine to convert between the abstract values and their
representations or vice versa.  The representations would have a different
type than the values.

I'd be happy to consider adding more support, for example some explicit
syntax, for this two-type idiom.  But I don't want to add support for
the one-type idiom that you're talking about, since that idiom fudges
the difference between values and their representations in a way that
would lead to logical inconsistencies.

Given this position, the only legitimate use that I can think of for
solver types with a concrete Mercury discriminated union type definition
would be for Herbrand types, so it might make sense to use the
`:- solver type foo ---> ...'  syntax for that.  (IMHO it would be best
to avoid using jargon such as "Herbrand" in the language syntax.)

-- 
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-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------