[m-users.] Existential higher-order type

[Mark Brown]

On Tue, Oct 11, 2022 at 6:42 PM Volker Wysk <post at volker-wysk.de> wrote:
>
> Am Dienstag, dem 11.10.2022 um 18:32 +1100 schrieb 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.
>
> The checker is supposed to check the value (second argument) and throw an
> exception if it is invalid.

I assumed you _weren't_ doing that. I think the reference manual
leaves this behaviour unspecified if a det predicate has no outputs
(i.e., it doesn't require that the exception is thrown), so that would
mean your code doesn't say what you intend it to, or the reference
manual doesn't say what we intend it to. Either way, I'd avoid it
personally.

>
>
> Bye
> Volker