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

[Fergus Henderson]

Mark Wielaard, you wrote:
> > > But why doesn't it say anything anymore about implied modes not being
> > > implemented?
> > 
> > That is because the current mode analysis does not propagate type information
> > into the modes; it does not know that `emp/4' is the only possible functor.
> > `emp_det' specifies that the functor must be emp/4, but `ground' does
> > not guarantee that.  I've attached a version of your code modified
> > to include the type information in the modes; for that code, you
> > gets a "sorry" rather than a mode error.
> > 
> > The error message could be improved; it might be clearer to say
> > "subtype error" rather than mode error.
> 
> Let me see if I get this. Combining the type employee with the mode out or
> more precise (free -> ground) should imply that the mode checker knows
> everything there is to know about the instantiatedness tree before and
> after the call to make_employee, but since the mode-checker doesn't
> combine them, you have to give this out(emp) mode (free -> emp), which
> gives the mode checker all the information it could have known if it
> combined modes with types. 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...)

> > > The reason I tried this example is because I wondered how I could indicate
> > > that a predicate doesn't use some parts of a structure.
> > > From these error messages I conclude that free -> free really means "free"
> > > and not "don't care".
> > 
> > Yes.  For example, the predicate is allowed to bind the variable
> > and then fail, e.g.
> > 
> > 	in_department(Department, emp(X,_,Department)) :-
> > 		X = "x",
> > 		fail.
> 
> This seems like a strange example.

Sure...

> I think I know why the compiler would
> allow this, because it knows the determinism of fail being failure, so it
> concludes that in_department has determinism failure also (It gives me a
> warning about that) and so the variable X is dead anyway. So it changes
> the code to (from hlds_dump): 
> 
> in_department(HeadVar__1, HeadVar__2) :-
> 	fail.

In this particular case, the compiler may be able to do that optimization.
But in general, if the unification with `X' is hidden away in a predicate
defined in another module, it may not be able to eliminate it.
(The predicate might loop, or call error/1, rather than failing, and
depending on the semantic model selected, the compiler may not be
allowed to optimize away such predicates.)

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

> > > So the compiler must generate code that constructs
> > > a whole new structure with real "free" variables in it to invoke my
> > > in_department predicate in the given mode. At the moment it doesn't do
> > > so, but I guess that is what it is supposed to do.
> > 
> > Right.
> > 
> > > That seems like a lot of work if my structure is really big.
> > 
> > Yep, so maybe it is not a good idea to support those sort of implied modes.
> > Perhaps we should change the message from "sorry, not implemented"
> > to "error".
> 
> Hmmm. But this isn't really an implied mode thing.

No, I disagree, it is an implied mode ting.

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

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

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

> Notice that this is also different from any -> any modes. Because there it
> could be a variable, but you can try to touch it anyway.

Another alternative might be to use a `clobbered_any -> clobbered_any' mode.
`clobbered' (a.k.a. `dead') does mean "don't touch me", so it might be
a better way of achieving what you want.

That doesn't quite work, though, because if you call a pred with that
mode, passing it an argument of inst `foo', then the compiler will
infer a final inst of `clobbered_any', not `foo'.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.