[mercury-users] Higher-order unification question

[doug.auclair at logicaltypes.com]

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 ... I actually wished
to include modality and determinism annotations and have types match:

:- instance my_apply(pred(pred(A::out, B::in, C::out) is det, D::in, E::out, F::in, G::out) is det,
                                 pred(A::out, B::in, C::out) is det, pred(D::in, E::out, F::in, G::out) is det) where [
    my_apply(Pred, Arg) = (pred(P::in, Q::out, R::in, S::out) is det)
].

... so how do I create a typeclass and instance that say:

The composition of a pred of arity N+1 with a higher order pred first argument yields
a (curried) pred of arity N.

Sincerely,
Doug Auclair

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