[mercury-users] "some" and existential types

[Ralph Becket]

> Right, thanks! That appears to be the concept I was having trouble
> wrapping my head around, I couldn't see the difference between the two
> types of polymorphism. Just to shift focus for a second to 
> the caller, how
> exactly do you demand a particular return type?

Glad to be of assistance.  With existential types, the caller can't place
*any* constraints on what the type of the returned object is going to be -
that's up to the callee.  At best the callee will tell you that the returned
object belongs to one or more particular typeclasses.

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

This wouldn't work in the sense I think you mean, where

:- some [T] pred give_me_a_value(T).			% Case I

since in this case the *caller* has imposed the type constraint X:list(T)
whereas the callee has made no such promise.  However, if we had

:- some [T] pred give_me_a_value(list(T)).		% Case II

then your code would be fine, it's just that you wouldn't be able to decide
ahead of time what the type of A is going to be.

There are some subtleties here.  In case II, give_me_a_value/1 is going to
return a list of objects, of some type T which you the caller can't work
out, *all* of which will be of type T.  So, if T turns out to be an int then
you'll get a list(int) back - but the fact that they're ints won't be
visible
to you (unless you try something using e.g. type_of/1, but that's a whole
other can of worms).  If I have

:- type anything ---> some [T] thing(T).

:- pred give_me_a_value(list(anything)).

then what I get back is a list of anythings, each of which can encapsulate
an object of a completely different type to all the others.  In this
situation
you really want to use a typeclass constraint so that you can actually *do*
something with these objects.  For example,

:- type anything ---> some [T] thing(T) => printable(T).

means you can do things like

foo :-
	give_me_a_value(Xs),
	print_anythings(Xs).

print_anythings([]) --> [].
print_anythings([thing(X) | Xs]) --> print(X), print_anythings(Xs).

The things in the list can all be different, but because of the typeclass
constraint give_me_a_value/1 promises that they will all have a print//1
method defined for them.

QUESTION FOR THE MERCURY SQUAD: can I write something like the following,

print_anythings(Xs) --> list__foldl(print, Xs).

I suspect not, because the print//1 method may be different in each case.
However, to disallow this sort of code would be a great shame, IMHO.  Not
sure what the solution is, assuming this is the case.



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

That's correct.

> Indeed, a very very informative post, thank you kindly! It 
> occurs to me
> that you've practically written a new chapter for your tutorial in
> replying, perhaps worth putting on the web so you can just refer the
> desperately unenlightened to an appropriate url? :)

Good plan - I really ought to get back to work on that...  Tragically
I scored zero in the completer-finisher category on the psychometric
test I took!

Cheers,

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