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

[Volker Wysk]

Am Montag, dem 23.10.2023 um 19:56 +1100 schrieb Zoltan Somogyi:
> On 2023-10-23 19:32 +11:00 AEDT, "Volker Wysk" <post at volker-wysk.de> wrote:
> > Am Montag, dem 23.10.2023 um 19:17 +1100 schrieb Zoltan Somogyi:
> > > On 2023-10-22 22:54 +11:00 AEDT, "Volker Wysk" <post at volker-wysk.de> wrote:
> > > > I have a predicate which takes an existentially quantified type as one of
> > > > its arguments.
> > > 
> > > By this, I presume you mean a predicate that *returns*
> > > a value of an existentially quantified type.
> > 
> > No, it should take an existentially quantified value as its input argument
> 
> This does not make sense. This is from section 12.1.2 of the language reference manual
> (latest rotd version), titled "Semantics of type quantifiers:
> 
>   If a type variable in the type declaration for a polymorphic predicate or function is universally quantified,
>   this means the caller will determine the value of the type variable, and the callee must be defined
>   so that it will work for all types which are an instance of its declared type.
> 
>  For an existentially quantified type variable, the situation is the converse: the callee must determine
>   the value of the type variable, and all callers must be defined so as to work for all types
>   which are an instance of the called procedure’s declared type.
> 
> This means that for an existentially typed input argument, if one existed,
> 
> - the caller would determine its value before the call, and
> - the callee would determine its type during the call.
> 
> Since in Mercury, you cannot choose a value without choosing a type,
> this cannot happen.
> 
> I suspect we are talking past each other because you use "existentially quantified type"
> to mean something other than its standard definition. Neither I nor anyone else can help you
> until you help us to understand what your question means. (For example, quantification
> applies to type *variables*, but the type of Pred is not a type variable. It *contains*
> type variables, but that is a different issue.)
> 
> I would also draw your attention to the start of section 12, which says:
>   
>   Mercury supports existential type quantifiers on predicate and function declarations, and in data type definitions
> 
> Note that it says you can put existential type quantifiers on pred and func declarations,
> but does not say that you can put them on the argument types inside them,
> and in fact, as you discovered, you can't. It is not a matter of syntax; it is a matter of
> what constructs the language does and does not support.

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 half understand you. But let me try hard to understand by myself, before
you write another long answer.


Thnx,
Volker