[m-dev.] subtypes discussion

[Mark Brown]

On 24-Dec-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 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.

No.  From what you say below, I can see that there is a real difference
in our intuitions -- see my comments below.  The terminology has probably
been concealing exactly what that difference is, though.

...

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

Yes, this terminology is being stretched a bit, as usual.  It is really some
arguments to some functor, in this case the initial insts of a pred or
func inst constructor, that are covariant with respect to an ordering; the
ordering itself is not what is covariant.  The ordering in question is
the partial order determined by the rules for propagation.

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

I am indeed conflating the rules for propagation and the rules for subtyping.
This is deliberate, because doing otherwise is what I find counterintuitive.
Earlier I gave the rules for how to derive a partial order from the rules for
propagation, and I said that "This shows how I derived the subtype partial
order."  It appears that this sums up the part of my intuition that conflicts
with yours.

On the other hand, you are conflating the rules for subtyping and the rules
for matching.  That is, your intuition is that the subtype partial order
and the matches partial order should be the same.

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

Right; I didn't think so.  I just didn't realise that you were happy for
the subtype partial order and the propagation partial order to be different.

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

Yes, I am arguing to make that legal, because fyy can be thought of as a
specialisation of fbb.  I am aware that fyy does not subsume fbb, but
that doesn't bother me because my intuitive view of the subtype relation
is as specialisation, not subsumption.

So I don't just view the propagation as specialisation, I view the whole
subtyping system as specialisation.

I think the subtypes of fbb (with the default func inst) should include
at least the following:

	func(bool) = bool
	func(bool) = y
	func(bool) = n			% n is analogous to y
	func(y) = bool
	func(y) = y
	func(y) = n
	func(n) = bool
	func(n) = y
	func(n) = n

But if you disallow fyy, it seems to me you would have to disallow all but
the first three of these.  So, what subtypes of fbb (with the default func
inst) do you think should be 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))'.

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

Well, the default mode for g is

	:- mode g(in(func(in) = out is det)) = out is det.

so the mode after propagation should be equivalent to

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

but I think that is what you mean.

In other words, the initial inst of the argument of g before propagation is

	func(ground >> ground) = (free >> ground) is det

and after propagation is

	func(bound(y) >> bound(y)) = (free >> bound(y)) is det.

This does indeed satisfy the declarative interpretation of your above
paragraph: the subset of _values_ represented by the latter inst is the
intersection of the subsets of values represented by the former inst and
the subtype.  This is true since all of these subsets are equal for higher
order types.

My view, however, is that if you can declare g to have the type given above,
then you should be able to achieve the same effect by declaring

	:- func g(fyy) = int.

and declaring fyy -- legally -- in the way that you did above.  In either
case g could be viewed as taking an argument that is specialised with
respect to its base type, and in either case the desired declarative
interpretation would be satisfied.

> 
> So, does that clear up our differences?

It certainly clarifies precisely what our differences are, which is a
large part of resolving them.

At this stage of the discussion, there seem to be three partial orders
of interest: the "matches" partial order (from David Overton's thesis
draft), the "propagation" partial order (determined from the rules for
propagation), and the "subtype" partial order (which reflects the rules
we impose on subtype declarations).  There is no disagreement on either
the matches partial order, which supports subsumption, or the propagation
partial order, which supports specialization.  There are two views on the
subtype partial order:

	1) it should be the same as the matches partial order, or

	2) it should be the same as the propagation partial order.

In either of these views, the declarative interpretation of subtypes as
subsets of values is consistent.

I'm still of the view that option 2 is the right design, and I'll try to
come up with some more motivating examples to support it.  Maybe, though,
the problem is that I just haven't seen enough motivating examples to
support option 1 (hint hint ;-)).

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