[mercury-users] "some" and existential types

[Ralph Becket]

> From: Michael Day [mailto:mikeday at corplink.com.au]
> 
> I'm a little confused about this part. What exactly is the difference
> between these two declarations:
> 
> :- pred give_me_a_value1(T::out).
> :- some [T] pred give_me_a_value2(T::out).

If we make all quantification explicit, the first becomes

:- all [T] pred give_me_a_value1(T::out).

which says that for any particular T you (i.e. the caller) want, 
give_me_a_value1/1 will supply a value of that type.  I can't come
up with the proof off the top of my head (it was a good night) but
I suspect that any implementation satisfying this declaration will
not be well typed.  So this declaration doesn't make much sense.

The second one remains the same,

:- some [T] pred give_me_a_value2(T::out).

and says that give_me_a_value2/1 will provide a value of *some* type, but
it won't tell you what that type is.  So you (the caller) have to be
prepared
to handle *any* type that comes back.  Basically, it's a constraint that the
caller be polymorphic rather than the callee.

The classic idiom is

:- some [T] make_a_foo(T::out) => foo(T).

which will provide *something* that has the property foo - there may be
many such candidates (e.g. subclasses).

> Pardon my clumsy attempts to understand this topic, but 
> *cough* thanks to
> C++ I'm not used to things having polymorphic return types :(

You probably are!  C++ just doesn't make it explicit.  For example,
you might have an array of foo objects.  You can assign any subclass
instance of a foo to an element of this array.  When you project out
an element of the array you don't know whether you're getting a plain
foo or a subclass instance - all you know is that whatever you get will
have the properties of a foo.  That's all that the existential typing
and typeclass constraint is saying.

> One final question, which of the following is appropriate:
> 
> :- pred transform1(T::in, T::out) <= object(T).

This says that transform1/2 works on any T that satisfies object(T) (i.e.
is a member of the object/1 typeclass) and produces another thing of the
same type.  I think this is probably what you're after.

> :- pred transform2(T::in, T::out) => object(T).

>From the direction of the arrow this is implicitly existentially quantified
and, AFAIK, you need to make that explicit:

:- some [T] pred transform2(T::in, T::out) => object(T).

This doesn't make much sense to me.  What it says is that there is/are
*some*
T that are members of the object/1 typeclass for which this predicate is
defined.  You can't know ahead of time what that type is, so you can't
construct a value for the input argument.  Hence you could never write
correctly typed code that could call transform2/2.

> :- pred transform3(T::in, T::out) <= object(T) => object(T).

Again, you need to make the existential quantification explicit and then
the interpretation depends upon how you bracket things.



Here are the rules of thumb I use for type quantification.

(a) I want to `label' objects so that `keys' for one instance aren't used
to access another instance:

:- type store(T).			% c.f. store module.

	% Every time I call new_store/1, I'm magicking up a new type
	% for it that distinguishes this store from all the others.
:- some [T] pred new_store(store(T)::uo) is det.

	% I can generate `keys' that can only be used on a particular store.
:- type mutvar(T1, T2).

	% All operations on mutvar/2s will be carried out in association
with
	% the store/1 they belong to.  Thanks to existential typing, we
can't
	% use a mutvar from one store with another store since the T2s
wouldn't
	% agree.
:- pred new_mutvar(T1::in, mutvar(T1, T2)::out, store(T2)::di,
store(T2)::uo) is det.

(b) I just want a standard polymorphic predicate - I don't care what the
argument type is:

:- pred list__length(list(T)::in, int::out) is det.

(c) I want a predicate that operates on anything that implements foo
behaviour:

:- pred fooalise(T::in, ...) <= foo(T).	% Any colour you like as long as
it's foo.

I can require that they be both foo and bar:

:- pred foobaralise(T::in, ...) <= (foo(T), bar(T)).

(d) I have a predicate that is going to return an object of some type
that will implement foo, but other than that I want to keep the details
a secret:

:- some [T] make_a_foo(T::out) => foo(T).

<and I can do the same sort of thing as before if it's also going to be a
bar>

(e) If I want collections of things that are different types but all of
which
are foo, then I have to do something like this:

	% If I deconstruct an any_foo/1, all I know is that what I get out
	% will be a member of the foo typeclass - other than that, all bets
	% are off.
:- type any_foo ---> some [T] any_foo(T) => foo(T).
:- type foo_list == list(any_foo).

	% Adding a new item to my list...
	Xs1 = ['new any_foo'(AFoo) | Xs],
	% And adding another of a different type, but a member of foo...
	Xs2 = ['new any_foo'(ADifferentFoo) | Xs1],
	% Taking a member out...
	Xs2 = [any_foo(Thing) | _],
	% All I can say here is that Thing is a member of foo and that's it.

Hope this helps,

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