[m-dev.] for review: polymorphic ground insts

[Fergus Henderson]

This email is summarizing a brief discussion that David and I had.

On 13-Oct-2000, David Overton <dmo at cs.mu.OZ.AU> wrote:
> On Tue, Oct 10, 2000 at 10:43:59PM +1100, Fergus Henderson wrote:
> > On 29-Sep-2000, David Overton <dmo at cs.mu.OZ.AU> wrote:
> > > It's been a long time, but I've finally got back to this and got it
> > > working.  I've fixed the problem with existential types
> > 
> > Well, I'm not really convinced that this change handles existential
> > types consistently with the way it handles non-existential types.
> > But if it is only the corner cases that it mishandles, and these cases
> > occur rarely or not at all in practice, and the symptom is just that
> > the mode checker rejects the program, and the code in question (in
> > maybe_get_cons_id_arg_types in modes.m) is marked with an XXX, then I
> > think it is OK to commit it.
> > 
> > The situations I'm worried about are things like
> > 
> > 	:- type t ---> some [T] f(T).
> > 	:- inst t ---> f(ground).
> > 
> > 	:- pred p(t::in, t::out(t)) is det.
> > 	p(X, X).
> > 
> > Is this allowed?
> 
> This case will work fine.
...
> The problematic case would be if you change the definition of the inst
> `t' to something like
> 
> 	:- inst t ---> f(bound(....)).
> 
> There is no way of checking whether this bound ints contains all the
> functors for the existential type T.

That case is fine -- it would be quite reasonable for the compiler to
reject the code in that case.

The case which I think the code that you posted gets wrong is
where the existentially quantified constructor has some arguments
whose types are not existentially quantified, e.g.

 	:- type t ---> some [T] f(int, T).
 	:- inst t ---> f(bound(1), ground).
 
 	:- pred p(t::in, t::out(t)) is det.
 	p(X, X).

Another related case is when the argument types are not existentially
quantified type variables, but instead just _contain_ existentially
quantified type variables, e.g.

	:- type g(T) ---> g(T).
 
 	:- type t ---> some [T] f(g(T)).
 	:- inst t ---> f(bound(g(ground))).

 	:- pred p(t::in, t::out(t)) is det.
 	p(X, X).

Anyway, these are corner cases; it would be OK to commit as is,
just so long as the code in question is marked with an XXX.

-- 
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-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------