[mercury-users] existential constraints

[Fergus Henderson]

On 26-Jul-2000, Michael Day <mcda at students.cs.mu.oz.au> wrote:
> 
> > 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).
> 
> The compiler didn't seem to complain, the compiler in question being
> rotd-1999-11-23.

The compiler won't complain until you try to write a call to such a
procedure, but when you do, it will complain.

I suppose it would be possible for the compiler to issue a warning
when it compiles the procedure definition.  But currently it doesn't.

> > 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.
> 
> This is rather what I was thinking of.
>
> > 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.
> 
> Oh I see. Is this something that will one day change (post 1.0?) or must
> it remain for theoretical reasons beyond my ken?

The reason is that type checking needs to know whether it is
a construction or a deconstruction, since this determines whether
it is universally or existentially typed.  Type checking occurs
before mode analysis, so we can't rely on mode analysis to determine
whether it is a construction or deconstruction, we need some
explicit syntax.

It is possible that one day we might have a unified type/mode analysis,
rather than separating out those two phases.  With a unified analysis,
we could avoid the "new functor" syntax, support implied quantification,
and perhaps also support mode inference for lambda expressions.
However, this is easier said than done, and personally I don't think
it will happen 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
--------------------------------------------------------------------------