[mercury-users] "some" and existential types

[Ralph Becket]

> when declaring a predicate that outputs an instance of a particular
> typeclass as follows:
> 
> :- some [T] pred get_object(T) => object(T).
> 
> why is the "some [T]" necessary? I would have thought that the typeclass
> constraint would be sufficient in this case; what role does the "some"
> fill?

In a sense it's all down to who decides what the argument type is.  If I
have

:- all [T] pred get_object(T) <= object(T).

then I am saying that get_object/1 is defined over all T that satisfy
object(T).  In other words, the *caller* gets to decide what type the
argument is and get_object/1 has to be able to handle it.  This is
standard type polymorphism and the quantification is usually left implicit.

If, on the other hand, I write

:- some [T] pred get_object(T) => object(T).

then I am saying that get_object/1 is defined for *some* (unpublished)
types T that also satisfy object(T).  Since the caller cannot know ahead of
time what T are acceptable, the only sensible interpretation is that
get_object/1 (the callee) gets to decide what the type of its argument is
and the caller has to be able to handle whatever that T turns out to be
(i.e. it must polymorphic in that argument).

A consequence of this is that it only really makes sense to existentially
quantify output arguments.  An example of how this can be used is to prevent
keys from one database being inadvertently used to access another database:

:- type db(T, U).
:- type key(T).

	% T is used to uniquely identify a particular DB instance.
	% U is the type of objects stored inside the DB.
:- some [T] pred new_db(db(T, U)).
:- mode new_db(out) is det.

	% If we add a new record to the DB then we get a key tied
	% to that particular DB.  This key can only be used to access
	% this particular DB since different DBs will have different Ts.
:- pred add_record(U, db(T, U), key(T), db(T, U)).
:- mode add_record(in, in, out, out) is det.

:- pred lookup_record(key(T), db(T, U), U).
:- mode lookup_record(in, in, out) is det.

Of course, things get really cool when you start mixing in typeclasses.

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