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

[Mark Wielaard]

On 20 Oct 1997, Lee Naish wrote:

> 
> A couple of thoughts about this issue.
> 
> One "traditional" way of expressing the fact that certain things are
> "untouched" is to uses polymorphism at the type level.  By defining
> employee as follows
> 
> :- type employee(N,A,P)
> 	--->	emp(
> 			N,		% name
> 			A,		% age
> 			P		% department
>  		).
> 
> we could use the type employee(string,int,string) for code which might
> use all components and the type employee(X,Y,string) for code which only
> uses the department.  I'm not sure if this technique would work (in this
> case) in Mercury. 

Yes, this is indeed why I came up with the example in the first place. I
thought I could make a comparison between this "traditional" way and the
instantiations used in Mercury. You could than view a polymorphic type
variable as an instance free -> free. But this does not quite work since
free means 'not bound'. But this seems to be to strict a definition for
free, because as you can see in the above example if you have a very
big datastructure you then need either a lot of mode declarations (for
which the code generator probably generates all the same code) or you need
'implied modes' which means copying the whole data structure and inserting
free variables at the right places.

> In the declarative view of modes, mode checking is equivalent to
> checking the success set is a subset of the "mode set", thus making use
> of failure information makes sense for mode checking.  Using this
> information, in general, allows more precise mode checking.  However, it
> is reasonable for a language such as Mercury to impose additional
> constraints on modes (as well as being well moded from a declarative
> view, there will be additional restrictions) or not use all possible
> information to prove well modedness.  I think the "error" example is a
> strong argument in favour of using failure information in the mode
> checking algorithm.  Only using failure information from certain
> predicates (eg error) would solve some of Mark's objections to the
> current algorithm but I think such things tend to be frustrating in the
> longer term (you define things which are equivalent to certain builtins
> but can't convice the compiler to accept them, etc). 

Yes, Fergus also convinced me that error/n is not the way to go. I am now
convinced that you will need to use failure information some of the time.
But I am not yet convinced that the way Mercury uses this information is
correct. A nice example is given by Fergus (again) in his reply to Thomas
his code for parallel conjunctions:

> Hmm, what about examples like
> 
> 	:- pred p(out) is det.
> 	p(X) :-
> 		(
> 			X = a,
> 			...
> 			error("blah")
> 		&
> 			X = b,
> 			...
> 		).

Which seems to suggest that X isn't going to be bound in the first
conjunct. (We use our knowledge about the failure information of error to
prove that.) But of course if we would do this in parallel we have a big
problem, both conjects will try two overwrite X.

> One approach is to explain well-modedness in two steps: programs are
> well moded if <some relatively simple condition> holds; they are also
> well moded if <some more complex condition involving failure holds>.  It
> may be that the first case is sufficient nearly all the time. 

I will try to come up with such an approach. In my thesis I will try to
make a lot more than two steps though :-)

Cheers and thanks for all your comments,

Mark!