[m-dev.] Adding Herbrand types to Mercury

[Ralph Becket]

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.

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

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

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

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

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?

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

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