[m-users.] Existential higher-order type

[Mark Brown]

Hi Volker,

On Tue, Oct 11, 2022 at 12:04 AM Volker Wysk <post at volker-wysk.de> wrote:
>
> Sorry. Let me write this again:
>
> Is it possible to retrieve a higher-order value (a predicate) from inside a
> data constructor, when its type contains an existentially quantified type
> variable?

Yes.

>
> I have this:
>
> :- type checker
>     ---> some [T] (
>        checker( pred(T::in) is det ) => argument(T) ).
>
> How can you call the predicate that is stored inside, provided it has the
> expected type?

Just deconstruct it and call it :-)

(If you're getting an error from doing that, the problem might be elsewhere.)

> I want to do it inside a predicate that has a universally
> quantified type variable T.
>
> I have done something similar with a non-higher order type, and was able to
> extract the value with private_builtin.typed_unify/2. (I've taken this from
> the univ library.) This works.
>
> But you can't unify two higher-order terms, so can the same be achieved
> somehow for a higher-order type?

I'm guessing a bit what you're doing here, but the usage you're
looking for is the one for univ_value, not univ_to_type. Here's the
relevant signatures:

:- pred univ_to_type(univ, T).

:- some [T] func univ_value(univ) = T.

The question is, do you want the caller to determine the type, or the
callee? For univ_to_type, the caller determines the type and the
implementation has to do a dynamic type check to make sure it matches
the type stored in the univ - that's what typed_unify does. For
univ_value, the callee determines the type and the caller would have
to accept whatever type it was given (by only calling polymorphic
things).

In the print_univ example, the last else branch could be written as:

    io.format("no idea... %s\n", [s(string(univ_value(U)))], !IO)

The other branches deal with specific types, but this one can deal
with any type - univ_value/1 returns a value of _some_ type that is
only known at run time, but that is okay because string/1 can accept
values of _all_ types at run time.

Hope that helps!

Mark

>
>
> Bye,
> Volker
> _______________________________________________
> users mailing list
> users at lists.mercurylang.org
> https://lists.mercurylang.org/listinfo/users