[m-users.] Higher order type with existential quanitfication

[Zoltan Somogyi]

On 2023-10-23 20:19 +11:00 AEDT, "Volker Wysk" <post at volker-wysk.de> wrote:
> Does that mean, that it's impossible to define a map_hetlist predicate like
> this:
> 
> :- type hetlist
>     ---> some [T] hetcons(T, hetlist)   => att(T)
>     ;    hetnil.
> 
> % declaration of map_hetlist?
> 
> map_hetlist(_, hetnil, []).
> 
> map_hetlist(Pred, hetcons(X, L), [Y|Ys]) :-
>     Pred(X, Y),
>     map_hetlist(Pred, L, Ys).

I cannot answer your question, because I don't know for sure what you intend
this code to do. The code tells me one thing about your intentions;
your description tells me another.

If you mean "can I give meaning to that exact code", yes, I can, but I don't know
whether it is the meaning you INTENDED to give that code. Also, Mercury
can't implement my meaning.

In that code, Pred has to be an input of map_hetlist, because it is
used as the predicate to call. The second argument, the hetlist, is similar
to a list of univ in that each element may have a different type. It is different
from a list of univs in that you know that each of those types is a member
of the att type class. Since this is all you know about the elements of the hetlist,
the only things Pred can do with X are

- call the operations of the att typeclass,
- call operations that work on values of *any* type, such as string.string.

And of course Pred can do those things in any combination it likes.
I can accept that as the meaning of those code. However, Mercury can't do so.

The problem, as you discovered, is that there is no way in Mercury to type
the first argument of Pred in your code. This is why map_hetlist_a below,
which is effectively your code, gets an error from mmc.

The version map_hetlist_b below, which is what I am recommending,
avoids this error by making the type of the first argument of Pred
just a defined type. This sidesteps the problem, and the compiler accepts this version.

Zoltan

:- module y.

:- interface.

:- import_module list.

:- typeclass att(T) where [].

:- type hetlist
    --->    some [T] hetcons(T, hetlist) => att(T)
    ;       hetnil.

:- pred map_hetlist_a(pred(X, Y), hetlist, list(Y)).
:- mode map_hetlist_a(in(pred(in, out) is det), in, out) is det.

:- type hetunit
    --->    some [T] hetunit(T) => att(T).

:- pred map_hetlist_b(pred(hetunit, Y), list(hetunit), list(Y)).
:- mode map_hetlist_b(in(pred(in, out) is det), in, out) is det.

:- implementation.

map_hetlist_a(_, hetnil, []).
map_hetlist_a(Pred, hetcons(Head, Tail), [Y | Ys]) :-
    Pred(Head, Y),
    map_hetlist_a(Pred, Tail, Ys).

map_hetlist_b(_, [], []).
map_hetlist_b(Pred, [Head | Tail], [Y | Ys]) :-
    Pred(Head, Y),
    map_hetlist_b(Pred, Tail, Ys).