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

[Volker Wysk]

Am Montag, dem 23.10.2023 um 20:53 +1100 schrieb 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.

I have a database application and made semantic wrappers for the attributes
of my database tables. I wanted to be able to pass a list of such attributes
to, for instance, a generic "select" predicate. So I wanted to put them in a
heterogenous list. The attributes have typeclass member functions for
converting the wrapped value to SQL, and similar things.

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

Your meaning is correct. That's what I'm trying.

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

A moment ago, I found a different solution:

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

:- pred map_hetlist(
    pred(wrp, Y)::in(pred(in, out) is det),
    hetlist::in,
    list(Y)::out)
is det.

map_hetlist(_, hetnil, []).

map_hetlist(Pred, hetcons(X, L), [Y|Ys]) :-
    Wrp = 'new wrp'(X),
    Pred(Wrp, Y),
    map_hetlist(Pred, L, Ys).

But your map_hetlist_b is preferable, because it doesn't need a heterogenous
list. A normal list can be used and all the list operations from the
standard library are available.

Thanks!
Volker