[m-dev.] subtypes discussion

[Fergus Henderson]

On 24-Dec-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> 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.

Well, because the alternative would be counterintuitive!

But our differences here may be a matter of terminology.

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

Fair enough.  No disagreement here.

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

Change the word "object" to "predicate or function" and I'll agree with
that too.

As a consequence, a specialized version of a predicate should in general
not be a subtype of a non-specialized version.

> Obviously you wouldn't be able to
> pass fruit_problem as a higher-order value to somewhere expecting a
> function defined on all fruit.

Agreed.

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

Agreed.

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

You lost me here.

"Propagation should be covariant"? -- that I think I can probably agree with,
although I'm not sure whether the terminology is really appropriate here.

"The subtype order should be covariant"? -- that I am strongly opposed to.

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

You are talking about a covariant approach to propagation.
That I don't have a problem with.  It's the covariant approach
to the subtype ordering that I would have a problem with.

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

Here I think you are incorrectly conflating the rules for propagation with
the rules for subtyping.

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

That is definitely not what I am arguing for.

Consider the following:

	:- type bool ---> yes ; no.
	:- subtype y < bool ---> yes.

	:- type fbb = (func(bool) = bool).
	:- subtype fyy < fbb = (func(y) = y).

IMHO this example should be illegal, since fyy is not a subtype of fbb,
because the subtype ordering is be contravariant.  When you say that
the subtype ordering should be covariant, this implies to me that you
are arguing to make examples like the one above legal.

But for propagation, the inst after propagation should always represent
the intersection of the sets represented by the subtype and the inst before
propagation.  That is, it should always use glb.  This is regardless of
whether the inst is an initial inst or not.

So for example for

	:- func f(y) = y.
	:- mode f(in) = out is det.
	f(yes) = yes.

the mode after propagation should definitely be
`:- mode f(bound(yes) >> bound(yes)) = (free >> bound(yes))'.
Likewise for

	:- func g(func(y) = y) = int.
	g(_) = 42.

the mode after propagation should be

	:- mode g((func(bound(yes)) = bound(yes)) >>
	          (func(bound(yes)) = bound(yes))) = (ground >> ground).

So, does that clear up our differences?

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- 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
--------------------------------------------------------------------------