[m-dev.] Ye Olde Subtyping Proposal
Fergus Henderson
fjh at cs.mu.OZ.AU
Tue Nov 12 21:24:36 AEDT 2002
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
--------------------------------------------------------------------------
More information about the developers
mailing list