[m-dev.] Ye Olde Subtyping Proposal

[Fergus Henderson]

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

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.

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