[m-rev.] for discussion: subtypes documentation

[Mark Brown]

On 25-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 24-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > + at node Higher-order subtypes
> > + at section Higher-order subtypes
> > +
> > +As stated earlier, the subtype relation on first-order types
> > +is the same as the subset relation.
> > +For higher-order types, the subtype relation is slightly more complex.
> > +We extend the relation to higher-order types with the following two cases.
> > +
> > + at itemize @bullet
> > + at item
> > +A type @code{func(@var{S1}, @dots{}, @var{SN}) = @var{S}}
> > +is a subtype of @code{func(@var{T1}, @dots{}, @var{TN}) = @var{T}}
> > +iff @var{S} is a subtype of @var{T},
> > +and for each argument @var{i}, @var{Si} is a subtype of @var{Ti}.
> > +
> > + at item
> > +A type @code{pred(@var{S1}, @dots{}, @var{SN})}
> > +is a subtype of @code{pred(@var{T1}, @dots{}, @var{TN})}
> > +iff for each argument @var{i}, @var{Si} is a subtype of @var{Ti}.
> > +
> > + at end itemize
> > +
> > + at noindent
> > +In other words the subtype relation on predicate and function types
> > +is @emph{covariant} in the argument values
> > +and (for function types) the return values.
> > + at c This is in contrast to the usual object-oriented view of subtypes,
> > + at c where inputs are contravariant and outputs are covariant.  We use
> > + at c covariant subtypes because they work much better with parametric
> > + at c polymorphism.
> > +Mercury's mode system provides enough information for the compiler
> > +to statically check that the use of covariant subtypes is safe.
> 
> I think this is wrong.
>
> The mode system uses covariant subtyping for the
> final insts and contravariant subtyping for the initial insts.

The "subtype" partial order which I describe and the "matches" partial
order from David's thesis draft are not the same.  Whether the fact that
they differ is wrong or not is the question -- I can't see any reason
that the subtype partial order and the matches partial order must be the
same.  Note that the only purpose of the subtype partial order is to ensure
that subtype declarations are "sensible".  It isn't used to check that
programs are mode correct.

Here's a definition of the subtype partial order in terms of the
propagation of one base inst into another.  This shows how I derived
the subtype partial order.

	Let A' and B' be the base insts of two subtypes A and B.  A and B
	must have the same base type.  If it is not legal to propagate A'
	into B', then A and B are incomparable.  Otherwise, let C' be the
	inst that results from propagating A' into B'.

	1) If C' = A', then A is a subtype of B.

	2) If C' = B', then B is a subtype of A.

	3) Otherwise, A and B are incomparable.

Maybe there is some other way of doing the propagation which generates a
"better" subtype partial order; I'll have to look into it further to
know one way or the other.

> Using covariant subtyping for the initial insts would be unsafe.

We don't have to worry about safety, because the transformed program
(i.e., the program that results from processing all the subtypes) will
still be mode analysed in the usual way.  All we have to worry about is
that any error messages generated for the transformed program are
translated back so that they make sense for the original program.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------