[m-dev.] Ye Olde Subtyping Proposal

[Fergus Henderson]

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

The main reasons that the library uses "ground" are
	(1) historical
and	(2) speed of compilation.

There are also a few procedures such as io__read and univ_to_type
for which a polymorphic mode is not appropriate.

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

Placing a typeclass constraint on univ_to_type is exactly the right solution.
It's not a kludge at all, IMHO.

Perhaps it should be a different type class, though -- `castable(T)'
rather than `constructible(T)'.  (In Haskell, the castable(T) class
is called "Dynamic".)

> Furthermore, I don't know whether there are any other predicates that may
> need the constraint as well.

There are a few.  The problematic cases are all implemented using the C
interface.

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

The proof is along the same lines as the proof of "free theorems"
in functional programming [1].
See below for a very brief sketch.

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

I don't know what "the parameters all have the same subtype" would mean.
Do you mean "there exists a subtype S such that the parameters all have
the same subtype"?  If so, this is trivially true -- just take S = T.
Do you mean "for all subtypes S, the parameters all have that subtype"?
If so, the answer is no.

But the property we are looking for is not that "for all subtypes S,
the parameters all have that subtype".

Rather, the property that we are looking for is that *if* the inputs
have a particular subtype, then the output will have that subtype too.
This property *does* hold.

<proof sketch>
The reason for this is that since the output is an unconstrained
polymorphically typed variable, the only type-correct way to construct
values of this type is by unifying them with some value of the input
type.  The type checker's proof of type correctness remains valid if
you substitute a subtype for the type.  This can be verified by
examining each of the typing rules and verifying that they hold for
subtypes too.
</proof sketch>

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

I don't know what you mean here.  Could you elaborate?

> The reason we wanted inference of the polymorphic modes was (IIRC)

What do you mean by "inference of polymorphic modes"?
Are you referring to this part of the proposal:

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

?
If so, using the phrase "inference of polymorphic modes" to describe
that might be confusing.  I think it would be better to call it
"implicit polymorphic modes".  This is just a kind of syntactic sugar
for polymorphic modes, not inference of polymorphic modes.

"inference of polymorphic modes" would refer to the mode checker's
ability to infer polymorphic modes in the absence of any mode
declaration at all.

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

It's not just procedures in the standard library -- this also applies
to all existing polymorphically typed Mercury code.  In the compiler it
applies to the libs__tree, libs__graph_color, and libs__atsort modules,
and lots more (see the output of "grep T *.int").

However, the problem is worst for the standard library since users
can't easily modify the standard library, whereas they can modify
their own code.

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

(2) has been proposed before, but has not been applied because it
significantly slows down compilation of programs that use the library :-(

Of course making them all implicitly polymorphically moded
would have the same problem.

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

Great!  Despite the current efficiency problem with (2), I think it is
nevertheless still worth going ahead with (1).


References
----------
[1] P. Wadler, "Theorems for free!," in Fourth International
Conference on Functional Programming and Computer Architecture, London,
MacQueen, ed., Addison Wesley, 1989.
http://citeseer.nj.nec.com/wadler89theorems.html   

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