[mercury-users] Higher-order unification question

[Mark Brown]

On 27-Feb-2007, doug.auclair at logicaltypes.com <doug.auclair at logicaltypes.com> wrote:
> Dear Mark, you wrote:
> 
> >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>
> 
> While the example may work for simple function application of ground terms,
> I've been having difficulty formatting an instance of a pred that takes a higher
> order pred argument.  My attempted
> 
> :- typeclass my_apply(T1, T2, T3) <= (T1 ->T2, T3) where [
>     func my_apply(T1, T2) = T3
> ].
> 
> :- instance my_apply(pred(pred(A, B, C), D, E, F, G), pred(H, I, J), pred(K, L, M, N)) where [
>     my_apply(Pred, Arg) = (pred(P::in, Q::out, R::in, S::out) is det)
> ].
> 
> met with contempt by the compiler:
> 
> test_series.m:019: Error: types in instance declarations must be functors with distinct variables as arguments: my_apply(pred(pred(_1, _2, _3), _4, _5, _6, _7), pred(_8, _9, _10), pred(_11, _12, _13, _14)).
> 
> This error is strange to me, because all the variables /are/ distinct

Not all *arguments* are distinct variables, though.  The `pred(_1, _2, _3)'
argument is the showstopper in this case, since it isn't a variable.

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