[m-dev.] Ye Olde Subtyping Proposal

[Mark Brown]

Hi,

I'd like to once again bring up the subject of the subtyping proposal.
As I have mentioned before, I think this feature is sorely missed in
the language.  However, since the last time it was discussed I've had
some time to think about it more, and unfortunately I think I now see
some problems in the proposal as it stands at the moment.

I also have a variant of the proposal that avoids the problem, but I'll
describe the problem first.

The full proposal can be found at:
http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-developers/mercury-developers.0002/0093.html

On 09-Feb-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> Drawbacks:
> 	
> 	One problem with this proposal as it stands is that using the
> 	mode system for subtypes doesn't work well with polymorphic
> 	predicates or containers.
> 
> 	We could fix these problems by adding support for polymorphic
> 	modes, with the inst variables required to name ground insts.
> 	This restriction would make polymorphic modes relatively easy
> 	to implement.

We have this now, so that problem is fixed ...

>	For polymorphically typed predicates, we could
> 	propagate type information into the modes so that all polymorphically
> 	typed predicates also become polymorphically moded.

I've had a growing suspicion for a while that there is something not
quite right about this.  It isn't just the problem with constructable
types, for which a solution has been given, but the fact that I am now
quite unclear as to precisely what "ground" means as an inst.  If the
meaning of it is so clear, why does the compiler find it useful to infer
a polymorphic mode instead?  If the polymorphic mode is so useful for,
say, append/3, why does the library even use "ground" at all?

> 	For example, for `set__singleton_set(set(T)::out, T::in)',
> 	if at a particular call the 2nd argument has inst `bound(foo)',
> 	then on exit the first argument would have inst `set(bound(foo))'
> 	where `set(I)' is a (compiler-generated) polymorphic inst
> 	whose shape reflects the definition of the `set(T)' type.
> 
> 	That is unsound in the case of programs that use std_util__construct/3
> 	(e.g. via io__read/3 or term__to_type/2).  However, we could patch
> 	up that hole by adding a typeclass `constructable(T)',
> 	declaring std_util_construct/3 and its callers to take arguments
> 	of that typeclass, and allowing the propagation of subtype
> 	information only for polymorphic type variables which are not
> 	constrained to be a subclass of `constructable'.

That patch is not large enough to cover the hole.  Consider the
following code:

	:- pred p(univ, T, T).
	:- mode p(in, in, out) is det.

	p(U, X, Y) :-
		( univ_to_type(U, T) ->
			Y = T
		;
			Y = X
		).

This would compile fine even without the typeclass constraint, but
inferring a polymorphic mode for it would be unsound, because there
may be a value of type T hidden inside the univ, and univs don't contain
any subtype information.  Maybe a solution to this would be to place the
typeclass constraint on univ_to_type, but this seems a bit kludgy to me.
Furthermore, I don't know whether there are any other predicates that may
need the constraint as well.

I haven't seen any proof that the proposed inference is sound, and I
feel strongly that we should not proceed with this part of the proposal
unless such a proof is seen.

Here is an example that illustrates another problem:

	:- pred q(T, T, T).
	:- mode q(in, in, out) is semidet.

	q(X, Y, Z) :-
		test_some_condition(X),		% semidet
		Z = Y.

The problem here is that the pred declaration says the parameters all
have the same type, but does it imply they have the same subtype?
Well, if the user instead wrote the mode declaration as follows:

	:- mode q(in(I), in(J), out(J)) is semidet.

then there would be no such requirement (none that the compiler would
check, anyway), so the answer to the question must be "no".  The
inferred polymorphic mode for q may therefore not be general enough.
(This isn't as serious a problem as the previous example, but I thought
it worth mentioning still).

The reason we wanted inference of the polymorphic modes was (IIRC)
that predicates and functions in the standard library are mostly
polymorphically moded, but generally aren't written that way and
hence won't work with subtypes without the inference.  Therefore,
anyone using subtypes would not be able to use the standard library
as easily as they would like.  With that in mind, here is my variant
of the proposal:

	1) implement all of the previous proposal except for the
	   inference of polymorphic modes, and

	2) manually change all of the library preds/funcs to be
	   polymorphically moded, except where the change would be
	   unsafe.

With this variant of the proposal, a polymorphic type that is not
polymorphically moded means "types only, no subtypes".

Consider the first example again.  With the variant proposal the mode
of the third parameter to p is forced to be 'out' by the call to
univ_to_type (which wouldn't be polymorphically moded) and the
unification in the 'then' branch.  The inst of the second parameter
could be polymorphic, provided is constrained to be compatible
with 'ground'.

The only drawbacks to this change that I can think of are that the
modifications to the standard library will be rather tedious, and that
our users might find the modifications they will be obliged to do to
their own libraries rather tedious as well (if they want the libraries
to work with subtypes, that is).  But I think this would be a poor reason
not to proceed, particularly since polymorphic modes may in general give
more precise information about the predicates and functions in question,
as the second example shows.

Comments?

Part 1) above is common to both proposals, and since we already have
in-principle agreement with the idea I'm going to go ahead and start
working on that part.

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