[m-dev.] Ye Olde Subtyping Proposal

[Mark Brown]

On 12-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 12-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > On 12-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > > On 11-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > > > 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.
> > 
> > Those results apply to _unconstrained_ polymorphism.  Here is another
> > example:
> > 
> > 	:- typeclass foo(T) where [ func foo = T ].
> > 
> > 	:- type bar ---> a ; b.
> > 	:- instance foo(bar) where [ (foo = a) ].
> > 
> > 	:- pred p(T, T) <= foo(T).
> > 	:- mode p(in, out) is det.
> > 
> > 	p(X, foo(X)).

That should of course be:

	p(_, foo).

> > 
> > In this case the implicit polymorphic mode would be wrong.
> 
> Yes.  So we shouldn't add implicit polymorphic modes in cases like this.
> The idea is to only add implicit polymorphic modes for unconstrained
> polymorphism.

Ah, I see.  In the proposal you allowed for

| the propagation of subtype
| information only for polymorphic type variables which are not
| constrained to be a subclass of `constructable'

and since the type variable T is not constrained by `constructable' I thought
it would be a candidate for the implicit polymorphic mode.  In other words
I read "only for" as "for and only for" -- that's what the proposal seemed
to be saying.

>As I wrote in Feb 2000 [1]:
> 
>  | in general it's not 
>  | safe to do that kind of automatic propagation for polymorphic types 
>  | which are type class constrained. So explicit polymorphic modes 
>  | declarations would still be necessary for those cases of predicates 
>  | which take type class constrained polymorphic types and which are 
>  | also polymorphically moded. 

So the typeclass `constructable' is not really special at all -- any other
typeclass would do just as well.  In particular, the constraint on
univ_to_type doesn't have to be the same as the constraint on construct.

> 
> Note that although adding an implicit polymorphic mode is unsafe
> in that case, it *would* be safe if the type class foo(T) was declared
> as e.g.  `:- typeclass foo(T) where [ func foo(T) = int ].'.
> In general, it would be possible to examine the structure of the type class
> and determine from that whether it is safe to add implicit polymorphic
> modes, but I think that would be getting too clever; it's better to have
> a simple rule that makes it easy for programmers to determine whether
> a procedure is polymorphically moded, without requiring them to look at
> the type class declaration(s) for any associated type class constraints.

Agreed.  Perhaps we could allow "promise_free" declarations, the meaning of
which be that the free theorem for each method is valid?  A promise like
this may have a number of effects:

	1)  Any instance of the typeclass must be promised free.

	2)  Any superclass of the typeclass must be promised free.

	3)  Implicit modes can be added for types which are constrained
	    by the typeclass.

	4)  etc.

Cheers,
Mark.

> [1] http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-developers/mercury-developers.0002/0103.html
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------