[m-dev.] Ye Olde Subtyping Proposal

[Fergus Henderson]

On 18-Nov-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Fergus Henderson, Monday, 18 November 2002:
> > Actually subtypes would need to get checked in the mode checker, not the
> > type checker, because you need to know the direction of data-flow in
> > order to check subtypes.
> 
> We have a number of places that need tweaking to make this change, but
> putting in a subtyping relation that is checked by the type checker
> shouldn't be too hard, surely?

Should the following example be legal?

	:- type fruit ---> apple ; orange.
	:- subtype citrus < fruit ---> orange.

	:- mode m == ...

	:- pred p(fruit::m).
	:- external(p/1).

	:- pred q(citrus::m).
	q(X) :- p(X).

My opinion is that it should be legal if m == out, but not if m == in.
Next consider a similar example, but using mode inference rather than
declared modes.  If the type checker has to do mode inference in order
to determine type-correctness, then we have a problem...

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