[m-dev.] Ye Olde Subtyping Proposal

Mark Brown dougl at cs.mu.OZ.AU
Tue Nov 12 19:59:16 AEDT 2002

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

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


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

More information about the developers mailing list