[m-dev.] Ye Olde Subtyping Proposal

[Ralph Becket]

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.

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

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