[mercury-users] Higher-order unification question

[Mark Brown]

On 26-Feb-2007, doug.auclair at logicaltypes.com <doug.auclair at logicaltypes.com> wrote:
> Dear Ralph, hello.
> 
> >> 	  Rnds = (pred(P::(pred(in, in, out) is det), A::in, B::out,
> >> 		       RNG0::in, RNG::out) is det :-
> >> 	          P(X, RNG0, RNG),
> >> 		  B = [X|A]),
> >> the call:
> >> 	  svunfold(counter(10), Rnds(random_int), [], Ans, J0, _),
> 
> you wrote:
> >Rnds has arity 5, svunfold expects a predicate of arity 4.
> 
> Rnds may have arity 5, but I'm trying to produce a predicate
> with arity 4 by binding the first argument and currying the 
> remaining arguments.  I see now, by rereading section 8.1
> again (that would be a third reading), that this doesn't work
> for higher order terms but it does work for ground pred type
> terms.

Yes, this is exactly the problem.

> So when Rnds becomes rnds/5:
> 
> :- pred rnds(pred(T, RNG, RNG), list(T), list(T), RNG, RNG) <= rng(RNG).
> :- mode rnds(pred(out, in, out) is det, in, out, in, out) is det.
> rnds(P, A, [X|A], !RNG) :- P(X, !RNG).
> 
> then the above code (s/Rnds/rnds/) now works.
> 
> Problem solved.  My misunderstanding.  However, it does seem a bit
> odd that higher-order currying is allowed, but not for ground higher
> order terms, which require (an extra) forwarding lambda term, what 
> is the need to make this a language specification requirement?
> 
> Would it be possible to allow currying of higher order terms and
> builtins (I found my (+)(1) function didn't work when I was mapping
> a list(int))?  I think allowing this would make higher order programming
> much easier to use (and to teach and to learn) in Mercury.

I agree this would be an improvement.  Fergus posted something a while ago
which gave the reason for the restriction, and also outlined how an
implementation could overcome this.  See:

<http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-users/mercury-users.200509/0024.html>

This mail was severely delayed by a broken mail server.  The original thread
started back here:

<http://www.mercury.cs.mu.oz.au/mailing-lists/mercury-users/mercury-users.200505/0021.html>

The short answer is that if we had a fully constraint-based type checker, the
implementation would be fairly straightforward.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------