[m-dev.] Adding Herbrand types to Mercury

Ralph Becket rafe at cs.mu.OZ.AU
Tue Dec 16 17:40:31 AEDT 2003

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


The aim would be to allow type declarations like the following in the

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

:- type herbrand_var(T)
	--->	free
	;	bound(T).

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

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.


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.

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

A special unification predicate for t would be constructed

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



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 '$').


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.


Does the Mercury compiler assume that X has inst ground or inst any
after the unification X = f ?

If not, is this an issue?


Should the interface to Herbrand types include impure non-logical
predicates to test for groundness etc?


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?

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

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

More information about the developers mailing list