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

[Fergus Henderson]

On 06-Aug-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> > From: Fergus Henderson [mailto:fjh at cs.mu.OZ.AU]
> > 
> > > Ahh.  This looks like a hole in type inference to me, now.
> > > From the typeclass definition and the typeclass constraint
> > > on solve/5 it can be deduced that PoppedNodes must have
> > > the same type as DummyNode:
> > 
> > No, it can't.
> > 
> > > :- typeclass csp(T, N) <= node(N) where [
> > > 	...
> > > 	pred pop_stack(list(N), T, T),
> > > 	...
> > > ].
> > > 
> > > :- pred solve(conflict_fn, bool, N, T, T) <= csp(T, N).
> > >
> > > So, N is related to T, the pop_stack/3 method returns a
> > > list of N, and we know that N is a polymorphically typed
> > > argument.
> > 
> > You're assuming here that the csp(T, N) instance
> > in the call to `solve' must be the same as that
> > in the call to `pop_stack'.  But there is no such
> > requirement.
> 
> Now I am totally confused.  If I write
> 
> :- typeclass csp(T, N) where [ pred pop_stack(list(N), T, T), ... ].
> 
> is it not the case that
> (1) T and N are *type* variables and that 

Yes, that's right so far...

> (2) given an instance csp(A, B) with X0:A, X:A (using : as a typing
> operator), declared as a typeclass constraint on a pred, then
> (3) a method call pop_stack(Ys, X0, X) in the body of the pred 
> implies that Ys:list(B).  

No.  It just implies that Ys has type list(C) with the constraint csp(A, C),
for some type variable C.  There is no requirement that C = B.

> The deduction Ys:list(B) relies purely on the typeclass definition,
> the typeclass constraint on the pred, the type of X0 and X, and the
> signature of the method call.

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.

> If we take a trivial example:
> 
> :- pred eg(N, T, T) <= csp(T, N).
> :- mode eg(unused, in, out) is det.
> 
> eg(DummyN, T0, T) :-
> 	pop_stack(Ns, T0, T1),
> 	push_agenda(Ns, T1, T).
> 
> I just can't get my head around why the N in DummyN:N could be
> different from the N in Ns:list(N).  T0, T1, and T all have the
> same type.

Well, there might be multiple instance declarations for csp, e.g.

	:- instance csp(my_cst, int).
	:- instance csp(my_cst, float).
	:- instance csp(my_cst, string).

and even if the arguments to `eg/3' have T=my_cst and N=int,
the call to `pop_stack' could be intended to refer to a
different instance declaration, e.g. the one with `float'
rather than `int'.

Here's a different example which may make it clearer:

	:- typeclass printable(Stream, Type) where [
		pred print_method(Stream, Type, io_state, io_state)
		mode print_method(in, in, di, uo) is det
	].

	:- pred my_format(Term, Stream, io__state, io__state)
		<= printable(Stream, Term).
	:- mode my_format(in, in, di, uo) is det.

	my_format(Term, Stream) -->
		print_method(Stream, Term),
		print_method(Stream, ".\n").

In this hypothetical example, the predicate `my_format' here contains
two calls to `print_method', which is a method of the printable/2 type
class.  In the first call to print_method, the `Term' type parameter
in that call will have the same value as the `Term' type parameter
in the class constraint for `my_format'.  But in the second call,
the `Term' type parameter has a different value, namely `string'.
This second call shows that a type class method call from a procedure
with a type class constraint for that class need not have the same
values for the type class parameters.

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