[m-dev.] subtypes discussion

[Mark Brown]

On 23-Dec-2002, Fergus Henderson <fjh 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:
> > > 5) Subtypes vs subsets
> > > ----------------------
> > > 
> > > For first order types, the subtype partial order corresponds to the subset
> > > relation on values of the given types, as expected.  For higher-order types,
> > > however, it is not obvious to me how to interpret a given subtype as a
> > > subset.
> 
> As I said in my previous mail, different subtypes of a higher-order type
> correspond to the same set of values (but different sets of representations).
> What I forgot to add is that as a result, the subset relation holds in
> both directions.  That is, the set of values described by a higher-order subtype
> is always a subset of the set of values described by any other higher-order
> subtype of the same higher-order base type.  (It is not a "proper subset".
> But it is a subset.)
> 
> Furthermore, the subset relation also holds (although only in one
> direction) if you talk about sets of representations.  That is, the set
> of representations described by a higher-order subtype is always a subset
> of the set of representations described by its base type.
> 
> My view is that:
> 
> 	- it should be possible to interpret types either declaratively,
> 	  as sets of values, or operationally, or as sets of representations;
> 
> 	- it should be possible to interpret subtypes either declaratively,
> 	  as subsets of values, or operationally, or as subsets of
> 	  representations;
> 
> 	- for the operational viewpoint, we should have subsumption;
> 	  that is, if S is a subtype of T, it should be possible to safely
> 	  use any representation in S whenever representations in T
> 	  could be used
> 
> 	- for the declarative viewpoint, we should have a weaker
> 	  guarantee: subsumption subject to mode- and determinism-correctness.
> 	  That is, if S is a subtype of T, it should be type-correct to
> 	  use any value in S whenever values in T could be used,
> 	  and furthermore this is also safe provided that the code
> 	  remains mode- and determinism-correct.

By the definition of our subtype order, if S is a subtype of T then S and T
must have the same base type.  As pointed out in your your first paragraph,
the values in S are a subset of the values in T if they have the same base
type, so it must be type-correct to use any value in S whenever a value in T
could be used.  Thus the approach that I am advocating supports the
declarative viewpoint.

As we've already established, though, this operational viewpoint is not
supported.

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