[m-users.] Existential higher-order type

[Mark Brown]

On Tue, Oct 11, 2022 at 4:29 PM Volker Wysk <post at volker-wysk.de> wrote:
>
> Am Dienstag, dem 11.10.2022 um 07:21 +0200 schrieb 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))
>
> That's
>
> some [T] (pred(argdesc(Arg), T)) => argument(T))
>
> > And the inst should be:
> >
> > pred(in, in) is det

This is the part that didn't make sense to me, since it doesn't do
anything. I assumed you either meant semidet or that one of the
arguments was supposed to be an output. (FWIW, my solution was to use
dynamic_cast on an input, which would do the required check. This
didn't require further encapsulation.)

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

FWIW, my solution was to use dynamic_cast on an input, which would do
the required check. This didn't require further encapsulation.

> >
> > 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?
>
> I've looked at the definition of dynamic_cast. It's a synonym for
> private_builtin.typed_unify/2. So it won't work for me.
>
>
> Cheers,
> Volker