[m-dev.] Partial Instantiated structures (free -> free)

[Andrew Bromage]

G'day all.

Mark Wielaard wrote:

> > It means that the argument will still be free when the predicate
> > exits.  But it doesn't necessarily mean that the predicate won't
> > touch it, just that whatever bindings it makes will be undone by
> > backtracking before the procedure exits.
> 
> hmmm, that is stange. As I recall mercury doesn't use a trail, so how can
> it undo bindings on backtracking?

Using our implementation, the unbinding isn't physical, it's internal
to the compiler.  The compiler knows what is free and what is bound,
and will only bind something which it knows to be free.  For this
reason, we don't need a special representation of a free variable ---
any old junk will do.  On backtracking, the junk that the variable was
bound to is as good as any other junk, so no physical unbinding has to
take place.  However the _compiler_ has to record that an "unbinding"
took place so that it can bind the variable later if necessary.

I'm not sure how clear that was, now that I review it.

> This brings me back to the difference
> between predicates that cannot succeed and predicates that can.
> Here is another example:
> 
> :- interface.
> 
> :- pred destroy_success(int::free->free) is det.
> :- pred destroy_failure(int::free->free) is failure.
> 
> :- pred fail_it is failure. % Is just fail, but to fool the compiler.
> 
> :- implementation.
> 
> destroy_success(1).
> destroy_failure(1) :- fail_it.
> 
> fail_it :- fail.

> So what is the difference between these two predicates?

Look at the HLDS representation of destroy_failure again:

> destroy:destroy_failure(HeadVar__1) :-
>         HeadVar__1 = 1,
>         fail_it.

One feature of Mercury is that variables can be "artifically" bound or
unbound.  That is, if a goal has no solutions, it doesn't matter if the
instantiations of its variables don't match the expected instantiations.

We use it all the time in assertion-like code.  For example:

	( map__search(Map, Key, Value0) ->
		Value = Value0
	;
		error("Couldn't find the key")
	),
	use(Value)

It doesn't matter that Value isn't sufficiently instantiated in the
"then" part of the if-then-else, because that goal has no solutions.
So if you can "not sufficiently instantiate" a variable in a branch
which has no solutions, you can over-instantiate one too:

	% X is free at this point
	( map__search(Map, Key, Value0) ->
		Value = Value0
		% X is free here
	;
		X = 1,
		% X is bound here
		error("Couldn't find the key")
		% We never reach this point in the computation, so
		% X is dead here (internally, we call it not_reached)
	),
	% X is free here because in all computation paths which actually
	% get to this point, X is free.
	X = 42,		% This unification is det
	use(Value)

Does that help any?

Cheers,
Andrew Bromage