[m-dev.] Re: [HAL-dev] Adding Herbrand types to Mercury

[Ralph Becket]

Fergus Henderson, Wednesday, 17 December 2003:
> I missed the start of this thread.

Probably not - it was cross posted to both Mercury and HAL developers.

> On 17-Dec-2003, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > David Overton, Wednesday, 17 December 2003:
> > > On Tue, Dec 16, 2003 at 05:40:31PM +1100, Ralph Becket wrote:
> > > > The reserve_tag pragma adds an extra data constructor (which I'll call
> > > > '$') to the type t and is roughly the same as saying
> > > > 
> > > > :- solver type t
> > > > 	--->	'$'(herbrand_var(t))
> > > > 	;	f
> > > > 	;	g(t)
> > > > 	where equality is unify_t.
> > > >
> > > > where herbrand_var/1 is a private builtin type that might look like
> 
> The reserve_tag pragma in Mercury is equivalent to adding an extra data
> constructor, but the Mercury implementation does not know the type or
> even the number of arguments to this constructor.  The argument might be
> herbrand_var/1 or it might be something else.  It is not a type defined
> in library/private_builtin.m, rather, it is up to the user-defined code
> which implements unification for `t'.

I wasn't being entirely clear: I understand that reserve_tag reserves an
extra data constructor with tag 0 for whatever purpose it's required for
and that handling this is the job of the corresponding unification
predicate.  I was conflating this with the herbrand_var stuff to tell a
simpler story, although I probably should have made that explicit.

> For traditional Prolog alias structures, you'd need something like this:
> 
> 	:- type herbrand_var(T)
> 	--->    free
> 	;       alias(herbrand_var(T))
> 	;       bound(T).

It occurred to me that with traditional Prolog alias structures, you
don't need alias(X) since that's equivalent to bound('$'(X)) (and both
rely upon structure sharing being preserved.)

> Or, if you want to be completely traditional, you can drop the "free"
> case and represent free variables as self-references, X = alias(X).

Indeed.  I'm inclined to prefer the PARMA scheme because once you've
bound a variable, you no longer need multi-step dereferencing for it.

> No.  In particular, there is no requirement that a solver type value
> with inst "ground" always be represented by a non-'$' data constructur.
> For example, the ground value "f" might be represented as '$'(bound(f))'.

Could you present a brief statement of what it means for
- a solver type value to have inst any,
- a solver type value to have inst ground,
- a non-solver type value to have inst any, and
- a non-solver type value to have inst ground.
I'd find that very useful.

Hmm, it seems that most of what needs to be done already exists in the
compiler.

Thanks for the feedback,
-- 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
--------------------------------------------------------------------------