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

[David Overton]

On Tue, Dec 16, 2003 at 05:40:31PM +1100, Ralph Becket wrote:
> Now we have the any inst and solver types, it might be an idea to add
> Herbrand types to the language.  This would hopefully also provide an
> idea as to how other constrained types should be implemented.
> 
> Implementation of constrained types in Mercury is supported by the any
> inst, solver types and types with reserved tags.
> 
> Since there is no extant documentation concerning these things, I

There is some documentation, e.g.

Mercury mode system, including `any' insts:
	http://www.cs.mu.oz.au/~dmo/dmo-phd-thesis.html

HAL mode system:
	http://www.csse.monash.edu.au/~mbanda/hal/cl2000-hal.ps

Implementation of Herbrand constraints in HAL:
	http://www.csse.monash.edu.au/~mbanda/hal/iclp99-hal.ps

although none of these explicitly describe Mercury's
`:- solver type' and `:- pragma reserve_tag' declarations.

I've put an updated and expanded copy of the last of these papers on
your desk at Monash.  It addresses a lot of the issues you discuss in
this email.  I think it would be worth a look.

> thought I'd start by outlining, as I see it, how they can be used
> to implement Herbrand types in Mercury (I believe this is very similar,
> if not identical, to what happens with HAL.)  Corrections and comments
> will be very welcome.
> 
> HERBRAND TYPES
> 
> The aim would be to allow type declarations like the following in the
> language:
> 
> :- herbrand type t
> 	--->	f.
> 	;	g(t).
> 
> The effect of the herbrand keyword would be to add Herbrand variables
> (supporting Prolog style variable aliasing) to the domain of the type t.
> 
> A source-to-source transformation would turn the above into
> 
> :- pragma reserve_tag(t/0).
> :- solver type t
> 	--->	f
> 	;	g(t)
> 	where equality is unify_t.
> 
> (unify_t is explained below).
> 
> 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
> this:
> 
> :- type herbrand_var(T)
> 	--->	free
> 	;	bound(T).

The `free' case here is really a reference to a PARMA pointer chain.
The `bound(T)' case does not apply because once a variable of type `t'
is bound it will be fully dereferenced.

> 
> The effect of the solver modifier on the transformed type definition for
> t is as follows:
> - a solver type value with inst *any* is not free and may be any of the
>   data constructors for the type *including* '$';
> - a solver type value with inst *ground* is not free and may be any of
>   the data constructors for the type *except* '$';
> - the inst *any* is identical to the inst *ground* for non-solver
>   types.

Not quite true, because a non-solver type could contain solver types.
E.g.

	:- type foo ---> f(bar).
	:- solver type bar.

inst `any' for type `foo' would be equivalent to `bound(f(any))'.

> 
> There would be a private builtin initialisation predicate that works for
> all Herbrand types:
> 
> :- pred init(<<any_herbrand_type>>).
> :- mode init(free >> any) is det.
> 
> init('$'(free)).

The implementation of init/1 would need to initialise the pointer chain
as a reference to itself.

> 
> The compiler would insert calls to init for every variable X or Y of
> type t in order to ensure that
> - X's inst is converted from free to any for calls that require it and
> - at least one of X and Y has a non-free inst in a unification X = Y.

I think you only want to add calls to init where it is actually required
(i.e. where a variable has inst `free' and needs to have inst `any').
Otherwise you incur unnecessary efficiency penalties.  E.g. in a
unification `X = Y' if you init both X and Y then you get a PARMA chain
with 2 elements after the unification.  If only one of X and Y is inited
and the other is `free' then you only need a single element chain.

It is reasonably easy to check where inits need to be inserted during
mode analysis.  In fact the Mercury mode checker already does this,
although it assumes the init predicate will be called <type>_init_any/1.
(See modes.m line 2111.)

> 
> There would be a private builtin dereferencing function that works for
> all Herbrand types:
> 
> :- func deref(<<any_herbrand_type>>).
> :- mode deref(any) = any is det.
> 
> deref(X) = ( if X = '$'(bound(Y)) then deref(Y) else X ).

OK, what you're describing is more of a WAM style variable
representation.  HAL uses PARMA bindings at the moment, do you have a
good reason for Mercury to use WAM bindings instead?

The advantage of the PARMA approach is that the case '$'(bound(Y)) never
occurs -- if the variable is bound then it is already dereferenced.
The only case where a dereference is necessary is where the variable is
unbound and is stored in a register or stack slot.  The PARMA chain can
only point to objects on the heap so a single step dereference will be
needed.

The main disadvantage of PARMA over the WAM approach is that it can
require more trailing.

> 
> A special unification predicate for t would be constructed
> automatically:
> 
> :- pred unify_t(t, t).
> :- mode unify_t(in(any), in(any)) is semidet.
> 
> unify would make use of deref/1 and have (safe) side effects if either
> of its arguments is bound to '$' or values containing '$'.  Its
> semantics are just what you'd expect.  Any side effects due to unify_t
> are trailed and will be undone on backtracking.

The HAL system also generates special construct and deconstruct
predicates for each data constructor of each type.  I assume this is
mainly for efficiency reasons -- we want to avoid having to do a general
unification if we have more specific information about the form of the
term.

> 
> CAVEATS
> 
> * SWITCHES
> 
> Any disjunction "switching" on a Herbrand value with inst any will be
> multi if the switch is exhaustive (i.e. tests for every data constructor
> except '$') and nondet if the switch is not exhaustive (i.e. misses
> tests for one or more of the data constructors other than '$').

I think this will require modification to switch detection and/or
determinism analysis to detect the `multi' case.

> * NEGATED CONTEXTS
> 
> Inst transitions of the form (any >> any) are forbidden inside negated
> contexts, with the special exception where a variable with inst any is
> unified with a variable with inst free (apparently this can happen
> fairly often with other source-to-source transformations.)
> 
> The reason for this is to prevent unsound situations like the following:
> say we define
> 
> p(X) :- not (X = g(_)).
> 
> If we start with Y bound to '$'(free) (i.e. Y starts off as a free
> Herbrand value) then
> 
> 	p(Y), Y = f
> 
> will succeed, but
> 
> 	Y = f, p(Y)
> 
> will fail.
> 
> * QUESTION ABOUT UNIFICATION
> 
> Does the Mercury compiler assume that X has inst ground or inst any
> after the unification X = f ?

The compiler will infer an inst of `bound(f)' which is a "sub-inst" of
ground.

> If not, is this an issue?
> 
> * QUESTION ABOUT THE INTERFACE
> 
> Should the interface to Herbrand types include impure non-logical
> predicates to test for groundness etc?
> 
> * QUESTION ABOUT OTHER SOLVERS
> 
> It seems to me that the herbrand_var type could be usefully extended to
> include a hook for other constraints (e.g. for finite domains.)  Is it
> the case that *all* other solver types should (reasonably) also be
> Herbrand types or not?

Most other solvers will _not_ be Herbrand types.  Often, a solver
variable is an integer representing an index into some sort of global
table.  E.g. see hal1/src/lib/cfloat.m for an example of an interface to
a CLP(R) solver, and hal1/src/solvers/domain.hal for an example of an
implementation of a FD solver.

> 
> Once we've got this hammered out, I'm tempted to start working on it.

Ok.  Looking forward to it!

David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 9373
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------