Partial Instantiated structures (free -> free)

[Mark Wielaard]

Hi all,

Fergus and I had a discussion on mercury-bugs about partial instantiated
structures and (free -> free) modes, but maybe mercury-developers is a
better place to discuss this. (And Fergus send me a fix for the bug that
triggered this discussion almost immediately, so I cannot longer use
mercury-bugs ;-) Please flame me if you don't agree. 

Maybe this is all because I don't get the difference between an
instantiation and modes being a pair of instantiations, but here comes the
original discussion and more questions. (The program it is all about is at
the end.) Any help in understanding this better would be appreciated.

On Sun, 19 Oct 1997, Fergus Henderson wrote:

> Mark Wielaard, you wrote:
> > 
> > And now for the question(s):
> > 
> > Replacing the line
> > 	Mark = emp("Wielaard", 24, "Sales"),
> > with the line
> > 	make_employee("Wielaard", 24, "Sales", Mark),
> > always gives an error:
> > emp.m:038: In clause for `mark':
> > emp.m:038:   in argument 2 of call to predicate `emp:in_department/2':
> > emp.m:038:   mode error: variable `Mark' has instantiatedness `ground',
> > emp.m:038:   expected instantiatedness was `emp:emp_dept'.
> > 
> > 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? 

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

Which would even be mode correct if fail would not fail! Because on exit
it hasn't bound any things in the instantiatedness tree that should be
free. (Actually it hasn't bound any things that it should bind either, but
then again fail never succeeds :-)
- 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. -

> > 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.
Implied modes come from free -> ground things which you give something
which is ground. Then you transform a program so that it gives the
predicate a new fresh variable and then check that this new variable is
bound to the same term as your original ground term.

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
will not look at it and it will not bind 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).

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.

I believe that if we regard (free -> free) as cannot look at this thing
and in the end I will not have touched this, then we (well someone :-) can
generate code for it that acts correctly wheter or not that term is a
variable.

Cheers,

Mark!

> :- module emp.
> 
> :- interface.
> 
> :- type employee
> 	--->	emp(
> 			string,		% name
> 			int,		% age
> 			string		% department
> 		).
> 
> :- inst emp
> 	--->
> 		emp(
> 			ground,
> 			ground,
> 			ground
> 		).
> 
> :- inst emp_dept
> 	--->
> 		emp(
> 			free,
> 			free,
> 			ground	% Only department is needed
> 		).
> 
> :- pred make_employee(string, int, string, employee).
> :- mode make_employee(in, in, in, out(emp)) is det.
> 
> :- pred in_department(string, employee).
> :- mode in_department(in, emp_dept -> emp_dept) is semidet.
> 
> :- pred mark is semidet.
> 
> :- implementation.
> 
> make_employee(Name, Age, Department, emp(Name, Age, Department)).
> 
> in_department(Department, emp(_,_,Department)).
> 
> mark :-
> 	make_employee("Wielaard", 24, "Sales", Mark),
> %	Mark = emp("Wielaard", 24, "Sales"),
> 	in_department("Sales", Mark).
> 
> :- end_module emp.