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

[Mark Wielaard]

Hi,

> Mark Wielaard wrote:
> 
> > 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.

No, that's clear enough and I really like the term 'physical unbinding'.
This and the examples you give show me that I have a difficulty with how
the mercury compiler finds out what is junk. It is way to implicit to my
taste. Let's look at your examples and see how I would like it more
explicit expressing bindings.

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

This is a very good example because it is usefull code and you certainly
want to write something like that. My difficulty with it is that the else
branch doesn't do anything with the variable Value and you have to use
your knowledge about the fact that error is erroneous. I would like the
compiler to warn me that it assumes that IF the else branch succeeds THEN
Value is magically bound. It would help me a lot if there was a predicate
bind/1 which always succeeds and binds whatever its argument is (to
something bogus). This seems clumpsy, but it would fix the logic for me,
because I have no problem with: 

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

Because now I know whatever hapens I can be sure that Value is bound.
Even when error hapens to succeed one day.
Maybe it would be nicer if you had error/n where the first argument was
the string and the rest of the arguments are the variables that should be
bound after error succeeds - which would be never. So you would write
this as error("Couldn't find the key", Value).

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

This is an example which you would never write in real live. So I want the
compiler to barf on that X = 1, because that only makes sense if the else
branche does never succeed, so why would you want to write that anyway?

> Does that help any?
Yes, these real live examples are good to see how some features are
actually used (or aren't used). Please consider my suggestion for error/n,
I think it would make the logic much more clearer.

Thanks,

Mark!