[m-users.] Existential higher-order type

[Volker Wysk]

Am Dienstag, dem 11.10.2022 um 05:05 +1100 schrieb 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.

I've simplified it. Here's the full story:

:- type checker(Arg)
    ---> some [T] ( checker( 
       pred(argdesc(Arg)::in, T::in) is det ) => argument(T) ).

:- type argdesc(Arg)
    ---> some [T] argdesc(
        argdesc_arg :: Arg,
        argdesc_valname :: maybe({ maybe(string), property(Arg) }),
        argdesc_long :: list(string),
        argdesc_short :: list(char),
        argdesc_default :: maybe({ T, property(Arg) }),
        argdesc_min :: maybe({ int, property(Arg) }),
        argdesc_max :: maybe({ int, property(Arg) }),
        argdesc_checker :: maybe({ checker(Arg), property(Arg) }),
        argdesc_env :: maybe({ string, property(Arg) })
    ).

And the call:

         MChecker = ArgDesc ^ argdesc_checker,
         (
             MChecker = yes({ checker(Checker), _ }),
             Checker(ArgDesc, Val)
         ;
             MChecker = no
         )

So, the type of the "Checker" variable should be:

some [T] (pred(argdesc(Arg), T) is det ) => argument(T))

And the inst should be:

pred(in, in) is det

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

Hmm...  Here's the declaration of dynamic_cast:

    % dynamic_cast(X, Y) succeeds with Y = X iff X has the same ground type
    % as Y (so this may succeed if Y is of type list(int), say, but not if
    % Y is of type list(T)).
    %
:- pred dynamic_cast(T1::in, T2::out) is semidet.

What's a "ground type"? What does it do, except for a unification?



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

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/20221011/55ea75fb/attachment.sig>