[mercury-users] typeclass error

[Ian MacLarty]

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.

>>
>> I get the following error when I try to compile it:
>>
>> tc.m:024: In function `tc.f/2':
>> tc.m:024:   type error: unsatisfied typeclass constraints:
>> tc.m:024:       `tc.tc1(A, C)'
>> tc.m:024:       `tc.tc2(B, C)'
>> tc.m:024: In function `tc.f/2':
>> tc.m:024:   warning: unresolved polymorphism.
>> tc.m:024:   The variable with an unbound type was:
>> tc.m:024:       V_6: C
>> tc.m:024:   The unbound type variable(s) will be implicitly
>> tc.m:024:   bound to the builtin type `void'.
>
> The error message would be better if the location of the place where 
> the
> constraint arose in the clause was reported, rather than the location 
> of
> the func declaration.  But the compiler doesn't currently keep enough
> information to be able to do that, unfortunately.
>
> Here are two ways that you can get the code to compile:
>
> a) Rewrite the clause so that there are unifications that imply that 
> C1 and
> C2 are the same as C.  For example:
>
> 	f(A, B) = C :-
> 		C0 = a_to_c(A),
> 		( if C0 = b_to_c(B) then
> 			C = C0
> 		else
> 			C = b_to_c(B)
> 		).
>
> b) Add functional dependencies so that the compiler can "improve" the 
> types
> C1 and C2 to be equal to C.  For example:
>
> 	:- typeclass tc1(A, C) <= (A -> C) where [ ... ].
>
> or
>
> 	:- typeclass tc2(B, C) <= (B -> C) where [ ... ].
>

Actually the code I gave was a simplification of another problem I was 
trying to solve.  I've opted to use higher order code instead of 
typeclasses which gets around the type error.

Thanks for your help,

Ian.

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