[m-users.] Existential higher-order type

[Volker Wysk]

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


(...)
> > 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?

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
-------------- 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/2319f9f9/attachment.sig>