[mercury-users] "some" and existential types

[Fergus Henderson]

On 02-Oct-1999, Michael Day <mikeday at corplink.com.au> wrote:
> 
> > Furthermore, the direction of the arrow(s) doesn't help in the case
> > where there are no type class constraints involved, because
> > in that case there are no arrows for the compiler to look at.
> 
> 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).

With the first declaration, the caller gets to choose the type.
With the second declaration, the _callee_ gets to choose the type.

> If the first declaration has an implicit "all", that would seem to imply
> it can return any type at all.

With the first declaration, the predicate has to work for _all_ possible types.
`T' can be any type at all, and the give_me_a_value/1 predicate does not
get to choose what `T' will be.

Here's some examples from the Mercury language reference manual:

     :- pred bad_foo(T).
     bad_foo(42).
        % type error
     
     :- some [T] pred e_foo(T).
     e_foo(42).
        % ok

Hopefully those examples illustrate this point.

> The second declaration has an explicit
> "some", which seems to imply it returns a particular subset of the
> available types? Does the compiler generate different code for these two
> cases, do they actually have a substantially different meaning?

Yes, they do have a substantially different meaning, see the examples above.

Yes, the compiler does generate different code for the two cases.
For each predicate, the compiler inserts additional arguments
corresponding to the type variables or type class constraints
in that predicates' type declaration.  For universally quantified
variables, the additional arguments have mode `in', but for
existentially quantified variables, the additional arguments
have mode `out'.

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

That one is fine, and it is the typical case.
The body of transform1 must work for any type T
which is an instance of the `object' type class. 
The caller can pass any type, so long as it is an
instance of the `object' type class.
The callee must work for whatever type the caller chose,
so basically the callee must treat the type passed as an abstract
type, accessing it only via the type class methods.

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

That type declaration is not useful.
Here `T' is universally qualified (since that is the default),
but the type class constraint `object(T)' is an existential constraint
(since you used `=>' rather than `<=').
Here's what the language reference manual says about
those kind of declarations:

 | In general, constraints that constrain any existentially quantified
 | type variables should be existential constraints, and constraints that
 | constrain only universally quantified type variables should be
 | universal constraints.  (The only time exceptions to this rule would
 | make any sense at all would be if there were instance declarations that
 | were visible in the definition of the caller but which due to module
 | visibility issues were not in the definition of the callee, or vice
 | versa.  But even then, any exception to this rule would have to involve
 | a rather obscure coding style, which we do not recommend.)

For this one, the caller can pass any type at all.
The definition of `transform2' must ensure that
the type T is an instance of the `object' type class,
even though the caller specifies what T is.

The only way that sort of thing could work is if
there was an instance declaration that declares that
_all_ types are an instance of the type class `object',
i.e.

	:- instance object(T) where [ ... ].

And the only time that sort of thing could be useful
is if that instance declaration is for some reason visible to
the body of `transform2', but not to the caller of `transform2'
(e.g. perhaps the instance declaration is private).

However, currently Mercury doesn't allow instance declarations
of that form.  The rules on instance declarations, which are
intended to prevent overlapping instance declarations, do
not allow the type in an instance declaration to be a type variable.

A more likely situation is a declaration of the form

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

Here the type `T' is existentially quantified, and the constraint
is also an existential one.  The effect of that one is that
the body of transform2b can define T to be any type that
is an instance of the `object' type class.
The caller must work for whatever type the callee chose,
so basically the caller must treat the type returned as an abstract
type, accessing it only via the type class methods.

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

First you need to correct the syntax problems.
The correct syntax for that is

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

The parentheses here are not optional (this is because of the
operator precedence based grammar: `=>' is a right-associative
operator, but here we want it to associate to the left, so we
need explicit parentheses).
Also note that the existential constraints must precede the
universal constraints.  (I just noticed that the reference manual
in our current release-of-the-day beta release has a mistake: it says
the opposite, that the universal constraints must precede the
existential ones.  That mistake will be corrected shortly.)

Anyway, even if you fix the syntax, that one is still useless.
It has the same semantics as the declaration for `transform1';
the only practical differences are that it is more verbose, and
the compiler implements it less efficiently.

The universal constraint `<= object(T)' says that the caller must
ensure that T is a member of the object class.  The existential
constraint `=> object(T)' says that the callee must ensure that
T is a member of the object class.
But the callee is always guaranteed that T is a member of that
class, since the caller already promised that.  So the extra
constraint here is useless.

Well, hopefully all that will make things a little clearer.

Cheers,
	Fergus.

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