[mercury-users] "some" and existential types

[Fergus Henderson]

On 03-Oct-1999, Michael Day <mikeday at corplink.com.au> wrote:
> 
> Just to shift focus for a second to the caller, how
> exactly do you demand a particular return type?

As Ralph explained, if the predicate is existentially typed,
then the callee gets to choose the type, not the caller.
There is no way for the caller to demand a particular type,
except perhaps by passing some additional arguments to the
callee to guide the callee's choice.

> Would this work:
> 
> % no references to "X" before this point...
> 
> 	give_me_a_value(X),
> 	(
> 		X = [],
> 		...
> 	;
> 		X = [A|As],
> 		...
> 	),

If `give_me_a_value' is existentially typed,

	:- some [T] pred give_me_a_value(T).

then that would be a type error.

> If give_me_a_value is declared for some [T], then attempting to constrain
> it to a list would create semidet code that would not necessarily succeed?

We decided to make that a type error, rather than making it just
be something that could fail at runtime.  The reason for that is
basically related to unhappy experiences with Prolog ;-)
If we allowed that code as is, then it would require a dynamic type
check.  But our view is that dynamic type tests are something that
you want only rarely, and that if you really do want a dynamic type
test, then you should be a bit more explicit about it, e.g. using
the `univ_to_type' predicate from the `std_util' module
(or something along those lines),
rather than just using unification.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------