[m-dev.] subtypes discussion

[Mark Brown]

On 28-Dec-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 27-Dec-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > 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.
> 
> This is a good summary of the discussion.
> 
> I still favour position (1), because that's the one which matches my
> mental model of types as sets of values and representations and
> subtypes as subsets of values and representations.

I've tried the design on some more practice examples.  I haven't found
any problems with position (1) other than that which I mentioned
previously:

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

...

> >	:- func g(func(y) = y) = int.

...

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

You can achieve a similar effect legally (with either position) as follows:

	:- type fb(B) == (func(B) = bool).
	:- subtype fy(B) < fb(B) == (func(B) = y).

	:- func g(fy(y)) = int.

or, for that matter:

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

	:- func g(fyy) = int.

Given this, I'm happy to agree to position (1).

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