[mercury-users] typeclass error

[Mark Brown]

On 19-Jan-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> On 19 Jan 2006, at 05:39, Mark Brown wrote:
> 
> >On 18-Jan-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> >>Hello,
> >>
> >>What's wrong with the following program?
> >>
> >>:- module tc.
> >>
> >>:- interface.
> >>
> >>:- import_module io.
> >>
> >>:- pred main(io::di, io::uo) is det.
> >>
> >>:- implementation.
> >>
> >>:- import_module list, int.
> >>
> >>main(!IO) :-
> >>        nl(!IO).
> >>
> >>:- typeclass tc1(A, C) where [
> >>        func a_to_c(A) = C
> >>].
> >>
> >>:- typeclass tc2(B, C) where [
> >>        func b_to_c(B) = C
> >>].
> >>
> >>:- func f(A, B) = C <= (tc1(A, C), tc2(B, C)).
> >>
> >>f(A, B) =
> >>        ( if a_to_c(A) = b_to_c(B) then
> >>                a_to_c(A)
> >>        else
> >>                b_to_c(B)
> >>        ).
> >
> >First, here's the clause with some explicit type annotations:
> >
> >	f(A, B):C0 =
> >		( if a_to_c(A):C1 = b_to_c(B):C2 then
> >			a_to_c(A):C3
> >		else
> >			b_to_c(A):C4
> >		):C5.
> >
> >Because of the result unification, we know that C0 = C5.  Because of 
> >the
> >semantics of if-then-else expressions, we know that C3 = C5 and C4 = 
> >C5.
> >Because of the unification in the condition, we know that C1 = C2.  So 
> >at
> >this stage there are two equivalence classes: {C0,C3,C4,C5} and 
> >{C1,C2}.
> >There is nothing in the clause which implies that these two equivalence
> >classes are the same.
> >
> >The first equivalence class is the type of the function result, so it 
> >is
> >bound to the universally quantified C from the func declaration.  Hence
> >the method calls in the "then" and "else" branches will call methods in
> >those dictionaries that are passed in as hidden arguments to f (that 
> >is,
> >the dictionaries that correspond to the two constraints on the func
> >declaration).
> >
> >The second equivalence class remains unbound.  Hence there are no 
> >assumed
> >constraints (e.g., constraints on the func declaration) that can 
> >satisfy
> >the constraints on the method calls in the condition; this explains the
> >first part of the error message.  The warning you get is because 
> >unbound
> >type variables are generally never what the programmer intends.
> >
> 
> That all makes perfect sense.  I was under the illusion that the 
> compiler would know that C1 and C3 are of the same type, because they 
> have the same value, but I guess type inference doesn't know anything 
> about the values.

Without the functional dependency, they wouldn't necessarily have the same
value, let alone the same type.  ;-)

Consider:

	:- typeclass convertible(A, B) where [
		func cast(A) = B
	].

	:- instance convertible(int, int) where [
		(cast(N) = N)
	].

	:- instance convertible(int, string) where [
		(cast(_) = "some number")
	].

	main(!IO) :-
		io.write_string(cast(1), !IO),
		io.nl(!IO),
		io.write_int(cast(1), !IO),
		io.nl(!IO).

The output would be:

	some number
	1

You should think of cast/1 as being an overloaded name, which is why it
appears to violate referential transparency.

Cheers,
Mark.

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