[m-dev.] Adding Herbrand types to Mercury

[Ralph Becket]

Hmm... some questions.

(1) If we have a list of Herbrand type values with inst any, then we
can't pass it to list.length because list.length expects a ground input
and ground, in this case, is a subinst of any.

I believe, however, that theorems-for-free tells us that a value passed
as an in mode (unconstrained) polymorphically typed argument cannot
have its inst changed by the called procedure.  out mode arguments of
the same type can be inferred to have the least general inst that
subsumes the insts of all in mode arguments of the same type (at the
call site.)

Is this true?
If so, does the compiler recognise this property?

It seems to me to be a sensible thing to have.

I'm aware that the ability to construct arbitrary terms rather throws a
spanner in the works.  My suggestion is therefore to make term
construction an impure operation on the grounds that it can bugger up
otherwise useful semantics.

(2) The proposed syntactic transformation is from

:- herbrand type t ---> ...

to

:- solver type t ---> ... where equality is unify_t, comparison is compare_t.

	% *Comment below.
	%
:- pred unify_t(t::in(any), t::in(any)) is semidet.

unify_t(X, Y) :-
	(      if tag0(X) then ...
	  else if tag0(Y) then ...
	  else ...unification for the given constructors...
	).

	% It doesn't make sense to compare two non-ground Herbrand
	% values (at least not until we add delay etc.)
	%
:- pred compare_t(comparison_result, t::in(any), t::in(any)) is det.

compare_t(R, X, Y) :-
	throw(software_error("attempt to compare two Herbrand values")).

	% Calls to t_init_any/1 are inserted during mode analysis to
	% ensure that solver type values have inst any instead of free
	% where necesary.  However, initialisation of all Herbrand
	% types is the same, hence generic_herbrand_init/1.
	%
:- pred t_init_any(t::out(any)) is det.

t_init_any(X) :-
	generic_herbrand_init(X).

Now, it would be nice if unify_t/2 could be written in Mercury, but of
course that would result in a circular dependency...  Can someone offer
advice on the best way to construct unify_t/2?

On a related note, it would be good to also have
unify_t_with_occurs_check/2 provided by the compiler.

(3) I assume that since this is a source-to-source transformation, it
should be handled in make_hlds.m?

(4) From the HAL paper on the subject, it seems that adding the delay
facility has a negligible impact on unification performance for Herbrand
types.  It occurs to me that we could profitably just make `herbrand'
mean "Herbrand type with delay" - splitting Herbrand types into
delayable and non-delayable seems like more work for little gain.

Indeed, delay can be used to make problems with comparison and
inequality go away.

Any opinions on that one?

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