[m-dev.] Ye Olde Subtyping Proposal

[Ralph Becket]

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.

> > The reason we wanted inference of the polymorphic modes was (IIRC)
> > that predicates and functions in the standard library are mostly
> > polymorphically moded, but generally aren't written that way and
> > hence won't work with subtypes without the inference.  Therefore,
> > anyone using subtypes would not be able to use the standard library
> > as easily as they would like.

Let's just get the job done.  We should have started on it as soon
as David's polymorphic mode change was accepted.  For users' own
libraries, it shouldn't be an issue since they've been using thier
own libraries without subtyping up till now anyway.

> > With that in mind, here is my variant
> > of the proposal:
> > 
> > 	1) implement all of the previous proposal except for the
> > 	   inference of polymorphic modes, and
> > 
> > 	2) manually change all of the library preds/funcs to be
> > 	   polymorphically moded, except where the change would be
> > 	   unsafe.
> 
> (2) has been proposed before, but has not been applied because it
> significantly slows down compilation of programs that use the library :-(
> 
> Of course making them all implicitly polymorphically moded
> would have the same problem.

Ah.  How significant is `significantly'?

Is this slow-down a necessary cost or just an artifact of our current
inference algorithm?

> > Part 1) above is common to both proposals, and since we already have
> > in-principle agreement with the idea I'm going to go ahead and start
> > working on that part.
> 
> Great!  Despite the current efficiency problem with (2), I think it is
> nevertheless still worth going ahead with (1).

Agreed.

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