[m-users.] Existential higher-order type

Volker Wysk post at volker-wysk.de
Mon Oct 10 23:40:27 AEDT 2022


Hi!

Is it possible to retrieve a higher-order type from inside a data
constructor, which has an existentially quantified type variable?

I have this:

:- type checker(Arg)
    ---> 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? 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.


Cheers,
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/20221010/f3f54fb7/attachment.sig>


More information about the users mailing list