[mercury-users] constrained polymorphic mode error

[Fergus Henderson]

On 16-Aug-2002, Tom Schrijvers <Tom.Schrijvers at cs.kuleuven.ac.be> wrote:
> On Mon, 12 Aug 2002, David Overton wrote:
> 
> > On Fri, Aug 09, 2002 at 08:14:18PM +0200, Tom Schrijvers wrote:
> > I've just committed a fix for this bug which should appear in the next
> > ROTD.
> 
> Yes, thank you, the bug is fixed in the rotd of 08-15-2002.
> 
> I have now run into another error message concerning contrained
> polymorphic modes in this unstable rotd.
> I think the real error  is the one saying that 'argument 1 became too
> instantiated'.

Yes.

> To me it looks similar to the previous bug, i.e. the
> expected instantiatedness is more general than the inferred one.
> Do you think this is a bug in the compiler or did I do something wrong?

This one is a complicated issue.
Your example touches a design issue which we have not yet
considered -- scoping of inst variables.  The specification (the
Mercury language reference manual) doesn't say what the right behaviour
is in this case.  In the short term I think we should clarify the
reference manual to match the compiler's current behaviour
(which would mean that it's not a bug ;-).
In the long term, however, we might change the specification
to make the language more expressive.

> closure2.m:066: In clause for `map(in(closure2:fun_closure((X =< ground),
> (Y =< ground))), in(closure2:val_closure(closure2:closure_list((X =<
> ground)))), out(closure2:val_closure(closure2:closure_list((Y =<
> ground)))))':
> closure2.m:066:   mode error: argument 1 became too instantiated.
> closure2.m:066:   Final instantiatedness of `V_20' was
> `bound(closure2:list((Y =< ground), bound(closure2:val_closure((pred((free
> -> bound(closure2:list((Y =< ground),
> bound(closure2:val_closure((pred((free -> ...)) is det)))) ;
> (closure2:nil)))) is
> det)))) ; (closure2:nil))',
> closure2.m:066:   expected final instantiatedness was `(X =< ground)'.

Here it is complaining about the actual/expected final inst in
the implicit lambda expression resulting from the partial application
of map in the clause body.

> :- mode map(in(fun_closure(X =< ground,Y =< ground)),
>             in(val_closure(closure_list(X =< ground))),
> 	    out(val_closure(closure_list(Y =< ground)))) is det.
> map(FC,CCL,RCL) :-
>    eval(CCL,CL),
>    ( CL = list(H,CTC) ->
>        apply(FC,H,NH),
>        NCTC = val_closure(eval2(map(FC,CTC))),	% line 66
>        RCL = val_closure(closure_list_list(NH,NCTC))
>    ;
>        RCL = val_closure(closure_list_nil)
>    ).

In this goal, the expression `eval2(map(FC,CTC))' is a partial application,
which is treated as an abbreviation for a lambda expression
with the modes and determinism being copied from the declaration
for `eval2'.  (Likewise, the sub-expression `map(FC, CTC)' is also a partial
application, and it turns out that there are similar problems there,
but `eval2' is the one that the compiler is complaining about.)

The mode of the argument of the implicit lambda expression for `eval2'
comes from the mode of the last argument of `eval2':

> :- mode eval2(pred(out(val_closure(X =< ground))) is det,out(X =< ground))
> is det.

Now, in this case, we have partially applied a polymorphically moded
procedure in such a way that the inst variable occurs both in the
applied arguments and in the remaining arguments.  That is going
to cause trouble, as you will see below, and so I think it warrants
at least a compiler warning.

But currently the compiler ignores this, and just
treats `eval2(map(FC,CTC))' as equivalent to
`pred(Arg2::out(X =< ground)) is det :- eval2(map(FC,CTC),Arg2)'.
Here X is treated as a fresh inst variable (i.e. not the
same as the inst variable X in the declaration of map),
whose scope is just the mode for this lambda expression,
and it is universally quantified (as are all inst variables in Mercury).

In other words, the mode it deduces for the implicit lambda
expression is one that would require it to be able to return
*any* ground inst chosen by the caller!
There's no way to satisfy that mode, except by never returning
(e.g. throwing an exception).

Hence you get a compile error.

Looking at the documentation for variable scoping in the Mercury
language reference manual, it documents scoping for ordinary variables
and for type variables, but not for inst variables... since at the time
that documentation was written, Mercury didn't support inst variables.
Obviously that is something which we should have updated when we were
adding polymorphic modes.

But in the current Mercury implementation, inst variables only
scope over a single `:- mode' or `:- inst' declaration;
the insts variables in a predicate's mode do not scope over
any inst variables in lambda goals in the predicate's body.
Likewise inst variables in a lambda goal's mode only
scope over the mode of that lambda goal, not over any inst
variables contained in nested lambda goals.

That means inst variables in a lambda expressions's mode can only be
bound when that lambda expression is called, not when it is constructed.

(Making inst variables scope over mode declarations in lambda goals
is arguably somewhat inconsistent with our approach for type variables,
which scope over `with_type' declarations in procedure bodies.
However, that's what happens.)

To make code similar to your example work, I think that would need to
change.  You need a way to bind inst variables when a lambda expression
is constructed.  However, implementing that would require sustantial
changes to the Mercury compiler, I suspect.

If that change were made, then I think your example would work
if rewritten to use explicit lambda expressions (rather than
partial application), with appropriate mode for the lambda
expressions:

:- mode map(in(fun_closure(X =< ground,Y =< ground)),
            in(val_closure(closure_list(X =< ground))),
	    out(val_closure(closure_list(Y =< ground)))) is det.
map(FC,CCL,RCL) :-
   eval(CCL,CL),
   ( CL = list(H,CTC) ->
       apply(FC,H,NH),

       %
       % Instead of `NCTC = val_closure(eval2(map(FC,CTC)))':
       %
       Map = (pred(H3::out(val_closure(closure_list(Y =< ground)))) is det :-
       		map(FC,CTC,H3 )),
       Eval2 = (pred(H2::out(closure_list(Y =< ground))) is det :-
		eval2(Map, H2)),
       NCTC = val_closure(Eval2),

       RCL = val_closure(closure_list_list(NH,NCTC))
   ;
       RCL = val_closure(closure_list_nil)
   ).

In the short term, if you are looking for work-arounds, then I have
two suggestions.  First, I think you might find that you can avoid the
need for polymorphically modes if you use higher-order functions rather
than higher-order predicates, thanks to our recent changes to the
semantics of higher-order function insts.  (See the NEWS file in
the rotd for details.)

Second, if all else fails, you can always use an ``inst cast''.  Although
Mercury has no built-in support for inst casts, they can be trivially
implemented using the foreign language interface -- see `inst_cast'
in browser/interactive_query.m in the Mercury source distribution for
an example.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------