[m-dev.] subtypes discussion

[Fergus Henderson]

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.

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

> 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.
> 
> Consider the following type and inst (which is a subtype, although it isn't
> "type-like" so we couldn't define it with our subtype declarations):
> 
> 	pred(fruit :: ground >> disliked_fruit) is semidet.
> 
> Possibly we can think of this as a subset of the values described by inst
> 'pred(fruit::in) is semidet', where P is in the subset iff P(orange) cannot
> succeed.

"cannot succeed" is an operational property, not a declarative property.
The almost-but-not-exactly corresponding declarative property is
"has no solution".

Consider the following example:

	:- pred p(fruit::ground >> disliked_fruit) is semidet.
	p(orange) :- (loop ; not loop).

	:- pred loop is erroneous.
	loop :- loop.

For this example the property "p(orange) cannot succeed" is true
in the "strict sequential" operational semantics,
but the property "p(orange) has no solution" is false.

Determinism analysis only checks the operational property "cannot succeed",
not the declarative property "has no solution".

Thus the set of values described by inst
`pred(fruit :: ground >> disliked_fruit) is semidet'
is the same as the set of values described by `pred(fruit::in) is semidet'.
What is different is the set of *representations* of those values:
the former inst describes a subset of the representations described
by the latter inst.  In other words, declaratively they are the same,
but operationally there is a subset relation.

> On the other hand, consider the case where the initial inst is modified:
> 
> 	pred(fruit :: disliked_fruit >> ground) is semidet.
> 
> Values described by this inst are unary relations on the set {apple, lemon},
> and none of these values are in the set of values described by
> 'pred(fruit::in) is semidet', since the latter are all defined on oranges.

Here too I think your analysis is not correct.  Values described by this
inst are unary relations on the set {apple,lemon,orange}.  The mode
and determinism of the higher-order term only constrain the representation,
not the set of values.

In particular the following examples are legal,

	:- pred p2(fruit::disliked_fruit >> ground) is semidet.
	p2(orange).

	:- pred p3(fruit::disliked_fruit >> ground) is semidet.
	p3(orange) :- fail.

and the values `p2' and `p3' are both members of the set of values described
by the inst `pred(fruit :: disliked_fruit >> ground) is semidet'.

> Therefore the subtype order does not in general correspond to the subset
> order.  Note that even if the subtype order was contravariant instead of
> covariant, it would still not correspond to the subset order.  It appears
> to me that the subtype order must be invariant if it is to directly
> correspond to the subset order.

I disagree with these conclusions.  IMHO the analysis by which you
derived them was flawed, as explained above.

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