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

[Mark Wielaard]

On Sun, 19 Oct 1997, Fergus Henderson wrote:
>
> Mark Wielaard, you wrote:
> >
> > So a natural question to ask is: Why doesn't
> > the mode checker combine types and modes? 
> 
> Well, the first time I tried doing that, it caused performance problems.
> 
> Since then, we've fixed some performance bugs in mode analysis,
> so it may be that trying it now would not cause problems.
> (Volunteers welcome...)

<Grin> I am still a bit intimidated by the mercury compiler, but since I
have to do something like that for my project anyway, ask me again after I
have finished that :-)
 
> > - To be honest I wouldn't call this well-moded if I hadn't any determinism
> > information, but if you have determinism information than you can call it
> > well moded. Every mode declaration would be well-moded if you know that
> > the predicate never succeeds. -
> 
> It is not determinism information, it is "cannot-succeed" information --
> which is a subset of determinism information.

Yes, you are right. But now there seems to be a difference between
predicates that cannot succeed and predicates that can succeed. I will
give an example later.

> > Implied modes come from free -> ground things which you give something
> > which is ground.
> 
> That's a specific instance of implied modes.
> But in the general case, implied modes come from A -> B things called with
> an actual inst A', where A' is more instantiated than A.

Much better definition, thanks. I see now why I don't get it, because I
would think that to much instantation on procedure call wouldn't be a
problem. It would be a problem though if the actual inst A' indicates that
something is bound that goes from free to bound as indicated by A -> B.

Let's give an example.

:- mode length(in(listskel), out).
(Or :- mode length(listskel -> listskel, free->ground).)
length([], 0).
length([_|T], L+1) :-
	length(T,L).

Calling length like: length([1,2,3], X). Would be OK, the list is more
instantiated then required, but that is OK, length will not touch the
elements. (It will only try to unify it with a 'free' variable.)

But calling length([1,2,3], 3) would not be OK (or require an 'implied
mode'), because 3 is already bound and out (free -> ground) indicates that
it gets more bound.
 
> > If I have something which is free -> free I think that should mean that
> > here is (some part of) an argument that this predicate will not touch.
> 
> 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? 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?
destroy_success isn't accepted by the compiler:
destroy.m:018:   mode error: argument 1 became too instantiated.
But destroy_failure is!

The final hlds gives:

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

(OK, OK, you have to give it a -O -1 to disable all optimizations, because
otherwise it optimizes the assignment away. BTW it would be nice to know
what kind of unification the = represents, I am pretty sure this is an
assignment unification, but how can I be sure while looking at the hlds?)

This is strange, why can destroy_failure touch this variable and
destroy_success not? They should both be forbiden to touch the free->free
thing. (My opinion, you could of course also say that they should both be
allowed to touch the variable, it is free so garbage, do what you like
with it.)

> > What I want is that if I say
> > here is a mode that is free -> free, then it cannot rely on that (part of)
> > the argument (because it could be free) and it cannot bind it either
> > because it shouldn't be touched (It is free from touching).
> 
> Well, that may be what you want, but that's not the way the mode system
> currently works.
> 
> I suppose it might be possible to change the mode system to disallow
> examples like the one I gave.  But I think that would require some
> significant changes; I'm not yet convinced that the benefits would
> outweigh the gains.

(Can you really say "the benefits would outweigh the gains"?)

You are right, I described how I would like the mode system to be, not
what the mode system currently does. But I hope you are convinced by the
above examples that there is something strange with the current definition
of well-modedness (or that you are at least convinced that I still don't
get it). I don't know if my view of what should be well-moded isn't just
as strange for some examples. (But at least I think I get it :-)

Cheers,

Mark!