[mercury-users] existential constraints

[Fergus Henderson]

On 26-Jul-2000, Michael Day <mcda at students.cs.mu.oz.au> wrote:
> 
> Which of the following declarations is more correct:
> 
> :- all [S] some [T] ((pred foo(S, T) => c2(T)) <= c1(S)).
> :- mode foo(in, out) is det.
> :- mode foo(out, in) is det.		[wrong]
> 
> :- all [S] some [T] ((pred foo(T, S) => c2(T)) <= c1(S)).
> :- mode foo(in, out) is det.		[wrong]
> :- mode foo(out, in) is det.

The two type declarations are equally correct.

The two mode declarations that I have marked `[wrong]'
don't make sense for their respective type declarations,
since they give an existentially typed argument an input mode,
which is not possible, at least not for Mercury's current operational
semantics.  Think about it: if the argument is existentially typed, this
means that the _callee_ determines the type, but for the argument to be
input, the _caller_ must provide a value for that type (*before* calling
the callee).

Actually at one point we considered allowing what I think we called
"implied quantification", by analogy to implied modes: if in some
mode of a procedure an existentially typed argument has an input mode,
then treat it as universally quantified for that mode.  However, that
complicated things, was tricky to implement (if indeed it is possible
-- I haven't really analyzed it in depth), and we didn't see any
compelling need for it.  So we have basically shelved that one.  But
if you have some particular application where you think you might need
this, please let us know.

> Incidentally, will the 'new functor' syntax for existentially quanitifed
> data go away any time soon?

The syntax might change slightly, but it is not going to go away.

It would be nicer if the syntax was just "new functor" rather than
"'new functor'", and we might make that change at some time (it's a
fairly low priority item).  But the need to explicitly annotate
constructions of existentially quantified data types with "new" will
not be going away any time soon.

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