[m-dev.] Ye Olde Subtyping Proposal

[Fergus Henderson]

On 18-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> 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.

Agreed.  This was the intent in the original proposal.

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

I agree that abstract subtypes would be useful, but supporting them would
mean that the proposal was no longer just syntactic sugar, but instead added
a major new feature.  This would require substantial changes to mode analysis
to implement.  I'm not opposed to doing that in the long term, but in the
short term I think it would be better to support subtypes without abstract
subtypes.

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

IMHO the answer should be yes.

The subtyping in the mode system has always been structural subtyping
rather than by-name subtyping.  This is necessary because often terms
are constructed just by unifications in the body of a clause, which
do not give any name to the inst of the term that they create.

IMHO structural subtyping is the right kind of subtyping to use in this
context.  Subtypes just represent subsets and set inclusion is sufficient
to ensure safe usage.  (It's different than the use of structure subtyping
as the *only* typing mechanism; here we are building our structure subtypes
on top of by-name types, rather than making all types be sub-types of a
universal term type.  This essentially eliminates the dangers of problems
arising from unintended structural equivalence due to the use of equivalent
representations for conceptually different entities.)

For abstract subtypes, on the other hand, obviously structural subtyping
can't be used.  So in that case, it would be OK to use by-name subtyping
(that is, define the subtype relation only in terms of the declared subtypes).
By-name subtyping would be a conservative approximation to (or abstraction
of) structural subtyping.

Although using structural subtyping for concrete subtypes and by-name
subtyping for abstract subtypes could be considered inconsistent, it
has the following important advantages:

	- the treatement of subtyping for concrete subtypes is consistent
	  with the treatment of subtyping for terms whose subtype is not
	  explicitly named, e.g. those constructed in clause bodies

	- it is more expressive, in the sense that it allows programs which
	  by-name subtyping would not (and these programs are safe in the
	  sense that they do not lead to any violations of type or mode
	  correctness and that they are not likely to be buggy)

	- it will be much easier to implement structural subtyping.
	  This is because structural subtyping is just syntactic sugar on
	  top of the existing mode system, whereas by-naming subtyping
	  would require significant changes to mode analysis (which is
	  already the most complicated part of the Mercury front-end).

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