[m-users.] Existential higher-order type

[Volker Wysk]

Am Dienstag, dem 11.10.2022 um 01:31 +1100 schrieb Mark Brown:
> Hi Volker,
> 
> On Tue, Oct 11, 2022 at 12:04 AM Volker Wysk <post at volker-wysk.de> wrote:
> > 
> > Sorry. Let me write this again:
> > 
> > Is it possible to retrieve a higher-order value (a predicate) from inside a
> > data constructor, when its type contains an existentially quantified type
> > variable?
> 
> Yes.
> 
> > 
> > I have this:
> > 
> > :- type checker
> >     ---> some [T] (
> >        checker( pred(T::in) is det ) => argument(T) ).
> > 
> > How can you call the predicate that is stored inside, provided it has the
> > expected type?
> 
> Just deconstruct it and call it :-)
> 
> (If you're getting an error from doing that, the problem might be elsewhere.)

Here's what I've tried. But this can't work:

   MChecker = yes({ checker(Checker), _ }),
   Checker(ArgDesc, Val)    % <-- line 1371

Here Val has the polymorphic type T. This is the declaration of my function
which tries to call that checker:

:- func arg_value(arguments(Arg), Arg) = T <= argument(T).

Because Val can have any type (within the type class), the call
"Checker(ArgDesc, Val)" can't work. I get this compiler error:

...
colipa.m:1371:   in argument 3 (i.e. argument 2 of the called predicate) of
colipa.m:1371:   higher-order predicate call:
colipa.m:1371:   type error: variable `Val' has type
colipa.m:1371:     some [T_2] (T_2),
colipa.m:1371:   expected type was
colipa.m:1371:     some [T_21] (T_21).
colipa.m:1371:   The partial type assignment was:
...

What I want to do, is to check if the types of the called predicate (a so-
called "checker") and the type of the "Val" variable match (such that Val
has the type of the existentially quantified first argument of the checker).
When the types match, the checker is to be run. When not, an exception is to
be thrown. 

This works well with my other, non-higher order, existentially quantified
value. The check is accomplished by calling private_builtin.typed_unify/2.
And it also supplies a variable of the right type, when the types match
(here "Val" isn't bound yet):

  % The argument has a default value.
  MDef = yes({ Default, _ }),
  (   if   private_builtin.typed_unify(Default, Val0)
      then Val = Val0
      else throw(ade_type_mismatch_default(ArgDesc, 
               type_desc.type_of(Default), type_desc.type_of(Val)))
  )

> > I want to do it inside a predicate that has a universally
> > quantified type variable T.
> > 
> > I have done something similar with a non-higher order type, and was able to
> > extract the value with private_builtin.typed_unify/2. (I've taken this from
> > the univ library.) This works.
> > 
> > But you can't unify two higher-order terms, so can the same be achieved
> > somehow for a higher-order type?
> 
> I'm guessing a bit what you're doing here, but the usage you're
> looking for is the one for univ_value, not univ_to_type. Here's the
> relevant signatures:
> 
> :- pred univ_to_type(univ, T).
> 
> :- some [T] func univ_value(univ) = T.

univ_to_value just does a deconstruction of the univ_cons/1 data
constructor. That's what I've done with "checker", see line 1370, above, but
it doesn't fit my case.

> The question is, do you want the caller to determine the type, or the
> callee? For univ_to_type, the caller determines the type and the
> implementation has to do a dynamic type check to make sure it matches
> the type stored in the univ - that's what typed_unify does. 

I want the caller to call the callee only when its own polymorphic type T
matches the type of the callee (see above). This means I need something like
typed_unify/2. 

You could say that both determine the type. This can't be done with
universally or existentially qualified types alone. You need runtime type
information and something like typed_unify.

> For
> univ_value, the callee determines the type and the caller would have
> to accept whatever type it was given (by only calling polymorphic
> things).
> 
> In the print_univ example, the last else branch could be written as:
> 
>     io.format("no idea... %s\n", [s(string(univ_value(U)))], !IO)
> 
> The other branches deal with specific types, but this one can deal
> with any type - univ_value/1 returns a value of _some_ type that is
> only known at run time, but that is okay because string/1 can accept
> values of _all_ types at run time.

Yes, I'm aware of this.

Thanks for your response.

Cheers,
Volker
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.mercurylang.org/archives/users/attachments/20221010/091ec61b/attachment.sig>