[mercury-users] "some" and existential types

[Fergus Henderson]

On 01-Oct-1999, Michael Day <mikeday at corplink.com.au> wrote:
> 
> <huge snip of informative post>
> 
> hmm that makes sense, but I don't quite understand, why the some is
> necessary at all. It seems that these two declarations are symmetrical:
> 
> :- pred take_object(T) <= object(T).
> :- mode take_object(in).
> 
> :- pred give_object(T) => object(T).
> :- mode give_object(out).

Yes, strictly speaking, the `some' is not necessary;
for cases involving type class constraints, the direction of the
arrow(s) would be sufficient information for the compiler to infer
which types were existentially quantified.

However, if the direction of the arrows was the only syntactic clue
as to whether something was existentially typed or not, then
it would be easy for a human reader to miss that fact.
Having an explicit `some' to let the human reader know that the code
uses existential types makes the code more readable, IMHO.

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.

> In fact now that I look at it, why even are two different arrows <= and =>
> required? They do not seem to convey any information that the compiler
> does not already have, if they are used purely to distinguish input and
> output arguments.

You're right: conversely to the point above, if an explicit `some' is always
required for existentially quantified types, then the compiler could easily
infer which arrow is needed.  For a constraint c(T1, T2, ..., TN), if any
of the Ts are existentially quantified, then the constraint should use "=>",
otherwise it should use "<=".

The rationale for using different symbols here is that they represent
different things.  "<=" imposes a requirement on the caller, whereas "=>"
imposes a requirement on the callee.  That's an important distinction,
so it should be reflected in the syntax.

> Is this syntax set in stone

No, not yet.  But people have written code using this feature,
so any changes at this point would require a fairly compelling rationale.

Once the next major release comes out, then it will be pretty much set
in stone.

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