[m-users.] Existential higher-order type

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

Peter
-------------- next part --------------
%-----------------------------------------------------------------------------%

:- module t.
:- interface.

:- import_module io.

:- pred main(io::di, io::uo) is det.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- implementation.

:- import_module list.

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

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

:- typeclass argument(T) where [].

:- instance argument(int) where [].

:- pred int_checker(int::in) is det.

int_checker(Arg) :-
    trace [io(!IO)] (
        print_line({"int_checker", Arg}, !IO)
    ).

:- instance argument(string) where [].

:- pred string_checker(string::in) is det.

string_checker(Arg) :-
    trace [io(!IO)] (
        print_line({"string_checker", Arg}, !IO)
    ).

:- pred test_checker(list(checker)::in, int::in, T::in, io::di, io::uo) is det
    <= argument(T).

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

main(!IO) :-
    List = [
        'new checker'(checker_pred(int_checker)),
        'new checker'(checker_pred(string_checker))
    ],
    test_checker(List, 0, 123, !IO),
    test_checker(List, 1, "abc", !IO),
    test_checker(List, 1, 123, !IO).

%-----------------------------------------------------------------------------%