[m-dev.] Dependent insts

[Fergus Henderson]

On 10-Mar-1999, Thomas Charles Conway <conway at hydra.cs.mu.oz.au> wrote:
> 
> Consider the following program:
> 
> :- module dependent.
> 
> :- interface.
> 
> :- import_module io.
> 
> :- pred main(io__state, io__state).
> :- mode main(di, uo) is det.
> 
> :- implementation.
> 
> :- import_module string.
> 
> :- type (T/U) ---> (T/U).
> 
> :- inst isspecial = bound((
> 		(bound("builtin") / bound("int"))
> 	;	(bound("builtin") / bound("float"))
> 	;	(bound("builtin") / bound("character"))
> 	;	(bound("builtin") / bound("string"))
> 	;	(bound("std_util") / bound("univ"))
> 	)).

That should be illegal.  The fact that we currently
don't detect it is just a bug.

> It seems that for the compiler to distinguish alternatives in an
> inst, they must be discriminated by their top level functor.

Right.

> Is there any *technical* reason that the program above shouldn't behave
> as desired? I appreciate there may be a significant amount of
> implementation effort required to handle this kind of case.

I'm not sure if mode checking for dependent insts is decidable.

Anyway, supporting that kind of thing would be a major increase
in the complexity of the mode system, which is already quite complex.
Is that reason techical enough for you? ;-)

The complicated cases come where you have things like

	:- inst isspecial = bound((
			(bound("builtin") / bound("solutions"))
		;	(bound("float") / bound("plus"))
		)).

	:- mode p(out(isspecial)).
	:- mode q(out(isspecial)).

	p(X) :-
		q(X0),
		X0 = Y0/Z0,
		...
		X = Y0/Z0.

Here it's not sufficient to keep track of the inst of each variable;
because if you just look at the insts of Y0 and Z0, you can't tell
that X won't be bound to `"float"/"solutions"'.

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