[mercury-users] Typeclass problem (bug, misunderstanding, oth er?)

[Fergus Henderson]

On 09-Aug-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> Sorry to keep harping on about this one, but I am
> just totally bemused.  Can you go through the type
> inference on this one line by line and point out
> where the error is?

Actually the Mercury compiler's `--debug-types' option does exactly that.
So you might find that useful.  (Beware, though, that in the current
implementation it does not distinguish between different occurrences
of type variables that have the same name but have been renamed apart.)

On 09-Aug-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> > From: Fergus Henderson [mailto:fjh at cs.mu.OZ.AU]
> > 
> > In order to typecheck a procedure call, one must rename apart the
> > type variables in the called procedure's type declaration before
> > unifying them with the calling procedure's type variables.
> > I think that in making that deduction, you omitted the renaming
> > apart step.
> 
> That's a good point.  But I'm not sure it explains the following:
> 
> :- typeclass tc(T1, T2) where [
> 	func e(T1) = T1,
> 	func f(T1) = T2,
> 	func g(T1, T2) = T2
> ].

The `e' method here is already problematic.  The compiler really ought
to issue an error or at least a warning at this point, since there is
no way that e/1 can be called without an ambiguous type error.
(Thank you for continuing to harp on this point, since by doing so you
have identified an area in which we can easily improve the compiler's
diagnostics.)

The type for `e' is

	:- func e(T1) = T1 <= tc(T1, T2).

The problem is that none of the arguments to or result of this
function contain the type `T2', so there is no way that the `T2'
type parameter can ever be constrained.

The solution is to make that function a member of a different
single-parameter type class, and have the multi-paramater type
class inherit from the single parameter type class:

	:- typeclass base(T1) where [
		func e(T1) = T1
	].
	:- typeclass tc(T1, T2) <= base(T1) where [
		func f(T1) = T2,
		func g(T1, T2) = T2
	].

> :- func foo(T1) = T2 <= tc(T1, T2).
> 
> foo(A) = g(A, f(A)).
> 
> This will work fine.
...
> However,
> 
> :- func bar(T1) = T2 <= tc(T1, T2).
> 
> bar(A) = g(e(A), f(A)).
>
> causes an unsatisfied typeclass constraint error.

The compiler is right to reject this.
Consider the following similar function:

	:- func bar2(X1) = pair(X2,X3) <= (tc(X1, X2), tc(X1, X3)).

	bar2(A) = g(E, f(A)) - g(E, f(A)) :-
		E = e(A).

Here it is not clear whether the type T2 in the type class constraint
for e/1 should be bound to X2 or to X3.

The compiler can't infer that T2 should be bound to X2 simply
because (X1, X2) is known to be an instance of the class tc/2,
since there may be other instances (e.g. (X1, X3)) that also match but
which have different semantics.

Likewise in your example with bar/1, the compiler can't infer
that T2 in the type class constraint for e/1 should be bound
to the T2 from the type declaration for bar/1, since there may
be other instances that also match but which have different
semantics.

Anyway as I said the solution is to split such functions off into a
separate base class.

Cheers,
	Fergus.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------