[m-dev.] Ye Olde Subtyping Proposal

[Mark Brown]

On 18-Nov-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> I'm really starting to like this idea.  For instance, we could then
> write
> 
> :- type list(T) ---> [] ; [T | list(T)].
> 
> :- type non_empty_list(T) < list(T) ---> [T | list(T)].
> 
> without mucking around with hairy modes.
> 
> It occurs to me that the RHS of the subtype declaration should admit the
> following:
> 
> 	If a type t has constructor f(T1, ..., Tn) then a subtype s < t may
> 	have a constructor f(S1, .., Sn) such that for i in [1, n] Si =< Ti
> 	where Si =< Ti <=> (Si = Ti ; Si < Ti).
> 
> That is, we should not insist that Si = Ti.

Absolutely.  Here is another couple of examples which I think would be
allowed:

	:- subtype odd(T) < list(T) ---> [T | even(T)].
	:- subtype even(T) < list(T) ---> [] ; [T | odd(T)].

> I can't offhand think of any reason why this would go wrong (it isn't
> clear to me whether the existing proposal actually allows this or not -
> can anyone clarify one way or the other?)

The way I read the existing proposal, it does allow for this.

One thing to be careful of is that the relation "is a subtype of" may wind
up being recursively defined, so if that happens we have to make sure that
it is well defined.

Another problem is that we have to consider how the definition of the
subtype relation will work with the module system.  Although abstract
insts may not be useful, abstract subtypes would be, so we need to be able
to check that a subtype declaration is valid even though it may refer to
other subtypes for which we don't have the full implementation.

Consider the following:

	:- subtype zzz(T) < list(T) ---> [T | zzz(T)].

Is zzz(T) a subtype of odd(T)?  Is it a subtype of even(T)?

If we take the view that A is a subtype of B iff A specifies a set of
values that is a subset of the values specified by B, then the answer
to both questions is yes because the set of values specified by zzz(T)
is empty.  Likewise, odd(T) is a subtype of non_empty_list(T), since its
only constructor [|]/2 is also a constructor of non_empty_list(T), and
for the arguments we have that T is a subtype of T and even(T) is a
subtype of list(T).

Since these conclusions can only be drawn with reference to the
subtype implementation, the above definition of the subtype relation
won't work nicely with the module system.  With that in mind, here's
how I think the subtype relation should be defined.

\begin{defn}

The subtype relation, which we will write as <, is defined as the smallest
reflexive and transitive relation for which the following conditions hold:

        a)  Let \sigma and \tau be substitutions such that for any
        variable V,

                V \sigma  <  V \tau.

        If there is a declaration

                :- subtype S < T ---> ...

        then

                S \sigma  <  T \tau

        is true.

        b)  Let \sigma and \tau be substitutions such that for any
        variable V,

                V \sigma  <  V \tau.

        If S is any type or subtype then

                S \sigma  <  S \tau

        is true.

\end{defn}

Examples:

	non_empty_list(T) < list(T)
	odd(int) < list(int)
	list(odd(even(T))) < list(list(list(T)))

The following, however, is not true:

	odd(T) < non_empty_list(T).

If a subtype declaration tried to use odd(T) in an argument position
where the supertype had non_empty_list(T), this would therefore be an
error.  On the other hand, if the definition of odd/1 had been

	:- subtype odd(T) < non_empty_list(T) ---> [T | even(T)].

then it would be true that

	odd(T) < non_empty_list(T).

Cheers,
Mark.

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