[m-users.] Existential higher-order type

[Volker Wysk]

Am Dienstag, dem 11.10.2022 um 18:17 +1100 schrieb Zoltan Somogyi:
> 2022-10-11 18:11 GMT+11:00 "Volker Wysk" <post at volker-wysk.de>:
> > 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?
> 
> The call to dynamic_cast contains *one* predicate, not two:
> there is one in CheckerPred0, but not yet in CheckerPred. While you
> cannot unify two *existing* predicates, you can assign one existing predicate-containing
> term to an unbound variable. That is what dynamic_cast is doing, if the type test succeeds.


That's what I've figured out, see my other mail.

This means, that you can't unify two higher-order terms when the *types* are
higher-order. Even if it could be done, because one of them is a free
variable.

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