[m-users.] Existential higher-order type

[Volker Wysk]

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.


Bye
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/960aa691/attachment.sig>