[m-users.] Existential higher-order type

[Volker Wysk]

Am Dienstag, dem 11.10.2022 um 17:06 +1100 schrieb Peter Wang:
> On Tue, 11 Oct 2022 07:28:59 +0200 Volker Wysk <post at volker-wysk.de> wrote:
> > > > 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?
> 
> It means a type without type variables.
> 
> > 
> > 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.
> 
> Does the attached example help?

Yes, it does!

You're doing a double encapsulation, interesting... You've done it like
this:


:- type checker
    --->    some [T] checker(checker_pred(T)) => argument(T).

:- type checker_pred(T)
    --->    checker_pred(pred(T::in) is det).


test_checker(List, Index, Arg, !IO) :-
    list.det_index0(List, Index, Elem),
    Elem = checker(CheckerPred0),
    ( if dynamic_cast(CheckerPred0, CheckerPred) then
        CheckerPred = checker_pred(Pred),
        Pred(Arg)
    else
        print_line("dynamic_cast failed", !IO)
    ).


I don't understand why the unification "dynamic_cast(CheckerPred0,
CheckerPred)" works. It's between two checker_preds, which encapsulate a
higher-order type. Why isn't this an (unallowed) unification between higher-
order terms? Why doesn't the program look into those two checker_preds when
unifying them?

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/97f889de/attachment.sig>