[m-users.] Existential higher-order type

Volker Wysk post at volker-wysk.de
Tue Oct 11 00:04:04 AEDT 2022


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?

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


Bye,
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/83518bc2/attachment.sig>


More information about the users mailing list