[m-users.] Existential higher-order type

[Mark Brown]

On Tue, Oct 11, 2022 at 2:27 AM Volker Wysk <post at volker-wysk.de> wrote:
>
> Am Dienstag, dem 11.10.2022 um 01:31 +1100 schrieb Mark Brown:
> > > 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

What's the type and inst of Checker? It doesn't match the declaration you gave.

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

You can use dynamic_cast for this sort of thing, but I can't say where
without knowing how you've declared the checker.

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