[m-dev.] subtypes discussion

[Fergus Henderson]

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.

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