[m-users.] Existential higher-order type

[Volker Wysk]

Am Dienstag, dem 11.10.2022 um 09:11 +0200 schrieb 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?

I think I have figured it out. It's because CheckerPred is an free variable.
So this wouldn't work, because it's a unification of higher-order terms:

    dynamic_cast(CheckerPred0, checker_pred(Pred))

This means that dynamic_cast doesn't completely work like a (typed)
unification. For this:

    CheckerPred0 = CheckerPred,
    CheckerPred = checker_pred(Pred),
 
... the form ...
  
    CheckerPred0 = checker_pred(Pred)

would be the same. But it's different when using dynamic_cast. 

Is this correct?


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