[m-dev.] Adding Herbrand types to Mercury

[Fergus Henderson]

On 24-Dec-2003, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> 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.

That's correct.

It would be possible to declare an additional mode for list.length

	:- mode length(in(list_skel(any)), out) is det.

which would allow that.

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

I think that would be right, if theorems-for-free applied.
But in Mercury they don't, due to construct.construct and the like.

> If so, does the compiler recognise this property?

No.

But even if it did, you still wouldn't be able to call list.length with a
list of Herbrand type values with inst any.  Recognizing the property
that you're talking about here would affect the inferred final insts of
the arguments to such a call, but the mode error when calling list.length
occurs when checking the initial insts for the call.

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

It seems like a reasonable thing to have.  But there are lots of
reasonable things to have, and if we supported them all, the language
would become very complex.  So I think we should only support this if
there is a strong motivation for adding it.  So far I haven't seen any
good motivating examples that show how it would be useful. 

(Your example of list.length doesn't help motivate this proposal, since
the example would still be invalid even if the proposal was accepted.)

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

I don't support this suggestion.  If we are going to make dynamically
typed term construction a distinguished feature, I think it would be
better to use a type class constraint to distinguish it, rather than
using "impure".  This feature does not violate referential transparency,
so there's no need to make it impure.  Declaring something to be impure
would for example prevent the compiler from doing common sub-expression
elimination on it.

If we're going to distinguish dynamically typed term construction,
then we should also distinguish dynamically typed term deconstruction,
since that too can "bugger up otherwise useful semantics".

Distinguishing both of those with a type class constraint (or with "impure")
would break backwards compatibility in a quite major way.  So I would be
inclined towards leaving this for version 2 of the standard library.

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

This should not throw an exception if the Herbrand values being compared
are actually ground.

> Now, it would be nice if unify_t/2 could be written in Mercury, but of
> course that would result in a circular dependency...

I don't see why. unify_t/2 is the generic unification routine for type t;
it can deconstruct the terms X and Y, and can call the generic unification
for the arguments of X and Y, without any circular dependencies.

If you use `if tag0(X) then ... else ...', then you may need to
explicitly cast the inst of X in the else case, in order to be able to
use deconstruction unifications to deconstruct it.

It might be better to write it as


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

where not_tag0 has a mode

	:- mode not_tag0(t :: any >> t_bound) is semidet.

and where the inst t_bound is an inst for t whose top-level inst is
`bound(...)' with all the functors for the type, and whose sub-insts
are all `any'.  For example, if the type `t' is given by

	:- herbrand type t ---> f(t1) ; g(t2, t3).

then the inst `t_bound' would be

	:- inst t_bound == bound(f(any) ; g(any, any)).

The original alternative would require something like

	unify_t(X, Y) :-
		(      if tag0(X) then ...
		  else if tag0(Y) then ...
		  else 
		  	X1 = t_promise_bound(X),
		  	Y1 = t_promise_bound(Y),
		  	... code to unify X1 and Y1 ...
		).

where `t_promise_bound' would be a no-op builtin with mode

	:- pred t_promise_bound(t :: ground >> t_bound) is det.

with `t_bound' defined as above.

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

I think it would be better to generate the clauses for unification/comparison
of Herbrand terms in unify_proc.m, where we generate the clauses for
unification/comparison of other types.

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

That seems reasonable.

I did the same for extras/trailed_update/var.m.

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

For that to work, I think comparison_result would need to be a Herbrand type
with delay.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------