[m-users.] Existential higher-order type

[Mark Brown]

> In the print_univ example

I meant to say that this is in Ralph Becket's tutorial.

On Tue, Oct 11, 2022 at 1:31 AM Mark Brown <mark at mercurylang.org> wrote:
>
> 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