[m-dev.] Ye Olde Subtyping Proposal

[Mark Brown]

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.

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