[mercury-users] Idea for a currying library

[Fergus Henderson]

On 19-Jan-2000, Richard A. O'Keefe <ok at hermes.otago.ac.nz> wrote:
> 	> It would be very nice if mode &c inference for lambda-expressions were the
> 	> default, even when everything else was explicit.
> 	
> Fergus Henderson replied:
> 	Type inference for lambda-expressions is indeed the default.
> 	Mode and determinism inference for lambda expressions is something
> 	that the compiler just doesn't know how to do;
> 
> The cases we've been considering involve only a single goal.
> 
> If you have a single-goal predicate abstraction (or a single-application
> function abstraction) where some of the arguments are lambda-bound, the
> possible modes are constrained by the possible modes of the underlying
> predicate (function).  It's not obvious to me why the corresponding
> determinisms would not be identical to those of the underlying predicate
> (function).  Surely no new failures can be introduced?

That depends on exactly what you mean by a "single-goal predicate
abstraction".  Consider the following example:

	:- pred p(pred(int)) is semidet.
	:- mode p(pred(out) is semidet) is semidet.

	:- pred q(int::in, int::out, int::out) is det.
	
	example1 :-
		p(q(1, 2)).
	
	example2 :-
		p((pred(Z::out) is semidet :- q(1, 2, Z))).

If you mean cases like example1, then yes, what you say is true;
the determinism of a higher-order term like `q(1, 2)' must be
the same as the determinism of `q', i.e. `det' in this case,
and so since `p' expects something with determinism `semidet',
this example has a mode error.
But for cases like example2, your conclusion does not hold;
here the lambda expression has determinism `semidet', even
though `q' has determinism `det'; this example is well-moded.

But that's not the main problem with your suggested approach; the main
problem is that unlike predicates, lambda expressions can only have one
mode, not a set of modes.  The existing compiler does indeed
allow expressions like `q(1, 2)' if q has only one mode, and
correctly infers their determinism.  The problem comes only
if `q' has more than one mode.

Extending the language to allow lambda expressions to have sets
of modes is not easy; how would they be represented?  Note that the
representation must only depend on the type, not on the inst. Thus it's
difficult to support multiply-moded lambda expressions without having
a potentially significant impact on efficiency of higher-order code.

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