[m-dev.] Ye Olde Subtyping Proposal

[David Overton]

On Tue, Nov 12, 2002 at 09:21:41AM +1100, Ralph Becket wrote:
> Fergus Henderson, Tuesday, 12 November 2002:
> > On 11-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > 
> > Perhaps it should be a different type class, though -- `castable(T)'
> > rather than `constructible(T)'.  (In Haskell, the castable(T) class
> > is called "Dynamic".)
> 
> castable/1 is the better name.
> 
> > > Here is an example that illustrates another problem:
> > > 
> > > 	:- pred q(T, T, T).
> > > 	:- mode q(in, in, out) is semidet.
> > > 
> > > 	q(X, Y, Z) :-
> > > 		test_some_condition(X),		% semidet
> > > 		Z = Y.
> > > 
> > > The problem here is that the pred declaration says the parameters all
> > > have the same type, but does it imply they have the same subtype?
> > 
> > I don't know what "the parameters all have the same subtype" would mean.
> > Do you mean "there exists a subtype S such that the parameters all have
> > the same subtype"?  If so, this is trivially true -- just take S = T.
> > Do you mean "for all subtypes S, the parameters all have that subtype"?
> > If so, the answer is no.
> > 
> > But the property we are looking for is not that "for all subtypes S,
> > the parameters all have that subtype".
> > 
> > Rather, the property that we are looking for is that *if* the inputs
> > have a particular subtype, then the output will have that subtype too.
> > This property *does* hold.
> 
> Say we have types t3 < t2 < t1 (where t1 goes in the relation doesn't
> matter) with X:t1, Y:t3, Z:t2, then it seems to me that the type
> signature for q/3 would make a call q(X, Y, Z) appear valid (since there
> is a most general type for all three arguments), but the mode signature
> would make it appear invalid (since we're not really using the type
> system to implement subtyping.)
> 
> Put another way, say I have t2 < t1 (t1 not a subtype) with X:t2, Y:t2,
> Z:t2, then is it the case that q(X, Y, Z) is well moded?  It seems not,
> since the `out' mode of Z only allows us to conclude that it has type
> t1, not t2.

Yes, that is all correct.  If you want a more precise mode you would
need to explicitly add polymorphism to the mode declaration.


David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 9159
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------