[m-rev.] for discussion: subtypes documentation

[David Overton]

On Mon, Nov 25, 2002 at 07:28:15PM +1100, Fergus Henderson wrote:
> On 25-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > The mode system uses covariant subtyping for the
> > final insts and contravariant subtyping for the initial insts.
> > Using covariant subtyping for the initial insts would be unsafe.
> > 
> > Hmm, looking at the source, I see that although we use contravariant
> > subtyping for inst_matches_final, like we should, currently we are
> > using covariant subtyping for inst_matches_initial.  Ouch -- that looks
> > like a bug... 
> > 
> > Yep, it sure is.  I just got it to seg fault when running an example
> > program.  (See attached.)
> 
> Actually, looking more closely at the source, I see that in fact
> inst_matches_initial uses *invariant* subtyping for the initial
> insts of higher-order insts.  pred_inst_matches_initial
> first checks that the initial insts match covariantly,
> by calling pred_inst_argmodes_match_initial
> and then (this is the point I didn't notice originally)
> it also calls pred_inst_argmodes_matches, which checks that
> they also match contravariantly.  By checking that they
> match in both directions, it is enforcing "invariant" subtyping --
> in other words, no subtyping at all (the subtype information in the two
> insts must match exactly).
> 
> This is safe, but overly conservative.
> 
> David, was this deliberate?  What's the rationale for doing the covariant
> inst_matches_initial check in pred_inst_argmodes_match_initial?

The calls to inst_matches_initial are deliberate, although the fact that
this makes mode checking overly conservative is not.  The reason the
calls to inst_matches_initial are there is because inst_matches_initial
computes the substitution required for any inst parameters that occur in
the argument inst, and there may be inst parameters in the insts of the
higher-order argument modes.

To fix this, it would be necessary to factor out the code to compute the
inst parameter substitution from the rest of inst_matches_initial.  I
will do this some time, but I'm busy working on HAL stuff at the moment.


David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 9159
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------