[m-dev.] Ye Olde Subtyping Proposal

[Fergus Henderson]

On 12-Nov-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> It's not clear to me what would happen in this situation:
> 
> :- type abc       ---> a ; b ; c.
> :- type ab < abc  ---> a ; b.
> :- type really_ab ---> really_ab(ab).
> 
> :- pred p(T::in, T::out) is det.
> 
> p(X, Y) :- X = Y.

That is a very good question.

According to the semantics in my original post, this is equivalent to
the following program:

	:- type abc       ---> a ; b ; c.
	:- type ab == abc.
	:- inst ab == bound(a ; b).
	:- type really_ab ---> really_ab(ab).

	:- pred p(T::in, T::out) is det.

	p(X, Y) :- X = Y.

The inst `ab' is not used at all, so we can eliminate it.
We can also eliminate the equivalence type `ab' by substituting it away:

	:- type abc       ---> a ; b ; c.
	:- type really_ab ---> really_ab(abc).

	:- pred p(T::in, T::out) is det.

	p(X, Y) :- X = Y.

> Now, is the following goal legal or not:
> 
> 	p(X `with_type` really_ab, Y `with_type` really_ab)

Yes, provided it occurs in a context where X is ground, this is legal.

But as you can see, the subtypes have been entirely ignored.

I guess this is a serious shortcoming in the original proposal.
So we need to come up with a new semantics.
The semantics needs to address the cases when a subtype occurs
(a) in a data structure
(b) in an argument type, but not at the top level.
(c) in a `with_type` qualification

My new proposal is that for (a) and (b), we propagate the subtypes in these
cases into the modes in the "obvious" way [1].
For (c), I propose that we make it an error to use subtypes in `with_type`
qualifications.  The rationale for this is that just using the type
rather than the subtype would make this construct misleading;
and there's no obvious way to make use of the inst in this context.

So with this new proposal, your example goal is illegal since it uses
`with_type` with a subtype.  However, consider a slight variation:

	:- pred q(really_ab::in, really_ab::out).
	q(X, Y) :- p(X, Y).

	... rest of the example as above ...

In this case, the example would be legal iff we support implicit
polymorphic modes for p/2.  Also, if we changed p/2 so that it is declared
with explicit polymorphic modes, then this example would be legal.

Footnotes
[1] Well, obvious to me anyway ;-)
    Basically what I have in mind is a fairly straight-forward extension
    of the propagation already done when we propagate types into the modes.
    But for a proper specification we'd need to make this more precise.
    [Right now, for me getting the release out is a higher priority.
    So if anyone else wants to have a go at wording this precisely,
    feel free to go ahead.
    Otherwise I will have a go at this some time after the release is out.]

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