[m-dev.] subtypes discussion

[Mark Brown]

On 23-Dec-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 23-Dec-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > 4) Subtypes: subsumption vs specialization
> > ------------------------------------------
> > 
> > One reason our proposed design may seem counterintuitive is that our subtypes
> > do not support subsumption.  That is, we don't support the notion that if S
> > is a subtype of T, then values of type S can be safely used wherever values
> > of type T are expected.  This may be counterintuitive
> 
> Yes, IMHO it is counterintuitive.
> 
> I would much prefer to go with a design that does support subsumption.

I don't understand why it is important that this feature supports
subsumption.

I'm trying to characterize the use of subtypes as a form of specialization.
This certainly seems a reasonable way to describe the motivating example --
the two functions operate on a restricted set of inputs (restricted from the
full set of values for the type, that is), and the predicate takes as an
argument something that is specialized in this way.  I can't see how
specialization and subsumption can be compatible: you simply wouldn't
expect to be able to use a specialized version of an object where a
non-specialized version was expected.  Obviously you wouldn't be able to
pass fruit_problem as a higher-order value to somewhere expecting a
function defined on all fruit.

> 
> > In our example, the use of subtypes (with or without subtype declarations)
> > can be thought of as a form of specialization rather than subsumption.
> 
> The motivating example that you posted was good as an example supporting
> the introduction of subtypes, but as far as I can see it didn't illustrate
> any benefit from the covariant approach that you are proposing (or if it did,
> I missed it; maybe you need to spell it out for me ;-).

Okay.  Consider the argument of fruit_problem.  We intend the mode of
that argument to be 'in(disliked_fruit)', but we want to just write 'in'
(or, in fact, to use the default mode).  So we want the propagation of
subtype disliked_fruit into mode 'in' to convert the initial inst from
ground to disliked_fruit, and we want it to convert the final inst also
from ground to disliked_fruit.  That is, we want the initial inst and the
final inst to both become smaller -- we want them to vary in the same
direction.

If the subtype order is contravariant, then propagating a subtype into a
mode can never make the initial inst smaller, and there would be no way of
going from ground to disliked_fruit.

Therefore, for our motivating example, the covariant approach can help
and a contravariant approach cannot.

The best way I can think of to understand why the subtype partial order is
covariant is to follow David Overton's advice and consider the propagation
as a glb or lub operation.  A covariant order will result from using the
glb for both the initial and final insts.  A contravariant order will result
from using lub for the initial inst and glb for the final inst.  We want
to work with "type-like" subtypes, so we want propagation to affect the
initial and final insts in an identical way (otherwise the results wouldn't
generally be type-like).  That means using glb for both, with the result
that the order is covariant.

In order to support subsumption, the rule for propagation I suppose would be
to use the lub for the initial inst and the glb for the final inst.  With
this rule, our example would generate the mode

	:- mode fruit_problem(ground >> disliked_fruit) = string is det.

Since the function is det, we must define a non-failing clause for
fruit_problem(orange).  The final inst means that this clause cannot succeed,
so if we don't want to loop we have to throw an exception.  We are therefore
back where we started; the subtype declarations do not achieve what they are
designed to in this case.

Cheers,
Mark.

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