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

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

Zoltan.