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

[Ralph Becket]

Fergus Henderson, Tuesday, 27 January 2004:
> On 23-Jan-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > (2) Herbrand types in Mercury
> > 
> > Herbrand types are a special kind of solver type supporting Prolog
> > style unification.
> > 
> > The syntax for Herbrand type definitions will be as follows:
> > 
> > :- herbrand type <typename> ---> <du constructors>.
> >
> > Herbrand types have private builtin <initpred> and <unifypred>
> > definitions with signatures
> > 
> > :- pred init_Herbrand(T::out(any)) is det.
> > :- pred unify_Herbrand(T::in(any), T:in(any)) is semidet.
> 
> I'm a bit confused here.  Should that be
> 
> 	:- pred init_Herbrand(<typename>::out(any)) is det.
> 
> or perhaps
> 
> 	:- pred init_<typename>(<typename>::out(any)) is det.
> 
> (and likewise for unify_Herbrand)?
> 
> Here I am using angle brackets to denote meta-variables.

On the one hand, yes, and on the other, no :-)  init_Herbrand and
unify_Herbrand work identically for all Herbrand types under the PARMA
scheme.  But following Peter Stuckey's observation, I'll probably start
with WAM style Herbrand variables, in which case the signatures will
be type specific.

> > The unification procedure generated for <typename> is almost identical
> > to what would be generated if it were an ordinary du type, with the
> > exception that unify_Herbrand/2 is called where one or both of the
> > variables being unified is "unbound" (i.e. has been initialised, but is
> > not currently bound to a ground value.)
> 
> I'm not quite sure why you want to split unification into
> two parts, the first part being the unification procedure
> and the second part being the unify_Herbrand procedure.
> Wouldn't it be simpler to just have the unification procedure
> handle all the cases?

Yes - that was a late night "inspiration" that made it into a morning
e-mail.  Dumb idea.

> Is it a design goal to allow users to implement their own constraint
> solver for Herbrand-style variables?

Not as far as I have considered, although I see no reason why Herbrand
types shouldn't be used by other constraint solvers or types.

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