[m-users.] Existential higher-order type

[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.

Zoltan.